Formal Verification for AI-Generated Code

The Specification-Proof Workflow

Formal verification provides a mathematical guarantee that code satisfies a specification for every possible input. The workflow relies on a division of labor where humans define the specification—the definition of correctness—and machines generate the code and the corresponding proof. Because the specification is the upstream source of truth, it must be validated by humans or tested against inputs before any downstream implementation occurs. This approach addresses the limitations of probabilistic AI code grading and non-scalable human code reviews.

Lean 4 as a Proof Assistant

Lean 4 serves as both a programming language and a proof assistant, allowing code and proofs to coexist in the same environment without a translation layer. The process functions like a game of chess: the developer uses tactics as moves to traverse a tree of sub-goals, attempting to reach a final theorem (checkmate). If a branch fails, the system backtracks to try a different path. Once the proof is complete, a small, independent, and open-source kernel verifies the result. This kernel is minimal enough to be independently audited or reimplemented in languages like C++ or Rust to ensure trust.

Production Integration

Practical applications of this methodology include:

• Direct Formalization: Using AI to decompose complex libraries into lemmas and proofs, as demonstrated by the conversion of the zlib compression library into 32,000 lines of Lean proof.
• Differential Testing: For systems like Cedar, the authorization policy language used by AWS, the functional specification is written in Lean while the production code runs in Rust. The two are reconciled nightly through approximately 100 million differential random tests to ensure they produce identical outputs.
• Static Verification: Tools like Varys use SMT solvers (such as Z3) to enforce pre-conditions and post-conditions on code. These annotations are checked statically and erased at runtime, acting as ghost code that ensures correctness without impacting performance.
• Strata: An ongoing project that allows developers to create language-specific dialects that lower code into a common intermediate representation, enabling it to be dispatched to various verification engines including Lean, SMT solvers, or model checkers.