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
• When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
• Project Glasswing: Securing critical software for the AI era \ Anthropicanthropic.com
• Formally Verifying the Easy Partbrainflow.substack.com
• The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
• Prediction: AI will make formal verification go mainstream - Martin Kleppmann's blogmartin.kleppmann.com
• Verified Machine Learning Infrastructure: Formal Methods for Trustworthy Artificial Intelligence Deployment | RANDrand.org
• Automatic Formal Verification for Code Generationlogicalintelligence.com
• Asymmetry of verification and verifier’s rule - Jason Weijasonwei.net
• What Happens When the World is Run on Code No One Understands?time.com
• The Scalable Formal Oversight Research Program — LessWronglesswrong.com
• The Compute Verification Postfirstscattering.com