# Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

## Executive summary

As AI coding agents generate massive amounts of code, traditional checks (probabilistic model grading, input-limited tests, human review) are insufficient to guarantee correctness for all inputs. Formal verification provides mathematical proof that code satisfies a precise specification. The methodology involves humans owning the specification and machines handling both the implementation and the formal proof. Tools like Lean allow the same language for defining code and proofs, enabling robust systems where production code (e.g., Rust) is reconciled against specifications written in Lean, often through differential random testing.

## Key takeaways

- Limitations of Current Code Checks: None of the usual checks—AI model grading (probabilistic), unit tests (limited inputs), or human review (non-scalable)—can guarantee that code is correct for every possible input. Formal verification provides mathematical proof of correctness for all inputs.
- The Specification Hierarchy: In formal verification, humans own the specification (what 'correct' means). This specification must be validated first because it is the upstream artifact; everything else (code and proof) is downstream from it. The AI coding agent then implements code based on this spec.
- Lean as a Unified Language: Lean functions as both a programming language and a proof assistant, eliminating translation layers. It allows the same language to define definitions (code) and proofs (theorems).

## Technical details

- Formal Verification Process: The process requires defining a specification (formally in Lean or naturally for AI auto-formalization), validating that spec, having the AI generate code from it, and finally using the formal verification tool to prove the implementation matches the specification. The proof is constructed using 'tactics' (moves) which are assembled into a final theorem (checkmate).
- Lean Architecture: Lean utilizes a small trusted kernel that independently checks proofs, ensuring integrity even if incorrect proofs are attempted. Proofs can be exported and checked by multiple independent kernels (available in C++, Rust, Lean).
- Industry Applications (Cedar/Rust): AWS uses Cedar, an open-source authorization policy language, where the functional specification is written in Lean. The production code runs in Rust. Consistency is maintained by running approximately 100 million differential random tests nightly; nothing ships until this agreement is reached.
- Solvers and Pre/Post Conditions: Tools like Verus use powerful solvers (e.g., Z3) to perform static checks, enforcing pre-conditions (what must be true before execution) and post-conditions (what must be true after execution). These checks are enforced by the verifier but erased at runtime.

## Practical implications

- Build engineers can significantly increase system reliability by integrating formal verification into the CI/CD pipeline.
- The separation of concerns—human owning specification, machine owning code and proof—allows for scalable quality assurance in agent-driven development.
- Using tools like Lean allows critical components to be verified mathematically against their intended behavior, moving beyond probabilistic testing.

## Topics

Formal Verification, Lean Programming Language, Software Reliability, AI Engineering, Build Systems, Lean, Cedar, Z3

Source: https://www.youtube.com/watch?v=lRa9sPaMyy4