Plugging an AI into Prover iLock

Two questions that eat a whole afternoon

This work connected an artificial intelligence (AI) assistant to Prover iLock so engineers could draft checks and investigate failed checks without manually comparing several files. It mattered because the reasoning is often straightforward, but gathering the necessary facts can take a whole afternoon.

Two questions come back on nearly every station: "How do I write this requirement as a check the tool can prove?" and "This check came back Falsifiable — why?" Falsifiable means the verifier found at least one instance where the check does not hold. It is a result, not an error, and it names the affected instances.

Answering either question means holding three separate things in mind: the English sentence from the specification; the real members of a class in the object model — the classes that describe railway objects, such as tags, lines and level crossings, with their parameters and variables; and the numbers Prover iLock computed for that station. These sources live in different files and formats, none designed to be read side by side.

The setup uses an MCP server — Model Context Protocol, a standard way for an AI application to call a small local program and receive structured data. This server runs on the engineer's machine and puts all three sources in front of the assistant at once, in a form the assistant cannot fake.

The agent — the AI assistant that decides which tools to call and in what order, then writes the answer — works with those sources under strict limits on who may compute, explain and change the project.

Three parties, three different powers

Three parties are involved, and each owns a different verb. That division is the safety argument for the arrangement.

Prover iLock: computes the truth

Instantiates the station model from the layout and entered data.
Runs the verifier and decides Valid or Falsifiable. Nothing else may make that call.
Produces the evidence the other parties read: the verification and traceability reports, tables of entered values for tags, signals and routes, the exported layout topology and the partial-evaluation trace.
Writes those files only to the project's own output folders.

Never: interprets, argues or explains. It reports a value but does not say what that value means.

The agent: reads, drafts and explains

Finds the correct object-model class for a requirement and lists its real members before writing anything.
Looks up existing checks in the project's model so that a new one follows the same style.
Drafts a predicate — a condition in the model's own language that must hold for every object of a kind — and returns it as text, with a suggested file and class.
Reads a failing check together with its formal expression and trace, then explains which case fails and by how much.
Asks Prover iLock to generate a missing report or trace when the required data is not yet on disk.

Never: edits a model file, names a member the lookup did not return or decides that a fix is correct. If something is missing, it must say so rather than guess.

The engineer: judges and applies

Owns the requirement's intent. Only the engineer knows whether a draft says what the specification meant.
Checks the suggested class and every referenced member against the model before accepting a predicate.
Decides whether the problem is a formalization mistake, a data-entry mistake or a genuine design fault.
Performs every change: inserting the predicate, moving the equipment or correcting the table.

Always: the engineer is the only party with write access to the model. That restriction is deliberate and is not configurable.

One request, end to end

A question travels from the engineer's keyboard to an answer and back. The agent may consult the sources repeatedly, but nothing in the model changes while it does so. Only the final, human step touches a file that matters.

The engineer asks in plain English, without tool names or parameters.
The agent chooses the tools it needs and calls them through the MCP server.
The server fetches the real classes and members from the object model, together with reports and tables from Prover iLock. It returns an error rather than an invention when a fact is missing.
If required evidence does not exist, the agent asks Prover iLock to generate it in the project's own output folder.
The agent drafts or explains and returns text only.
The engineer reviews the answer, decides what to do and makes the change by hand.

The path from the engineer's request through the MCP server, Prover iLock and the agent. The orange arrow is the only action that alters the project, and it belongs to the engineer.

Why a check failed, followed to its punchline

A data check — a predicate that must hold for every instance of a class, given the design data — requires a trackside tag to sit at least 600 m ahead of the level-crossing track. The verifier reports the check as Falsifiable.

The engineer asks the question as they would ask a colleague:

The agent starts with the quick evidence. It reads the verification and traceability reports and returns an answer in seconds: the check requires at least 600 m, and it is Falsifiable for three tag instances. For most questions, the investigation ends here. The slower analysis is not run for a vague question.

The engineer asks for the root cause of one named check. That specific request unlocks the deeper analysis. The agent warns that it can take a long time — minutes rather than seconds on a large station.

Prover iLock produces the evidence. The required trace does not yet exist, so Prover iLock generates it. Partial evaluation unfolds the failing predicate for concrete instances and records the result of each sub-expression. The trace is written only to the project's output folder.

The agent reads the trace against this predicate:

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 …)))

The data check requiring the distance from the tag to the level-crossing track to be at least 600 m.

Most cases in the trace are false only because objects_in_path is false: the track is not on that tag's line. The informative case binds a real line and a real level-crossing track. Its distance sub-expression evaluates to:

The model uses base units: centimetres for distance and milliseconds for time. The agent gives both the raw value and its conversion so the engineer can check it.

The engineer makes the call the number cannot make. Being 5 m short has two possible explanations, and only one is a track problem:

In this case, the table of entered values agrees with the computed 59500 cm. There is no factor of 100. The data is exactly as designed, so this is a real design fault. The fix is to move the tag; the predicate is not changed.
In the corresponding data-entry case, a table value of 595 while the model computes in centimetres would indicate a unit or data-entry mistake. The table would be corrected instead of the track.

The agent can present both possibilities with their evidence. Choosing between them and moving equipment on a live railway remain engineering judgments that the tool is deliberately not allowed to make.

From a sentence to a predicate

The other half of the work begins with a requirement from the project's specification: "The maximum distance between two consecutive tags shall not be more than 1000 m."

Before drafting anything, the agent must identify the relevant class, list its actual members, inspect how existing predicates express distance and check the syntax of PiSPEC — the specification language used to write Prover iLock models. Only then may it compose the predicate.

The result comes back as text in the model's house style:

"""
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)
  );

The drafted PiSPEC predicate for the maximum permitted distance between consecutive tags.

The agent also suggests where to place the text rather than editing the model: in the static invariants section of the tag class, after the last existing predicate. The check name carries the specification clause as a traceability reference — the clause reference that links the English requirement, predicate and verification-report row.

The engineer reviews three specific points:

Does the English restatement still mean what the requirement means?
Does every member named in the expression exist on the class?
Is the unit conversion correct — here, 1000 m written as 100000 because the model counts centimetres?

If all three hold, the engineer pastes the predicate into the model. If one does not, the engineer identifies the problem and asks for another draft.

If a draft looks doubtful, one question exposes its basis:

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