The Cleverness of the Technical Approach
The fundamental anxiety of AI writing code is the chasm between "looks right" and "actually right," and human review can't fill that pit. Leanstral's approach borrows the rigidity of formal methods: describe the spec of critical logic in a proof assistant like Lean, and the AI-generated implementation must pass machine checking together with a proof, failing if a single step is wrong. AI happens to fill formal methods' decades-old shortcoming (writing proofs is too labor-intensive), and formal methods happen to fill AI's shortcoming (untrustworthy output)—two fields that used to disdain each other unexpectedly mesh.
The Real Radius of Applicability
First, a cold shower: the applicability radius of formal verification is limited—if the spec itself is written wrong, no proof can save it, and domains where "right and wrong are defined by humans," like UI and business logic, are basically out of reach. But on its home turf—cryptographic implementations, protocol stacks, financial cores, safety-critical systems—the value of this combination is real; those domains already use formal methods, but at a cost so high only a few organizations can afford it, and AI bringing the price down means opening the market. "AI-generated, machine-verified" may be the next standard posture for high-assurance software, and Leanstral is an early exploration on that path worth remembering by name.
via: Hacker News