Overview
AI coding agents can generate software much faster than human reviewers can inspect it, creating an assurance gap that probabilistic model judgments and input-sampling tests cannot completely close. The speaker presents formal verification as a way to prove that an implementation satisfies an explicit specification for every possible input. In the proposed specification-driven workflow, a human writes or reviews the definition of correctness, an AI agent implements it, and a verification system constructs a proof that a small trusted kernel independently checks. Lean supports this approach by expressing programs, definitions, and proofs in one extensible language. Its interactive tactics resemble moves through a chess search tree, while automated solvers such as Z3 behave more like calculators that decide whether formulas are satisfiable. The talk illustrates several integration patterns: implementing both specification and code in Lean, modeling Rust software in Lean and comparing behavior through differential testing, annotating Rust for deductive verification with Verus, translating Rust into Lean with Aeneas, and lowering multiple languages into Strata Core for dispatch to proof engines, SMT solvers, or model checkers. The central conclusion is that specifications must remain human-validated, living artifacts because proof only establishes compliance with the stated specification—not that the specification itself captures the right behavior.
Sections
Core Concepts
Terms used to explain specification-driven formal verification.
- Formal verification: the use of mathematical proof to establish that code satisfies a stated specification for every possible input.
- Specification: an explicit definition of what correct behavior means; it is the upstream artifact against which an implementation is verified.
- Lean: a programming language and proof assistant in which definitions, programs, and proofs can be expressed without an additional translation layer.
- Tactic: an interactive proof operation that advances, decomposes, or attempts to solve a theorem goal.
- Trusted kernel: the small component that independently checks whether a constructed proof is valid.
- Solver: an automated engine that receives a logical formula and returns a result such as satisfiable or unsatisfiable.
- Precondition and postcondition: statements describing what must be true before code executes and what must be true afterward.
- Ghost code: verification-only annotations or logic that are checked statically and erased from the runtime program.
Strategic Implications
Higher-level conclusions derived from the proposed workflow and examples.
- As implementation becomes cheaper through AI, precise specification becomes the new bottleneck and the highest-leverage point for human attention.
- Formal verification does not remove probabilistic AI from development; it places a deterministic checking boundary around AI-generated code and proofs.
- The strongest practical systems may combine deductive proof, executable reference models, and large-scale differential testing instead of treating them as competing techniques.
- A common verification intermediate representation could give formal methods an ecosystem role similar to compiler infrastructure, allowing many source languages to share analysis engines.
Tools and Architectures
Concrete implementation patterns and technologies discussed in the talk.
- A Lean theorem proves that reversing the concatenation of lists A and B equals the reverse of B concatenated with the reverse of A for every input.
- The AI-assisted zlib conversion used a natural-language specification, formalized it, generated Lean code and helper lemmas, and produced approximately 32,000 lines of proof.
- Cedar maintains its functional specification in Lean and its production authorization implementation in Rust, with approximately 100 million differential random tests run nightly.
- Verus embeds requires and ensures annotations in Rust, uses the Z3 SMT solver for static verification, and erases verification-only material at runtime.
- Aeneas uses Rust's mid-level intermediate representation to perform a functional translation into Lean for theorem proving.
- Strata lowers language-specific dialects into Strata Core, then dispatches the common representation to Lean, SMT solvers, or model checkers.
Limitations and Failure Modes
Conditions that can undermine or overstate the value of a successful proof.
- An implementation can be perfectly verified against a specification that is incomplete, mistranslated, or behaviorally wrong.
- AI auto-formalization can introduce a semantic gap between a natural-language requirement and the formal property actually proved.
- A proof covers only the properties stated in the specification; unstated security, performance, integration, or operational requirements remain outside its guarantee.
- Large proofs can require substantial decomposition and tooling effort, as illustrated by the 32,000-line zlib proof example.
- Strata is described as work in progress, so its proposed language-independent workflow should not be treated as a mature universal solution.
Recommended Adoption Path
Concrete steps for introducing formal verification into AI-assisted development.
- Select a small piece of critical code with a property whose correctness can be stated precisely.
- Write the intended behavior as a formal specification or begin with natural language and use AI to produce a formal candidate.
- Validate the specification through human review and representative input checks before generating the implementation.
- Choose an integration model suited to the codebase: native Lean, a Lean reference model with differential testing, Rust annotations with Verus, Rust translation with Aeneas, or another supported verification path.
- Let the coding agent implement from the validated specification and construct lemmas and proofs, then require acceptance by a trusted kernel.
- Keep the specification under active maintenance as requirements and implementations evolve.