Machine-checked proofs for AI-written software
A product manager writes the requirements, one agent turns them into Lean, another writes the code, and the checker proves the code satisfies the spec. The human reviews only the formalization, and most of that pipeline already works today.