An LLM's Logic, Checked Twice

TL;DR

Using Claude Opus 5.5, eighteen invented interlocking rules were translated into first-order clauses. Over three runs with the same prompt, 17, 18 and 17 of 18 were logically equivalent to a hand-written gold formalisation once type guards are allowed, and 12, 14 and 13 under the strict comparison.
The verdict never comes from the model. Two independent provers decide equivalence: Foras, my Rust port of the Otter theorem prover, and Z3. They agreed on every verdict, and on all 1,000 problems of a separate random cross-check.
The one real disagreement is about language, not logic. The model read “either … or” in rule R10 as exclusive in 2 runs and inclusive in 1, and said which reading it chose every time.
On the design side, a bounded model checker proves 5 safety properties of a toy junction interlocking and finds a seeded one-line bug as a 3-step counterexample that replays in a separately written simulator.
Limits: the rules are invented and easy, the gold formalisations are mine, and each rule is judged on its own, without the other 17.

Why check a model with a prover

On the tail end of massively popular large language models we’re starting to see a dramatic interest in a field which people forgot about more than Dre. Formal Verification.

ANo, but seriously, there seem to be growing interest in Formal Verfication, and that’s nice to see. The problem with Formal Verification is that humans write the Form. However, there’s an elephant in the room: Human Error. No amount of verfication is going to change the fact that the rationality of the input may already be compromised before verification has even begun. The failed maiden flight of Ariane 5 is one example. We can verify the logic all day long, but if the assumptions underlying the specifocation are wrong, then we’re just (unknowingly) verifying a pending catastrophy.

Just something to be mindful of.

Railway signalling software is held to SIL 4, the strictest safety level. CENELEC’s draft amendment to EN 50716 on AI tools, as Prover Technology summarises it, puts code and data generators in tool class T3 and asks for “verification of tool output by an independent, diverse tool or process” [1]. It names the failure modes to look for: tools that share a common cause, models that “prioritize fluency over semantic precision”, and runs that can’t be reproduced.

Project Process

The pattern that follows is generate, then verify. A language model may propose something, but it may not decide. This post builds a small version of that pattern end-to-end, and measures where it breaks.

Rules                                   Design
─────                                   ──────
rule text                               toy interlocking model
  │ LLM proposes clauses                  │ Z3: bounded model checking
  ▼                                       │     + inductive invariant
parse + vocabulary check                  ▼
  │ (≤ 2 repair rounds)                 proof for all reachable states,
  ▼                                     or a counterexample
Foras and Z3, separately:                 │
"equivalent to gold?"                     ▼
  │                                     replayed in an independent simulator
  ▼
verdict + audit log

The language of interlocking

Let’s start by creating a formal language that we can use to translate propositions stated in natural language to a language which machines can verify and reason about.

Definition 1 (Vocabulary and clauses).

The vocabulary is 16 function-free predicates, such as

\mathit{locked}(R)

\mathit{conflicts}(R_1,R_2)

\mathit{in_route}(T,R)

and

\mathit{occupied}(T)

. A clause is a disjunction of literals

C = \ell_1 \lor \dots \lor \ell_k

whose variables are universally quantified. A formalisation of a rule is a finite set of clauses.

Let’s use our language on something we want to verify:
Rule R01: “Two conflicting routes are never locked at the same time”, becomes one clause:

\forall x\,\forall y\;\big(\neg\mathit{conflicts}(x,y) \lor \neg\mathit{locked}(x) \lor \neg\mathit{locked}(y)\big).

The model receives the rule text and the vocabulary, and must answer with clauses plus a free-text field, assumptions, saying how it read the rule. A parser checks syntax and that every predicate exists with the right arity. If either check fails, the error message goes back to the model, at most twice. The gold answer is never sent.

What counts as correct?

Next we Let’s start by creating a formal language that we can use to translate propositions stated in natural language to a language which machines can verify and reason about.

Definition 2 (Acceptance).

Let $G$ be the gold formalisation of a rule, $F$ the model’s, and $\Theta$ a background theory. $F$ is accepted when

\Theta \cup F \models G \quad\text{and}\quad \Theta \cup G \models F .

If only the first entailment holds, $F$ is too strong; if only the second, too weak; if neither, different.

Two background theories are used. Strict: $\Theta = \emptyset$ . Modulo typing: $\Theta$ is 18 typing axioms, such as $\neg\mathit{locked}(x) \lor \mathit{route}(x)$ (“only routes are locked”). The second exists because a formalisation that adds a type guard, $\neg\mathit{route}(x) \lor \dots$ , says something weaker in general, but the same thing in every layout where the types are right.

Proposition 1 (What acceptance guarantees).

F

is accepted modulo

\Theta

, then every structure

\mathcal{M}

with

\mathcal{M} \models \Theta

satisfies

\mathcal{M} \models F \iff \mathcal{M} \models G

Proof

Suppose

\mathcal{M} \models \Theta

and

\mathcal{M} \models F

. Then

\mathcal{M} \models \Theta \cup F

, and since

\Theta \cup F \models G

\mathcal{M} \models G

. The converse is symmetric, using

\Theta \cup G \models F

. ∎

In words: in every well-typed layout, the model’s clauses and the gold clauses are true in exactly the same situations. That is the whole claim. It says nothing about whether the gold formalisation itself captures what an engineer meant. I return to that in the limits.

How an entailment is decided

$\Theta \cup F \models G$ holds exactly when it holds for every clause $c \in G$ , and each of those is checked by refutation:

\Theta \cup F \models c \iff \Theta \cup F \cup \{\neg c\,\sigma\} \text{ is unsatisfiable},

where $\sigma$ replaces the variables of $c$ by fresh constants, so that $\neg c\,\sigma$ is a set of ground unit clauses. Every query is sent to Foras and to Z3 separately. Foras answers “proof found” (unsatisfiable) or “search saturated” (satisfiable). Z3 answers unsat or sat. A disagreement is logged and counted.

Proposition 2 (Every check terminates).

For function-free clause sets, the question whether

\Theta \cup F \cup {\neg c,\sigma}

is unsatisfiable is decidable.

Why

With no function symbols, the Herbrand universe is the finite set of constants in the problem (the layout constants plus those introduced by

\sigma

). Each clause therefore has finitely many ground instances, and by Herbrand’s theorem the set is unsatisfiable iff a finite set of ground instances is propositionally unsatisfiable, which is decidable. This is the Bernays–Schönfinkel class [2]. In practice, both provers answered every query in these experiments.

Results

This figure needs JavaScript.

Figure 1. Every verdict from three runs of Claude Opus 5.5 on the 18 rules (columns R01–R18). Hover or tap a cell to see the rule, the gold clauses, the model’s clauses and the reading the model said it chose. Strict compares without typing axioms. The data is re-scored from the runs’ audit logs by railcheck.postdata, with no further API calls.

Table 1. Verdicts per run (18 rules each).

Run	Strict: equivalent	Strict: too weak	Strict: too strong	Modulo typing: equivalent	Z3 agrees with Foras
1	12	5	1	17	all
2	14	4	0	18	all
3	13	4	1	17	all

Each run cost about $0.13 (roughly 14,000 input and 3,400 to 4,000 output tokens). No answer needed a repair round: every response parsed and used the vocabulary correctly.

Every strict-only failure is a type guard. For R04, “If a route is not locked, its signal does not show proceed”, the gold clause is $\neg\mathit{clear}(x) \lor \mathit{locked}(x)$ . Run 1 answered $\neg\mathit{route}(x) \lor \mathit{locked}(x) \lor \neg\mathit{clear}(x)$ . Strictly that is too weak, because it says nothing about objects that are not routes. Modulo typing it is equivalent. The same happens with R09, R11, R15, R18 and, in run 3, R02. The checker does not need to be lenient for this: it applies $\Theta$ exactly and reports both numbers.

The one real disagreement: “either … or”

R10 reads: “Every set of points is either in the normal or in the reverse position.” The two readings are

\text{inclusive:}\quad \forall x\,\big(\mathit{points}(x) \to \mathit{normal}(x) \lor \mathit{reverse}(x)\big)

\text{exclusive:}\quad \text{inclusive} \;\land\; \forall x\,\big(\mathit{points}(x) \to \neg(\mathit{normal}(x) \land \mathit{reverse}(x))\big).

Runs 1 and 3 chose the exclusive reading and were judged too strong. Run 2 chose the inclusive one and matched the gold. Each time, the model stated its choice in the assumptions field, for example (run 1): “I read ’either … or’ as exclusive … If only the ‘at least one position’ reading is intended, drop the second clause.”

This is the behaviour the EN 50716 draft worries about: same model, same prompt, different meaning. Here it was not hidden. The verifier caught the difference and the model explained it. The right fix is to the requirement text, not to the model.

Does the checker catch wrong formalisations?

Agreement with a gold answer means little if the checker accepts almost anything. To test it, every gold formalisation is corrupted mechanically: a clause or a literal is dropped, a sign flipped, the arguments of a predicate swapped, a variable turned into a constant, or two variables merged. That gives 78 corrupted formalisations.

Outcome	Count
Caught by the parser or vocabulary check	18
Rejected by the provers as not equivalent	58
Accepted	2

Z3 confirms that both accepted ones are genuinely equivalent to the gold (the mutation happened not to change the meaning). So there were 0 false accepts and 0 false rejects. (Three random seeds produce the same 78 mutations, so this is one set, not three.)

The two provers are also tested against each other directly. On 1,000 random function-free clause sets, 840 satisfiable and 160 unsatisfiable, Foras and Z3 gave the same answer every time. Getting there took two fixes to Foras’s subsumption and duplicate-literal handling. Both bugs were found by exactly this kind of differential testing.

The design side: a toy interlocking

Rules are only half the story. The other half is the logic that is supposed to obey them. The toy model is a junction with two routes that share one section and one set of points. Route 1 needs the points normal, route 2 needs them reverse. The model has 8 Boolean state variables and 8 inputs.

Definition 3 (Transition system and safety property).

A transition system is a triple

(S, I, T)

: states

S = {0,1}^8

, an initial-state predicate

I(s)

, and a transition relation

T(s, i, s')

over a state, an input and the next state, constrained by environment assumptions

E(s,i)

(for example, trains obey signals). A safety property

P(s)

holds if it is true in every reachable state.

Five properties are checked. Two of them are P3, “signal 2 shows proceed only when the points are reverse”, and P5, “the points are never thrown while a route is locked”. A counterexample of length $k$ exists iff this formula is satisfiable [3]:

I(s_0) \;\land\; \bigwedge_{t=0}^{k-1} \Big(E(s_t,i_t) \land T(s_t,i_t,s_{t+1})\Big) \;\land\; \bigvee_{t=0}^{k} \neg P(s_t).

Bounded search only shows the absence of short counterexamples. For a proof over all reachable states, the checker looks for an inductive invariant $J$ with

I(s) \Rightarrow J(s), \qquad J(s) \land E(s,i) \land T(s,i,s') \Rightarrow J(s'), \qquad J(s) \Rightarrow P(s),

starting from the five properties plus four candidate helper facts (such as “route 1 locked implies points normal”) and dropping candidates until the rest is inductive. This is the Houdini algorithm [4].

On the intended design, all 5 properties are proved this way. The invariant uses all four helpers, and the base case is also checked to depth 10. Then one bug is seeded. The guard that decides whether the points may move checks that route 1 is not locked, but forgets route 2:

\mathit{can\_move} = \mathit{mv} \land \neg j \land \neg \mathit{can}_1 \land \neg \mathit{can}_2 \land \neg r_1 \;\underbrace{\land\; \neg r_2}_{\text{missing}}.

P1, P2 and P4 are still proved. P3 and P5 fail, with this counterexample:

This figure needs JavaScript.

Figure 2. The counterexample Z3 found for the seeded bug, step by step. Choose P3 or P5 to see which part of the state breaks each property. The same three inputs (throw points, request route 2, throw points) violate both. Every counterexample is also replayed through a plain-Python simulator written independently of the Z3 encoding.

Read as a story: the points are thrown to reverse, route 2 is granted, and then the points are thrown back to normal while route 2 is still locked and its signal still shows proceed. The fault is a single missing conjunct, the kind a review can miss and a model checker can’t.

What this does not show

The rules are invented and easy. No answer needed a repair round, so the repair loop was never tested. Real requirements are longer, refer to each other, and are more ambiguous.
The gold standard is mine. If my gold formalisation is wrong, “equivalent to gold” is wrong too. The consistency check of the whole rule base against a small layout is the one gold-free safeguard, and it is weak.
Rules are judged one at a time. The R10 note above shows that this can be too strict. It can also be too lenient.
The corrupted formalisations measure the checker, not the model. Mechanical mutations are not the mistakes an LLM makes.
Three runs is a small sample. The R10 split (2 to 1) shows that variation is real. It does not estimate how often it happens.
Toy scale. A 2-route junction is not a station. Prover’s model checker handles real interlockings. This one is for explaining the idea.

Reproducing the numbers

All numbers come from the railcheck project: the per-run verdicts from the audit logs in runs/, re-scored by railcheck.postdata; the model checker from railcheck.cli; the mutation test from railcheck.formalize --formalizer mutant; and the cross-check from railcheck.crosscheck --random 1000. Foras was built from its stable branch, Z3 version 4.15.4. The code is not public yet.

References

Prover Technology, “CENELEC is amending EN 50716 for AI. Here is what the draft says”, 16 September 2026. https://www.prover.com/company-news/cenelec-is-amending-en-50716-for-ai-here-is-what-the-draft-says/
E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997.
A. Biere, A. Cimatti, E. Clarke, Y. Zhu, “Symbolic Model Checking without BDDs”, TACAS 1999.
C. Flanagan, K. R. M. Leino, “Houdini, an Annotation Assistant for ESC/Java”, FME 2001.
L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, TACAS 2008.
W. McCune, Otter 3.3 Reference Manual, Argonne National Laboratory, 2003.