The first two posts examined formula-centered verification.

An SMT solver asks whether a set of constraints is satisfiable. A CTL or LTL model checker asks whether a transition system satisfies a temporal property.

Refinement and equivalence checkers introduce a different shape of question:

Does this model behave like that model?

That change matters because a specification can now be executable. Instead of describing the required controller with a collection of formulas, we can build a small abstract controller and compare the detailed implementation with it.

This is the natural language of abstraction. The concrete model contains queues, retries, scheduler choices, hardware handshakes, and bookkeeping. The abstract model says only what the environment is supposed to observe.

A refinement check can establish that the detail does not introduce forbidden behavior. An equivalence check can establish that two descriptions are interchangeable under a chosen view.

The phrase chosen view is central. There is no single universal meaning of “behaves like.” Every behavioral relation preserves some distinctions and deliberately ignores others.

A proof assistant makes that choice explicit. It can define the models, the comparison relation, the properties we care about, and the theorem connecting them. This is the step that turns isolated checker results into a hierarchy of assurance.

The controller at two levels

Return to our safety controller.

The abstract service has a small interface:

receive an authorized request
perform the requested operation
report completion or a defined failure

The concrete controller is far more detailed:

• requests enter a bounded queue;
• a scheduler selects work;
• interlocks are checked more than once;
• watchdog timers can trigger retries;
• hardware acknowledgements arrive asynchronously;
• audit records are written;
• internal recovery steps may be invisible to the caller.

The two models are not expected to have the same number of states or the same internal transitions. That is the point of abstraction.

A refinement assertion asks whether every relevant behavior of the concrete model is permitted by the abstract one. Notation varies across formalisms, but we can write the idea as:

Concrete refines Abstract

or schematically:

C ≼ A

If the check fails, a tool may return a distinguishing behavior: a trace the implementation can perform but the specification cannot, a refusal that violates the selected failures model, an unmatched transition, or a divergence that the specification did not permit.

FDR, for example, compares CSP processes in traces, failures, and failures-divergences models and reports counterexamples according to the selected semantics.¹ The mCRL2 toolset can compare labelled transition systems using trace, simulation, bisimulation, and related equivalences and preorders.²

These tools do not merely implement different algorithms for one fixed notion of correctness. They offer different meanings of behavioral comparison.

An abstraction relation is an observation lens

Consider four possible comparison lenses.

Trace comparison

Two systems are compared by the visible action sequences they can perform.

This is useful when the externally visible protocol is what matters. It may ignore where a choice was made or how many internal states support the same sequence.

Failures-style comparison

The comparison also observes which actions a process may refuse after a trace.

This can reveal deadlock and availability distinctions that plain trace comparison misses.

Bisimulation

The systems must match each other’s actions step by step, with successor states remaining related.

This preserves branching structure more closely than trace equivalence, but it still treats related states as behaviorally interchangeable rather than requiring them to be the same state.

Isomorphism

The transition graphs must have the same structure up to a one-to-one renaming of states.

This preserves far more detail and therefore supports less abstraction.

This left-to-right ordering is an intuition for the untimed examples shown, not a universal lattice across every refinement formalism. Failures, weak and branching relations, probabilistic models, timed systems, and divergence-sensitive semantics introduce additional axes.

The mCRL2 documentation gives a useful ordering intuition: trace equivalence preserves action sequences, bisimilarity also preserves branching structure, and isomorphism requires the transition structures to match up to a bijection.³

No lens is simply “best.” A coarser relation can hide irrelevant detail and dramatically reduce a state space. A finer relation can preserve a property that the coarser relation forgets.

Mental model: A refinement result is always relative to a selected meaning of observable behavior.

Passing a check does not preserve every property

Suppose we establish:

Concrete ≼ Abstract

Can we now prove every property of Abstract for Concrete?

No. We can transfer only properties preserved by the chosen relation.

The general reasoning pattern is:

1. the concrete model is related to the abstract model;
2. the abstract model has property P;
3. the relation preserves property P;
4. therefore the concrete model has property P.

Step 3 is easy to overlook because it is often built into the theory behind a checker. For example, a particular equivalence may be known to preserve a particular modal logic. But the preservation result has hypotheses and a scope. It is not a universal promise that every fact about one graph remains true of the other.

Our recurring reconvergence property makes this visible.

Behavioral sameness is not literal reconvergence

Part 2 introduced two small systems:

• a joined system, where two branches later reach the same state;
• a split system, where the branches reach separate states with identical labels and future actions.

The systems have the same traces and can be strongly bisimilar. From the chosen behavioral viewpoint, each move in one can be matched by the other.

But only the joined system is confluent in the literal graph-theoretic sense:

Whenever two executions start from one state, their endpoints can later reach a common state.

In the split system, the two branches never share a descendant. The states merely behave alike.

This gives a compact preservation test:

• the relation considers the two systems equivalent;
• confluence is true of one and false of the other;
• therefore confluence is not invariant under that relation.

A trace-equivalence or strong-bisimulation result cannot, by itself, transfer literal confluence. The relation has abstracted away exactly the state-identity distinction on which the property depends.

That is not a bug in bisimulation. It is a reminder to match the abstraction to the theorem.

A stronger or different relation could preserve the distinction. Isomorphism would. A custom confluence-aware relation might. A model could expose state identity as an observation. Each choice changes what the comparison means.

The accurate conclusion is:

A behavioral checker can establish only what its selected semantics observes or what has separately been proved to follow from that semantics.

The same expressibility caveat applies here

As in the previous posts, we are discussing the native comparison on the original models.

A toolchain may transform the models, add observers, retain histories, attach costs, reveal internal actions, or select a richer relation. It may reduce a property to a refinement assertion against a generated specification.

Those transformations can be effective. They also contribute semantic content.

It would therefore be too broad to say “refinement checkers cannot express confluence.” A defensible statement is:

Ordinary trace- and bisimulation-based comparison does not preserve literal confluence, so confluence cannot be recovered from those equivalence classes alone.

This formulation says exactly where the boundary lies. It does not deny the power of preprocessing, custom semantics, or a dedicated confluence checker.

A proof assistant can reason about the lens

A proof assistant is not forced to select one behavioral relation as the final notion of correctness.

It can define several things in one context:

ConcreteModel
AbstractModel
RefinementRelation
SafetyProperty
TemporalProperty
ConfluenceProperty

It can then state separate theorems:

ConcreteModel refines AbstractModel under R.

AbstractModel satisfies the service property.

R preserves the service property.

R does not necessarily preserve literal confluence.

ConcreteModel is confluent for an independent reason.

This is a substantial shift in perspective.

In a checker, the comparison relation is usually part of the verification mode. In a proof assistant, the relation can also be an object of reasoning. We can prove that it is reflexive or transitive, prove that two relations compose, and prove exactly which properties survive abstraction.

The proof assistant does not make those theorems automatic. It makes them stateable, reusable, and checkable in the same foundational language.

The small amount of dependent type theory needed here

The final conceptual step in this series is that models and relations can themselves be treated as typed objects.

A model can be packaged with:

• its state type;
• its initial states;
• its transition relation;
• its visible observations;
• assumptions such as determinism or input enabledness.

A property is something that can be applied to a model. A refinement relation can be applied to two models. A preservation theorem can quantify over all models and all properties satisfying stated conditions.

In informal pseudocode:

For every concrete model C,
for every abstract model A,
for every relation R,
for every property P,
if C is related to A by R,
and A has P,
and R preserves P,
then C has P.

This is the practical role of higher-order and dependent typing in the mental map. The theorem does not concern only one controller. It describes a reusable pattern across models, relations, and properties.

Agda, Lean, and Rocq implement different type theories and proof environments, but they share the broad dependent-type-theoretic tradition needed for this pattern:

• types can describe structured mathematical objects;
• propositions are represented inside the language;
• proofs are checked terms;
• structures can package data with laws;
• general theorems can quantify over those structures.

The reader does not need tactic syntax or universe theory to understand the consequence: the framework can talk about the verification methods, not only about the system being verified.

From checker outputs to an assurance hierarchy

Now we can assemble the three tool families.

An SMT-based analysis may establish a data invariant:

Queue indices remain in range, permission checks cannot be bypassed, and bit-vector updates preserve the interlock encoding.

A temporal model checker may establish a behavioral result:

Every accepted command eventually completes or enters a defined recovery state, under an explicit fairness assumption.

A refinement checker may establish an abstraction result:

The detailed controller implements the abstract request–completion service under the selected failures or bisimulation semantics.

A proof assistant can place those facts in one semantic context and prove an end-to-end theorem:

Under the stated hardware and scheduler assumptions, the concrete controller cannot issue an unsafe actuator command.

The key word is connecting.

A directory containing three successful tool runs is not yet one proof. The models may use different state spaces, abstractions, naming conventions, and environment assumptions. The temporal property may have been checked on an abstract model. The SMT invariant may concern an implementation-level state. The refinement relation may hide events relevant to safety.

A proof assistant can host the bridge theorems:

• the implementation state maps to the abstract state;
• the SMT invariant makes that mapping well defined;
• the refinement relation preserves the temporal guarantee;
• the environment assumptions used by each result are compatible;
• the combined facts imply the final safety theorem.

This is why semantic integration layer is a useful description. The proof assistant is not merely a dashboard for pass/fail signals. It contains definitions and proofs explaining how the signals relate.

Hierarchical verification becomes explicit

Large systems are rarely verified at one level.

A realistic hierarchy may include:

1. machine-word and memory invariants;
2. component transition systems;
3. protocol-level temporal properties;
4. subsystem refinement relations;
5. architectural assumptions;
6. a top-level hazard or safety theorem.

Each layer hides detail from the next. Each hiding step needs a preservation argument.

Proof assistants are well suited to representing this hierarchy because theorem conclusions can become premises of later theorems. A component proof can be reused without replaying its human rationale. A generic preservation result can be instantiated many times. An abstract theorem can be transferred through a chain of refinements when the required conditions have been proved.

This does not eliminate state explosion or make all verification scalable. It changes what can be composed once specialized tools have solved their local problems.

The result is not one giant monolithic proof attempt. It is a network of definitions and checked claims, with automation applied at the levels where it is effective.

External checker results still need a trust story

There is an important qualification.

A proof assistant does not make an external result trustworthy merely by naming it. The final context must account for how that result enters the proof.

Possible approaches include:

• checking a proof or certificate produced by the external tool;
• reconstructing the result with trusted proof-producing procedures;
• verifying the checker or a small result checker;
• or recording the result explicitly as an assumption.

These approaches have different engineering costs and trust bases. This series is about the conceptual architecture rather than the integration mechanisms, but the distinction cannot be skipped.

The Rocq documentation illustrates the underlying trust model clearly: tactics construct proof terms, and the kernel checks that the final term has the theorem’s type. This separation allows complex automation to remain outside the small core that validates the result.⁴

The same principle motivates LLM-assisted proof development.

Where LLMs may have the largest effect

In a hierarchical assurance argument, much of the cost lies in the glue:

• aligning two state representations;
• discovering an abstraction relation;
• finding which preservation theorem applies;
• restating a result at the correct level;
• generating routine cases for many transition rules;
• repairing proof scripts after a model changes;
• navigating large libraries of existing lemmas.

These tasks combine repetitive formal work with contextual judgment. They are plausible targets for LLM assistance.

Recent formal-proving systems do not rely on one perfect proof emitted in a single pass. They decompose goals, generate intermediate lemmas, interact with a formal checker, and revise failed attempts. AlphaProof demonstrated reinforcement-learning-based formal proof search in a Lean environment, while the 2026 LEAP preprint emphasizes agentic decomposition and continuous interaction with the Lean compiler.⁵⁶

The safe architectural slogan remains:

The LLM proposes. The proof assistant checks.

That slogan should not be confused with a claim that formalization is solved.

An accepted proof can still establish the wrong theorem if the original requirement was mistranslated. A model can omit a physical failure mode. An abstraction relation can assume away the behavior that matters. An imported result can have a larger trust base than expected.

LLMs primarily change the cost of constructing and maintaining the formal argument. They do not choose the correct assurance boundary automatically, and they do not replace model validation or engineering judgment.

The completed mental map

The categories overlap in practice. SMT solvers power model checkers. Model checkers can produce certificates. Refinement can be encoded as a temporal or fixed-point problem. Proof assistants contain decision procedures and invoke external automation.

The table is not a taxonomy of mutually exclusive software products. It is a map of native questions and engineering trade-offs.

Beyond the checker

The strategic case for proof assistants is not that every specialist checker should be replaced by a general theorem prover.

It is that modern verification needs a place where the meanings of many specialist results can meet.

A proof assistant can provide that place:

• a common language for models and semantics;
• explicit assumptions at every abstraction level;
• reusable preservation theorems;
• mechanically checked composition of results;
• and a foundation on which LLMs can generate proof candidates without becoming trusted authorities.

This suggests a layered future for formal verification:

specialized automation below
expressive semantic composition above

SMT solvers continue to solve constraints. Temporal model checkers continue to explore behavior. Refinement checkers continue to compare abstractions. Proof assistants connect those results into arguments that no one checker was designed to express alone.

That is the larger opportunity: not a more elaborate pass/fail tool, but a framework for hierarchical, cross-model safety reasoning.

Sources and further reading