Topic
Formal Verification
Machine-checked mathematical proofs, Lean 4, and provably correct software.
3 published pieces
Published work
Bend 2 and Proof-Blocked AI: What a Law File Actually Buys
Part three of the machine-checked proofs series. Bend 2 moves the kernel-checked loop from mathematics into ordinary code: you declare laws, the AI must prove its changes keep them. We read the site, the paper and the checker, and ran it. The checker held up against every cheat we tried. The laws are still yours to get right, and on launch day nothing but convention guards the file they live in.
AI · September 9, 2026Navier-Stokes Blowup: What a Machine-Checked Singularity Unlocks for Real Engineering
Yesterday’s Navier-Stokes result is part two of the machine-checked proofs series: OpenAI proved smooth forced flow can blow up in finite time, with the full derivation checked in Lean. The equations don’t give you a better pump tomorrow – but the verified lemmas, the blowup guard pattern, and the agent pipeline behind them map directly onto CFD, tidal and pumped-hydro sizing, and home hydronic loops you can test this week.
AI · September 5, 2026The Practical Value of Machine-Checked Proofs
Fermat’s Last Theorem has zero direct industrial utility. But the pipeline that machine-checked its 13 million lines of Lean code demonstrates an operational verification engine for critical software, cryptographic primitives, and hardware design. Here is where the real economic value lands – and how DIY developers and small teams can leverage it today.