How Could Formal Verification Help with Cyber Resilience?

Formal verification could help to secure critical software, but it faces a number of practical barriers. More advanced AI could help lift many, but not all, of them.

Cyber agents are getting good. A Chinese state-sponsored actor likely used Claude Code to orchestrate a cyber espionage campaign. Coding agents can help find exploits on live smart contracts worth millions of dollars. AI-enabled malware can dynamically generate malicious scripts and obfuscate code to evade detection. To mitigate increased cyber risks, we will need a multi-pronged approach. Approaches like misuse safeguards can help to deal with the leading edge of AI cyber capabilities. But we will also need societal-level interventions that can protect us as these capabilities diffuse…

related reading

• A shallow dive into formal verificationvitalik.eth.limo
• Automatic Formal Verification for Code Generationlogicalintelligence.com
• Formally Verifying the Easy Partbrainflow.substack.com
• When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
• The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentsalphaxiv.org
• Vulnerability Research Is Cooked - Quarrelsomesockpuppet.org
• The Compute Verification Postfirstscattering.com
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentsalphaxiv.org
• Prediction: AI will make formal verification go mainstream - Martin Kleppmann's blogmartin.kleppmann.com
• The End-State Fallacy: Where Is AI Security Headed?endstatefallacy.com
• The Great Refactor | IFPifp.org