← Reports

An AI assistant next to Prover iLock: it reads everything, and changes nothing.

On a customer project, an AI assistant now works beside the engineer's Prover iLock work. It reads the model and the verification report, and asks Prover iLock to run. It cannot change a single line of the model.

Tianqi ZhaoCreated on 19 September 2026 · ~5 min read

The setup

1

"How do I write this requirement as a check the tool can prove?"

2

"This check came back Falsifiable. Why?"

Falsifiable: the verifier found an instance where the check does not hold. A result, not an error.

Two questions that come back on nearly every station. The reasoning is not hard. Gathering the facts is:

three files, three formats, none written to be read side by side The English sentencefrom the specification The object modelreal classes and members What Prover iLock computedreports, tables, traces MCP server on the engineer's machine AI assistant the "agent" all three at once, in a form it cannot fake
An MCP server (Model Context Protocol) is a small local program an AI application calls to get structured data back. Plumbing, nothing to do with railways.

Three parties, three different powers

reads computesValid / Falsifiable drafts,explains judgesthe cause writesthe model Prover iLock ✓ only it The agent ✓ text The engineer ✓ ✓ only
Who owns which verb is the whole safety argument. Only the engineer has write access to the model, and that is not configurable.
Prover iLock computes the truth

Instantiates the model, runs the verifier, writes evidence into the project's own output folders.

Never interprets or explains a value.

The agent reads, drafts, explains

Returns drafts and explanations as text only, and asks iLock for missing evidence.

Never edits a file, names a member the lookup did not return, or decides a fix is correct.

The engineer judges and applies

Owns the requirement's intent, checks every member, makes every change.

Formalization mistake, data-entry mistake or design fault: their call.

One request, end to end

The engineer The agent Prover iLock 1 2 3 5 The project's model files classes · members · predicates · data 4 readsnever writes 6 writesthe only one
1 Plain-English question, no tool names. 2 The agent picks tools and calls them through the server, which returns an error rather than an invention when a fact is missing. 3 Prover iLock returns reports and values, generating any that are missing. 4 The model files are read, never written. 5 A draft or explanation comes back as text. 6 The engineer makes the change by hand, the only step that alters the project.

Worked example 1: why a check failed

A data check requires a trackside tag to sit at least 600 m ahead of the level-crossing track. The verifier says Falsifiable.

"Why does this check fail in this project?"

a question root cause ofone named check? no yes read the reports: secondsFalsifiable for three tag instances warn, then generate the traceminutes, not seconds, on a large station
Cheap answer first. For most questions the story ends there; the expensive analysis never runs on a vague question.

The trace is partial evaluation: Prover iLock unfolds the failing predicate for concrete instances and records each sub-expression's value.

ALL lcra:SELF.associated_lc
  SOME line (
    objects_in_path(line, SELF) &
    SOME lx:lcra.objects (
      objects_in_path(line, lx) & (… lx.distance - SELF.distance >= 60000 …)))

Most cases are false only because objects_in_path is false: noise. One case binds a real line and a real level-crossing track:

The punchline

Distance from tag to level-crossing track

5 m short
Required
600 m
Actual
595 m

lx.distance - SELF.distance == 59500 cm against >= 60000. The model counts centimetres (and milliseconds), so the agent quotes raw value and conversion.

As here: design fault

move the tag

The table agrees: 59500 cm, no factor of 100. The design itself is wrong. No predicate is touched.

Twin case: data entry

fix the table

Had the table said 595 while the model counts centimetres: a unit mistake, fixed in the table.

The agent lays out both, with evidence. Choosing, and moving equipment on a live railway, is the engineer's judgment.

Worked example 2: from a sentence to a predicate

"The maximum distance between two consecutive tags shall not be more than 1000 m."

Find the class→ List its real members→ Read existing predicates→ Check PiSPEC syntax→ Only then compose

Rule: never reference a member the lookup did not return; a missing one becomes an open question.

"""
The maximum distance between two consecutive tags shall not be
more than 1000m.

Note: Formalized as |SELF.distance - adjacent.distance| <= 100000 cm.
Traceability: <specification clause>
"""
DATACHECK_<clause>_max_tag_distance :=
  ALL rf:SELF.adjacent_tag (
    // 1000m = 100000 cm
    (SELF.distance - rf.distance <= 100000) &
    (rf.distance - SELF.distance <= 100000)
  );
Returned as text, in the model's house style, with a placement suggestion: the tag class's static invariants, after the last predicate. The clause in the name traces a report row back to its sentence.
1

Does the restatement mean what the requirement means?

2

Does every named member exist on the class?

3

Is the unit right? 1000 m = 100000 cm.

All three hold: the engineer pastes it in. If a draft looks doubtful, one question settles it:

"Show me which object-model members and existing predicates you used for that draft."

A grounded answer can name them. An invented one cannot.

The words used above

Object model

The classes describing things on the railway, with parameters and variables.

PiSPEC

The specification language Prover iLock models are written in.

Data check (static invariant)

A predicate that must hold for every instance of a class, given the design data.

Falsifiable

An instance fails the check. A result, not an error; it names the instances.

Traceability reference

The clause reference linking requirement, predicate and report row.

Partial evaluation

Unfolding a failing predicate for concrete instances. The raw material for a root cause, and why it is slow.

MCP server

A small local program on the engineer's machine; it sends nothing anywhere on its own.

Agent

The AI assistant that decides which tools to call, in what order, and writes the answer.

Written for Prover Labs, based on Prover's own experience connecting an AI assistant to Prover iLock on a customer project, 19 September 2026. Simplified for orientation: the tools have real parameters and limits, some evidence is more reliable than the rest, and a requirement whose class does not exist yet takes a different route. None of that changes who may write to the model. Not a specification.