AI verification is shifting from model judges to proof-carrying outputs

LLM-as-judge systems are useful because they cover domains where formal tools do not. Their weakness is architectural: the judge is another probabilistic model with many of the same failure modes as the generator. A scalar score can look authoritative while hiding which premise failed, whether a citation exists, or whether the judge accepted a polished but invalid step.

The newer verification systems do something narrower but stronger. They translate all or part of the candidate into a representation with explicit semantics, then ask a proof kernel, compiler, SMT solver, symbolic executor or structured transition checker to validate the result. The generator can remain probabilistic. The correctness boundary does not have to be.

This is why the phrase proof-carrying output is useful even outside theorem proving. The output is accompanied by enough structure that a separate mechanism can reject an invalid dependency, arithmetic expression, state transition or program property without trusting the original model.

Theoria rewrites an informal solution into a sequence of typed reasoning states. Every change between adjacent states must be licensed by a citation, computation, problem fact or another explicit justification. Its core invariant is simple: no material change is allowed to appear from nowhere.

That architecture is important because hidden premises are a recurring failure mode in fluent reasoning. A holistic judge may accept the overall story. A transition checker can instead ask why one expression, fact or conclusion changed between states. The paper reports that this structure was especially useful against hidden premises and fabricated citations in its adversarial evaluation.

The broader engineering lesson is not that Theoria solves verification. It is that verification improves when reasoning is transformed from a monolithic paragraph into inspectable transitions with local obligations.

VeryTrace formalizes reasoning traces into a domain-specific language that makes dependencies explicit and turns quantitative content into executable expressions. Deterministic checks handle computations, dependency resolution and constraints, while residual semantic judgments are sent to targeted model audits.

This hybrid design is more realistic than pretending every useful answer can be fully formalized. The verified part and the judgment-dependent part are separated. When an error occurs, the system can localize the failed step and attempt repair rather than merely declaring the whole answer low confidence.

A production analogue would resemble a compiler pipeline: parse the model output, lower it into a typed intermediate form, run strong passes where semantics are available, and keep unsupported claims visible as unresolved obligations.

VeriSynth is a clear example of the division of labor. It uses an LLM to translate zkEVM implementation code into symbolic verification models, but an SMT solver determines whether the resulting constraints expose semantic faults. The model is not asked to certify its own translation.

That pattern is attractive because specification has historically been one of the expensive parts of formal methods. LLMs can reduce the cost of writing invariants, proof skeletons and symbolic models, while a smaller trusted computing base still checks whether the artifact satisfies the formal rules.

The danger moves upstream: if the generated specification omits the real requirement, the solver can prove the wrong thing perfectly. Verification pipelines therefore need specification mutation, counterexample generation and independent adequacy tests, not only successful solver termination.

LEAP uses a general-purpose foundation model in an agentic loop with Lean, decomposing a problem, proposing formal proof steps and refining them against compiler feedback. Pythagoras-Prover attacks the same space from a compute-efficiency angle with verified Lean corpora and smaller prover models.

The significance is not a single benchmark number. Formal proof languages create a cheap, exact success signal once the theorem has been stated correctly. That allows search, self-repair and training to use feedback that is much harder to obtain in open-ended prose.

OpenAI’s First Proof exercise also illustrates the boundary. Informal research proofs can be impressive and still require expert scrutiny. A later correction to one attempted proof is a reminder that polished long-form reasoning and verified correctness remain different things.

Fully formal proofs are mechanically checkable but expensive to produce, especially for frontier mathematics and loosely specified technical reasoning. Pure natural language is flexible but difficult to audit reliably. Pseudo-Formalization proposes a middle layer: decompose a proof into modules with explicit premises, conclusions and local justifications, then verify those blocks independently.

This middle layer matters beyond mathematics. A security analysis, incident report or engineering decision can often be decomposed into claims whose inputs and transformations are explicit even when the complete document cannot be encoded in Lean or SMT.

The right architecture may therefore be graduated verification rather than one universal checker: deterministic arithmetic and constraints where possible, typed structured claims next, targeted model judgment where necessary, and human review for the residual high-impact uncertainty.

Industrial formal verification has traditionally been constrained by expert labor. Work on AutoReal and IsabeLLM targets real verification projects rather than toy math alone, including seL4-style theorem proving and consensus verification. The common bet is that models can automate proof search, context retrieval, annotation generation and repair while established proof assistants preserve the final correctness boundary.

If that pattern holds, formal methods do not become less strict. They become cheaper to apply because part of the specification and proof labor is automated. This could expand verification from a small set of safety-critical systems into more security-sensitive libraries, protocols and generated software.

The economic question is therefore cost per mechanically verified property, not tokens per proof attempt. Tooling that produces more candidate proofs but requires more human rescue may still be uneconomic compared with a smaller model paired with better project context and compiler feedback.

Formal verification never proves that software is “correct” in the abstract. It proves that an implementation satisfies a stated property under a model. A malicious or careless generator can exploit this by weakening a postcondition, omitting an edge case, changing an assumption or constructing a vacuous theorem that is easy to prove.

This is especially important for AI-generated specifications because fluent models can produce contracts that look rigorous to a reviewer. The defense is adversarial specification testing: mutate implementations, search for counterexamples, compare against independent properties, pin environmental assumptions and reject proofs whose guarantees are weaker than the original requirement.

For production systems, specification provenance should be as carefully versioned as source code. A verified artifact without the exact property version, solver version and assumptions is difficult to audit later.

The strongest reason to separate generator and checker is security. A frontier model, retrieval layer, agent harness and prompt are all large mutable systems. A proof kernel or SMT solver can often be much smaller and more deterministic.

That does not make the pipeline invulnerable. Solvers have bugs, formalizations can be wrong, generated code can exploit undefined behavior, and tool interfaces can be manipulated. But a small checker gives defenders a narrower component to harden, version and independently test.

For high-impact actions, the safest pattern is capability gating: the model may propose a transaction, code change or configuration, but execution requires a machine-checkable certificate that specific policy predicates are satisfied. The certificate should be tied to the exact artifact being executed.

The next stage of this trend will be determined by coverage. Formal systems are powerful precisely because their semantics are narrow. If the cost of translating real work into those semantics remains high, proof-carrying AI will stay concentrated in mathematics, code and bounded decision systems.

Watch for better auto-formalization, stronger specification adequacy tests, domain-specific intermediate languages, solver-backed code agents, and evaluation that reports false certification rather than only solve rate. Also watch how often systems can abstain cleanly when a claim cannot be mechanized.

The most important production signal will be whether teams can make independent re-verification routine. A useful proof artifact should survive model upgrades, prompt changes and organizational handoffs because correctness is encoded in something more durable than the original model conversation.