Formal verification in the loop

The family runs from the cheap to the ambitious. At the cheap end, a type that cannot be constructed unauthorized, required by every gated function, retires a whole class of time-of-check/time-of-use bugs that more tests kept failing to catch — once the type is enforcing it, the test is redundant. At the ambitious end sits generating code with machine-checkable guarantees, so vulnerability classes are eliminated by construction rather than detected instance by instance. In between: proof assistants grounding reasoning, and explicitly described causal models with an ontology, an uncertainty model, quantitative bounds, and formal verification inside those bounds rather than probabilistic confidence.

Two nearby moves make this practical rather than academic. Autoformalization translates informal artifacts into formal ones — and where no specification exists, it treats the input artifact as its own spec and checks the translation with a generated equivalence suite. The verifiable substrate generalizes the discipline: every claim must resolve to an executed artifact — a log line, a code path, a hardware run — with the substrate bootstrapped from verified reproductions rather than from model recall, which also defeats training-data contamination by construction.

The economic argument is that an attacker needs one hole and a defender must cover all of them, and detection-based defense loses that race at agent speed. With average patch deployment in some sectors close to 500 days, near-term capability gains favour the attacker; coding ability and cyber ability are two sides of one coin and cannot be separately suppressed. Security by construction is the only paradigm that changes the arithmetic.

Also: Lean, Isabelle, PutnamBench, Verina, Veriall, CyberGym, ExploitGym.

This is the field’s endorsement of Assay’s existing invariant canon: pure verification — invariant checks are closed-form mathematics, not runtime assertions. The principle behind it is exactly the one the proof-assistant and causal-model reports state: verification you can trust is verification that does not share the generator’s failure modes. Shipped as a rule; not mechanized — nothing in Assay checks that an invariant is closed-form, and no proof checker sits in the loop.

The AuthorizedRequest type is the canon stated as an agent-management technique rather than as a mathematical preference, and it is the cleanest citation to add to the methodology next time the defense-in-depth material is edited. The verifiable-substrate idea, meanwhile, is Assay’s evidence-row discipline generalized: every claim traceable to a log, a line of code or a run is exactly what the verify role demands of a brief’s Verify table. The contamination-defeating construction has no Assay analogue and is probably not needed at repo scale, but the framing is worth keeping.

For migration-style briefs, the source artifact can serve as the specification and a generated equivalence suite as the Verify rows — cheaper than hand-authoring expected behaviour for a legacy transformation, and the shape of the reported translation pipeline applied to brief authoring. Not designed. The attacker/defender asymmetry is also the arithmetic behind Assay’s guard posture: advisory client-side, binding server-side, with the standing publication checks as the defender that has to cover everything. Verify rows are the lightweight per-brief step on the road to provable guarantees, and Assay claims nothing beyond that.

• Status is held at corroborated deliberately: the sources converge, but almost all of the evidence is benchmark- or research-stage.
• What would move it to established is a first-hand account of formal verification running inside a production agent loop — not a benchmark score, but a team saying “our agents’ output goes through a proof checker before merge, here is the pass rate and the cost.”
• Whether repo-scale verifiable-code-generation numbers hold up on real codebases, and whether autoformalization holds its small-model advantage as frontier models improve.