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

Formal verification moves a crucial engineering question into the specification: what, exactly, must the program satisfy? A conference presentation from Amazon Web Services describes having machines produce code and mathematical proofs while humans remain responsible for the requirements. Lean's small proof-checking kernel checks whether the submitted argument establishes the stated proposition.

The Cedar example shows how this can coexist with conventional testing. Its authorization rules have a formal description in Lean, while the production implementation uses Rust; differential tests compare their behavior. Checking agreement between those implementations is distinct from proving every property of the production program. The specification still needs to express the behavior people actually intend.