Building Formally Verified Software After Mythos: From Tests to Proofs
On April 7, 2026, Anthropic announced an AI model so good at finding zero-day vulnerabilities that they declined to release it publicly. By then, Claude Mythos had already found thousands; across every major browser and operating system. Six weeks into coordinated disclosure, roughly ~2% had been patched. Maintainers are asking Anthropic to slow down; they cannot triage fast enough.
Bug-finding now scales with compute. Bug-fixing still scales with humans. When models like this become public, anyone will be able to craft a tailored exploit for any software. Will yours hold up?
This talk argues the durable answer is formal verification; using mathematics to prove software correct for every possible input. Testing shows bugs are absent from the cases you tried; a proof shows an entire class of bugs cannot exist.
1. Why we need proofs now?
What Mythos found, why only ~2% is patched, and why the same failure mode, one input nobody thought to test, has been quietly destroying mission-critical systems for 40 years, ending with Chandrayaan-2's Vikram lander.
2. What proofs give that testing can't?
Testing samples the input space; proofs search it. Where each catches bugs and where each lets them through, and where verification already ships in production: a verified OS kernel, AWS's TLS code, a compiler certified for aviation.
3. How to integrate it into real development?
This talk is structured around a live, on-screen demonstration of a working compiler and proof toolchain: a lunar-lander braking controller where every test passes, yet the prover finds in seconds the exact class of bug that crashed Vikram. Then: where proofs fit alongside testing, and a realistic adoption path for teams who can't verify everything at once.
This continues my IndiaFOSS 2025 talk, Building A Software Language, though no prior context is required.
