Nothing to tell yet.
Prover Labs
Prover LabsAI-driven innovation
Discover and shape the future
Prover Labs is a space and community where innovation thrives. We invite you to test cutting-edge applications and give feedback on solutions involving artificial intelligence, formal methods and digital twins.
The 60-second challenge
Let's get these three trains home.
An interactive simulation of the AI-to-proof workflow.
Junction 1 · 3 trains · 5 track sectionsno rules
Get all three home. Dispatch the trains with the signals and the points. No safety rules are active.
1Now prevent it You
Every ticked rule is in force at once. Prover judges the whole set.
AppAmbiguity RadarThe defensible readings of one sentence, the words where they diverge, and the question that settles it.
AppReq Quality CheckerOne requirement against the usual quality criteria, with a rewrite.
2The formal rules Prover Agent
The agent translates each sentence into HLL, the language Prover proves in — exactly what you said, flaws included.
Tick a rule on the left. The agent writes its HLL
form here, and every rule in force stays listed.Rules in force: none. Every order you give will be obeyed.
AppFormal-Req Description CheckerDoes the formal text say the same thing as its informal description? Nothing missing, nothing extra.
3The verdict Prover
Prover explores every order the trains could be given under the rules in force. No sampling, no testing — every order.
Nothing to prove yet.
With no rules in force, any order is allowed — including the ones that end in a collision. Tick a rule to give Prover something to check.
ProductProver iLock · Prover PSLNot an app — what Prover has done for real interlockings since 2008: every reachable state, or a counterexample.
4The story Prover Agent
When Prover hands back a counterexample, the agent reads the raw trace and tells it cycle by cycle — the Counterexample Storyteller.
AppCounterexample StorytellerA raw proof-engine trace becomes a cycle-by-cycle story, the signals that matter separated from the noise.
The engineering principle
AI generates.Prover verifies.
AI accelerates the work. Prover establishes whether the result is safe.
AI accelerates
Generates- Reads documents, drawings and existing software
- Drafts requirements, models, configuration data and fixes
- Explains counterexamples in engineering language
Prover assures
Verifies- Checks properties derived independently from the generated artifact
- Explores every reachable behavior in the formal model
- Returns a proof or a reproducible counterexample
- Produces evidence engineers and assessors can review
Engineers approve what moves forward.
The applications
Four tools, on your own text
The four steps of the challenge are four applications, written here by Prover's AI team. Bring a requirement, a formal expression or a counterexample trace, and tell us with the thumbs under the result what to build next.
- Req Quality CheckerOne requirement against the usual quality criteria, with a rewrite.
- Formal-Req Description CheckerDoes the formal text say the same thing as its informal description?
- Ambiguity RadarThe defensible readings of one sentence, and the question that settles it.
- Counterexample StorytellerA raw proof-engine trace, told cycle by cycle in plain language.
Ask Prover
One agent. Four applications. Prover's own knowledge.
Ask a question, paste a requirement or attach a document. It reads the knowledge base, runs the application the question calls for and shows where the answer came from.
Or open Ask Prover with your conversations, bookshelf and memory.
Agent
Plans, searches, runs, remembers
Several tools at a time, and it keeps what you tell it.
Tools
The four applications, inside the answer
Paste a requirement or a trace and the right one runs.
- Req Quality Checker
- Formal-Req Description Checker
- Ambiguity Radar
- Counterexample Storyteller
Prover's own knowledge
Standards, manuals, project notes
Every answer cites the page it rests on.
The team
Built by the Prover AI team
Built in house
The applications are written by Prover's AI team on top of the company's formal-methods and railway signaling expertise. The reasoning behind each answer is our own code, not a third-party chat product.
Measured before it ships
Every application is run against a fixed test set before a change goes live, so a new prompt or model has to hold its ground on cases we already care about. Quality is tracked, not assumed.
Your feedback decides what is next
The thumbs up and thumbs down under each result goes straight to the team, together with your comment. It is the main input to what we build and fix next.
The mission
Experience cutting-edge technology
At Prover, our mission is to engineer a safer world by automating the design, development and verification of safety-critical rail systems.
Through Prover Labs, we offer you the opportunity to engage with the latest innovations in AI, formal methods and digital twins. These technologies are key to advancing our goals of greater automation and efficiency, without ever compromising on safety.
Tell us what to build next
Tell us what you would like to see, or ask a question; a Prover engineer answers by email.