Formal verification tools are often compared as though they were competing implementations of the same idea. They are not. The most important difference is usually not the search algorithm or the input syntax. It is the shape of the question the tool is designed to answer.

An SMT solver asks a particularly useful question:

Can all of these logical constraints be true at the same time?

That question is narrow enough to support formidable automation and broad enough to cover a large part of software and hardware verification. Arithmetic, arrays, bit-vectors, algebraic data types, strings, and uninterpreted functions can all appear in solver obligations. The result is a workhorse technology: SMT solvers sit behind symbolic execution, bounded model checking, deductive program verifiers, synthesis tools, proof assistants, and many domain-specific verification systems.

This first post develops a mental map for that role. The point is not that SMT is weak. The point is that its strength comes from a deliberate bargain: shape the verification problem as satisfiability, and receive extremely strong automation in return.

A proof assistant makes a different bargain. It provides a much more general language for defining the system, its semantics, and the theorem we actually want. The price is that more of the proof structure must be supplied. Increasingly, AI systems can help construct that structure while the proof assistant checks the result.

A running example: a small safety controller

We will use one system throughout this series.

Imagine a controller that receives commands and drives a physical actuator. Its state contains:

• an operating mode such as idle, armed, running, or fault;
• a bounded command queue;
• permission and interlock bits;
• a watchdog counter;
• an audit record.

A transition applies one controller rule: accept a command, start an operation, acknowledge completion, refresh a watchdog, reject an unauthorized request, or enter recovery.

A central safety invariant might say:

The actuator is enabled only when the controller is armed, the current command is authorized, and every required interlock is closed.

This is an excellent SMT problem.

The native SMT workflow

Suppose Safe(s) means that state s satisfies the invariant, and Step(s, s') means that the controller can move from s to s' in one valid transition.

To search for a transition that breaks the invariant, a verifier can ask whether this formula is satisfiable:

Safe(s)
and Step(s, s')
and not Safe(s')

If the answer is SAT, the solver can usually provide values for s and s'. Those values form a concrete counterexample: a safe state and one allowed step leading to an unsafe state.

If the answer is UNSAT, no such transition exists within the encoded model. The invariant is preserved by one step.

This pattern scales surprisingly far. A tool can encode:

• integer bounds on the queue;
• bit-vector behavior of registers;
• array reads and writes;
• permission maps;
• relationships among several program variables;
• the conditions under which each transition rule is enabled.

SMT-LIB standardizes the language in which many such problems are exchanged. Its current Version 2.7 separates the underlying logic, background theories, accepted formula fragments, and solver interface—an important reminder that “SMT” is not one monolithic logic.¹

Mental model: An SMT solver is not primarily exploring a story about the system. It is deciding whether a precisely constructed logical situation has a model.

The restriction is part of the product

It is tempting to describe a restricted logic as a deficiency. In automated reasoning, restriction is usually the source of leverage.

A solver can exploit specialized decision procedures for linear arithmetic, bit-vectors, arrays, or combinations of theories. It can learn clauses, propagate equalities, build candidate models, and produce compact counterexamples. A verification tool can generate thousands of obligations and rely on the solver to close most of them without human attention.

The result is an attractive division of labor:

1. The front end translates a program or model into logical obligations.
2. The SMT solver handles the obligations that fit its supported fragments.
3. The front end interprets SAT, UNSAT, models, and sometimes proofs.

This explains why SMT is embedded in so many other tools. It is often more useful as a high-performance reasoning engine than as the top-level language in which the complete correctness argument is expressed.

Where the one-step question stops

Now consider a different property of the controller.

Two housekeeping rules may be enabled at the same time. One refreshes the watchdog. The other records an audit event. The scheduler may choose either rule first.

We would like to know:

Whenever execution splits because two rules are possible, can the resulting branches eventually reach a common controller state?

This is an instance of confluence, or reconvergence. In abstract form:

• start in a state a;
• reach b by zero or more steps;
• reach c by zero or more steps;
• require some state d reachable from both b and c.

The difficult phrase is not “common state.” It is zero or more steps, with no fixed bound.

A first-order formula can mention the one-step relation Step. It cannot, in general, define the reflexive-transitive closure of an arbitrary relation. The problem is not solved by writing a longer first-order formula: any fixed formula has finite syntactic depth, while reachability may require arbitrarily many transitions.

There is a particularly strong result for confluence. Over a bare signature containing equality and a one-step rewrite relation, confluence is not first-order definable—even by an arbitrary set of first-order sentences.²

That statement is precise, but it is easy to overstate. It does not mean:

• no SMT-based tool can reason about confluence;
• no finite transition system can be encoded for an SMT solver;
• no solver extension can support recursive predicates or fixed points;
• no bounded counterexample can be found;
• no local confluence condition can be discharged by SMT.

All of those may be possible. A front end can unroll paths to a chosen depth, introduce auxiliary reachability predicates, use constrained Horn clauses, generate induction obligations, or encode a finite graph with explicit state identifiers.

The narrower and defensible claim is:

Confluence is not a native first-order property of an arbitrary one-step relation on the original model. An SMT-based workflow must add an encoding, a bound, an invariant, a recursion mechanism, or a surrounding proof argument.

A necessary scope note

SMT itself continues to evolve. SMT-LIB 2.7 adds map sorts and lambda syntax while keeping its underlying logic nominally first-order, and a preliminary SMT-LIB 3 proposal moves toward a higher-order foundation with dependent types.³

For that reason, claims such as “SMT cannot express X” are usually too broad. The useful comparison is between a specific native input problem and the larger semantic theorem a verification effort needs.

What changes in a proof assistant

A proof assistant begins one level above the solver obligation.

Instead of starting with a formula about unnamed values, we define the mathematical objects involved. In pseudocode—not the syntax of any one system—we might introduce:

State : a type
Step  : a relation between states

We then define finite reachability inductively:

Every state reaches itself.
If s reaches t and t takes one step to u,
then s reaches u.

Once reachability exists as a definition, confluence becomes a direct proposition:

For every a, b, and c,
if a reaches b and a reaches c,
then there exists d such that
b reaches d and c reaches d.

Nothing in this statement assumes that the state space is finite or that the joining paths have a predetermined length. The property is simply part of the formal language.

That does not make the proof automatic. The user may still need to establish that:

• independent rules commute;
• critical rule pairs can be joined;
• a measure decreases;
• the system terminates;
• a generic theorem such as Newman’s lemma applies.

The advantage is prior to automation: the complete claim is representable, and its proof can be decomposed according to its mathematical structure.

The small amount of type theory you need for the mental map

Agda, Lean, and Rocq are not identical systems. Agda explicitly describes itself as an extension of Martin-Löf type theory; Lean is based on a version of dependent type theory in the Calculus of Constructions family with inductive types; Rocq uses the Calculus of Inductive Constructions.⁴⁵⁶

They nevertheless share a useful conceptual tradition:

Types describe objects

There may be a type of controller states, a type of commands, and a type of finite execution paths.

Claims have formal types

A claim such as “s reaches t” is represented inside the system. A proof is an object accepted as evidence for that claim.

Inductive definitions describe finite derivations

Reachability is not introduced as an unexplained oracle. It is built from two cases: a zero-step path and the extension of an existing path by one transition.

Proofs compose

A proof that a local rule pair reconverges can become an input to a larger theorem about all executions. A solver result about arithmetic can become one premise of that local proof.

This is the practical meaning of “propositions as types” for our discussion. It is not necessary to learn tactic syntax to understand the architectural difference.

The proof assistant is an envelope, not a replacement solver

The most productive design is often hybrid.

Inside the proof assistant, we may define:

• the controller state;
• the transition relation;
• reachability;
• the safety invariant;
• confluence;
• assumptions about the environment.

Then specialized automation can solve the subproblems it handles well:

• SMT proves arithmetic side conditions;
• a decision procedure handles finite data;
• simplification normalizes definitions;
• a model checker establishes a finite-state lemma;
• a human or AI assistant proposes the global proof structure.

The final theorem is not “the SMT solver returned UNSAT.” It is closer to:

Under these explicit assumptions, every execution of this defined controller preserves the safety invariant, and independent scheduling choices reconverge.

The UNSAT result may be an important step in that theorem. It is no longer the entire semantic context.

Why LLM-assisted proving changes the economics

Proof assistants have historically imposed a substantial labor cost. The difficulty is not only discovering deep arguments. It is also formal work that experts perform repeatedly:

• translating an informal model into precise definitions;
• finding the right library lemma;
• stating intermediate invariants;
• selecting an induction principle;
• filling routine proof steps;
• repairing proofs after definitions change.

Language models are well suited to proposing this kind of structured text. More importantly, a proof assistant supplies a precise feedback loop. A candidate proof is parsed, elaborated, and checked. Incorrect steps do not become correct because they sound persuasive.

AlphaProof is a prominent example of this pattern: it searches for formal proofs by interacting with a verifiable environment based on Lean.⁷ The important architectural lesson is broader than any one benchmark:

The generative system proposes; the proof assistant checks.

This does not remove the hard parts.

An LLM may formalize the wrong property, use assumptions that are too strong, or choose a model that does not match the deployed controller. Type checking verifies that a theorem follows from the formal definitions. It does not prove that those definitions are the right account of reality.

Still, the verification loop changes what is economically plausible. Proof assistants become less dependent on every line being authored manually by a specialist. They become candidates for work that previously stopped at isolated checker runs because the semantic “glue” was too expensive to construct.

The mental map after Part 1

An SMT solver and a proof assistant occupy different levels.

The practical conclusion is not “use a proof assistant instead of SMT.” It is:

Use SMT for the sharply defined obligations it solves exceptionally well. Use a proof assistant when the assurance claim must quantify over the semantics, combine several forms of evidence, or state a theorem that is larger than the solver’s native question.

Part 2 moves from constraints to time. CTL and LTL model checkers make whole executions visible—but even a temporal view does not expose every relationship among executions.

Sources and further reading