Three days before I was pushed out of OpenAI I posted a Formal Verification Manifesto in a core research Slack channel. It listed OpenAI systems that could benefit from formal verification. The only person who responded was @sama, who was very supportive. Not sure what the moral of this story is, but it's never too late for OpenAI to invest seriously in software & hardware formal verification! On a more serious note, @theoremlabs and @AnthropicAI did something amazing. They showed how to verify software at scale without requiring developers to write specifications in Rocq or Lean. Instead, they used existing fuzz harnesses as specifications and LLMs to generate machine-checked proofs. Of course, fuzz harnesses specify only some correctness properties. In the simplest case, the proofs establish crash-safety, not full functional correctness. We need community-maintained open-source projects with reusable formal specifications and correctness proofs for major libraries, kernels, compilers, virtual machines and hardware. Human review of critical specifications and LLM-generated patches is essential. A model could satisfy a specification simply by removing functionality. As AI writes and rewrites critical infrastructure, formal verification should become a key part of AI control. Critical properties of AI-generated code should be machine-checked rather than taken on faith. AI is making vulnerabilities easier to find and exploit. Frontier LLMs and reusable formal specifications could finally make formal verification practical and economical at scale, while keeping it understandable to humans. Kudos to Theorem co-founders @rajashree and @diagram_chaser!