Formal verification might solve AI's review bottleneck
17 hours ago
- A new software engineering paradigm combines formal verification and AI: humans specify requirements in a formal language like Lean, and AI writes code along with a machine-checkable proof of correctness, eliminating human review of generated code.
- AI alone faces a review bottleneck because it can write code at near-zero cost, but reviewing all that code becomes a new bottleneck; formal verification removes this by proving correctness automatically, with increased assurance as a side effect.
- The framework involves humans defining hard constraints (formal specification) and optimization objectives (benchmarks), while AI agents write code and proofs; human effort is minimal as constraints are proven and objectives measured automatically.
- Analogies to machine learning include risks like overfitting and specification gaming, where agents may exploit weaknesses in specs; tools like regularization and careful metric design are needed to manage these risks.
- A Hello World example (k-th smallest element) demonstrates the approach: Lean definitions capture correctness, agents fill in implementation and proof, and benchmarks optimize runtime; the agent improved from sorting to quickselect.
- A case study at powdr (autoprecompiles for zkVMs) shows success: 500 lines of Lean spec, benchmarks for optimization, and 100% AI-generated code and proofs without human review; circuit-size reduction matches previous implementation, and runtime improved significantly.
- The approach may generalize if writing specs is cheaper than maintaining code, and reusable spec libraries could help; integration via FFI allows incremental adoption, potentially shifting focus from code to requirements in software engineering.