Try Prover's AI applications on your own requirements and traces. What the AI writes is never taken on trust: a proof engine decides whether it is safe.
An interactive simulation of the AI-to-proof workflow.
Let's get these three trains
home.
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.
Nothing to tell yet.
AppCounterexample StorytellerA raw proof-engine trace becomes a cycle-by-cycle story, the signals that matter separated from the noise.
The closed loop
Know, model, verify.
One rule about locked routes, followed through three Prover Labs applications: found in the knowledge base, grounded in an object model, and played back where the proof breaks.
Ask Prover / New conversationShare●Ask
What must the interlocking guarantee while a train route is locked?
TRVINFRA-00303 — Reservation of track sectionspublic
§5.2 Locked train route · K124440public
While it is locked, the route shall technically ensure that the following requirements are met …
HLL — industrial usage examplesinternal
✓read_docTRVINFRA-00303 §5.2read
TRVINFRA-00303 · K124440TRVINFRA-00303 · K124441
↑
01 Know
Ask, and see where the answer comes from
A question about a Swedish signalling rule. Ask Prover searches Prover's own knowledge base before it answers, and every claim points back at the clause it came from.
Ask Prover / New conversationShare●Ask
What must the interlocking guarantee while a train route is locked?
TRVINFRA-00303 — Reservation of track sectionspublic
§5.2 Locked train route · K124440public
While it is locked, the route shall technically ensure that the following requirements are met …
HLL — industrial usage examplesinternal
✓read_docTRVINFRA-00303 §5.2read
TRVINFRA-00303 · K124440TRVINFRA-00303 · K124441
↑
02 Model
Turn the specification into an object model
Every requirement row grounds a type or an attribute; the graph is the model. A family lights up as one, and a type opens on the rows behind it, the locked-route rule among them.
Sample project / Object model · graphShare●Ask
Every type, grounded in a requirement row
03 Verify
Play the counterexample on the real station
Prover finds the cycle where that rule breaks. Counterexample Studio replays it on the station drawing, so the failing signal and section are the ones an engineer knows.
Counterexample Studio / REQ-041 · Test stationShare●Ask
Cycle 0 of 4
Requirement does not apply at cycle 0
Initial cycle: no track is confirmed clear, no points are detected, S1 is not commanded to proceed.
When
✗S1 is commanded to proceed
✗route S1–S9 is set
Then required
✗every track of S1–S9 is clear
Counterexamples repair the model. Proven results become reusable knowledge.
The same evidence trail works across requirements, signaling design and software verification.
Ask Prover
One agent. Four applications. Prover's own knowledge.
The engineering principle
AI generates.Prover verifies.
The draft amendment to EN 50716 asks for the same: AI may be used across the railway software lifecycle, as long as a diverse, independent tool checks each output.
EN 50716:2023/prA1:2026 (draft) · clause 6.7.4.4
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
