title: "用 Lean 4 为代码建立可验证的正确性证明"
source_url: "https://www.youtube.com/watch?v=lRa9sPaMyy4"
author: "AI Engineer"
excerpt: "公共早报 Varun Pant 讲解如何借助 Lean 形式化验证，把规格转化为机器可检查的保证，让工程团队在测试、代码审查和概率性的 AI 判断之外验证关键代码。"

Brief Description

Varun Pant explains why formal verification becomes more relevant as coding agents produce code faster than people can review it. He introduces Lean as both a programming language and proof assistant, then walks through specification-first development, proof kernels, tactics, and several ways to apply formal methods to Lean, Rust, policy systems, and multi-language tooling.

Table of Contents

• Why tests and review are not enough

• Specification-first development and Lean

• Proof search, tactics, and trusted kernels

• Formal verification in practice

• Applying formal methods across languages

Why tests and review are not enough

Coding agents are generating more code than ever, and builders may create hundreds or thousands of pull requests each week. That raises a basic question: how can we know the resulting code is correct? Using an LLM as a judge is probabilistic. Tests only cover some inputs rather than all possible inputs, and human code review does not scale at the same pace as agents. None of those approaches can establish that code is correct for every input.

Formal verification can provide that stronger guarantee. It gives a mathematical proof that code is correct for all inputs. A developer writes a specification defining what "correct" means, and a formal verification tool proves that the implementation satisfies that specification. When the proof passes, the claim holds for every possible input.

Specification-first development and Lean

One way to use formal verification is to begin with the specification. The specification can be written directly in a formal language such as Lean, or first written in natural language and then formalized with AI assistance. The specification itself must be validated, either by human review or by testing it against some inputs, because it is upstream of every later artifact. It is a living artifact that the builder interacts with; everything else follows from it.

Once the specification is accepted, an AI coding agent can implement the code from it, and the verification tool can prove that the implementation matches the specification. In this division of work, humans own the specification while machines own the code and the proof.

Lean is both a programming language and a proof assistant. Definitions and proofs use the same language, so there is no translation layer between them. Lean is implemented in Lean, which makes it extensible, and it has a small trusted kernel. Proofs can be exported and checked independently.

Proof search, tactics, and trusted kernels

A Lean file can contain both executable code and its proof. For example, a function can reverse a list, while a theorem in the same file proves a property of list reversal: reversing the concatenation of A and B yields the reverse of B followed by the reverse of A. The theorem applies to every possible input.

The work of constructing such a proof is often done with tactics, while the small trusted kernel checks the result. A useful analogy is chess. The goal is like checkmate, and tactics are the moves. A person or tool explores a tree of possible moves, backtracks when one branch does not prove the goal, and tries another. When a proof is found, the independent kernel confirms it.

The kernel rejects incorrect proofs immediately, which reduces the amount of software that must be trusted. Multiple independent kernels are possible, and the surrounding ecosystem is open source, with kernels and related implementations in languages including C++, Rust, and Lean.

Formal verification in practice

One practical approach is to keep both specification and code in Lean. The talk describes Andreo AI converting zlib, a C compression library, to Lean over roughly a week. Its natural-language specification says that decompressing the output of compression returns the original data. AI can generate a formal specification, but checking that specification remains essential. Afterward, AI writes Lean code, produces helper lemmas as subgoals, and proves the final theorem, which is verified by the small independent kernel.

In this example, the AI decomposes the task into lemmas, proves them with tactics, and assembles the results into a final theorem. The cited proof contains 32,000 lines, illustrating that formal verification can support substantial proofs rather than only small demonstrations.

Another model is to keep production code in Rust while writing its functional specification in Lean. Cedar, an open-source authorization policy language used by AWS Verified Permissions and access systems, follows this approach: its specification is written in Lean and its production code runs in Rust. For a policy with a forbid rule, the important property is that any request satisfying that forbid policy is always denied.

The Rust implementation and Lean specification can be checked with differential random testing: for the same inputs, both should produce the same outputs. The talk notes that roughly 100 million differential random tests run nightly for this system, and no version ships until that condition is satisfied.

Applying formal methods across languages

Rust code can also be deductively verified with Lean or solvers. A solver is described as a powerful calculator: given a formula, it determines whether the formula is satisfiable or unsatisfiable. Verus is an open-source tool that uses the Z3 solver. Developers add specifications as annotations in the code, including requires and ensures clauses that state preconditions and postconditions. These are static checks enforced by the verifier and erased at runtime, much like ghost code.

Eneus is another example. It works from Rust's mid-level intermediate representation, translates functionally to Lean, and then uses the same theorem-proving environment discussed earlier.

For broader language support, AWS is working on an open-source tool called Strata. The idea is that a developer can start with any programming language and create a dialect, much like a compiler lowers a high-level intermediate representation to a low-level one. Strata Core is written in Lean. Once programs share that core representation, they can be dispatched to different engines: Lean proofs, SMT solvers, or model checkers.

The closing recommendation is to begin with critical code: write down what correctness means, validate that specification, let a coding agent implement it, and let a formal verification tool prove it. The aim is to build software and systems that are not merely probably correct, but provably correct.