AI vs. Formal Verification: contradiction or complementary?

While AI-assisted tools are revolutionizing how quickly we uncover software vulnerabilities, formal verification remains a powerful and mathematically proven defense.

This has been proven in practice for years. In a landmark study testing automated, randomized fuzzing against a variety of C compilers, researchers successfully forced almost all of them to produce wrong outputs, except for CompCert, a formally verified compiler.

We’ve seen the exact same story play out in high-stakes aerospace security: during both elite hacker conventions and DARPA red-teaming exercises, professional hackers consistently failed to breach drones and autonomous helicopters running seL4, a formally verified microkernel. Even when hackers were given full access to uncritical partitions, the core system remained untouchable.

This raises an important question for the modern security landscape, particularly in security-critical and cryptography-heavy code: how do AI-driven exploit tools and formal verification actually relate to one another?

AI Excels at Vulnerability Detection

If your goal is finding bugs fast, AI is far more efficient than formal verification. AI tools are unparalleled at rapidly combing through codebases, mutating inputs, and surfacing obscure edge cases, and this way dramatically lowering the cost and time required to find exploitable flaws. Anthropic's recent Claude Mythos Preview assessment illustrates just how far this has come: the model autonomously identified and exploited zero-day vulnerabilities across every major operating system and browser, including a 27-year-old bug in OpenBSD and a 16-year-old vulnerability in FFmpeg that had survived years of intensive fuzzing by human researchers. We've seen this capability put to defensive use firsthand: auditing our own repositories with AI has already produced concrete results, surfacing real issues in unverified code and leading to targeted fixes such as this pull request.

Verification Is About the Proof of Absence

Formal verification is not a bug-finding tool. It is a mathematical guarantee. Formally verified software will remain secure against AI-driven attacks because it eliminates entire classes of vulnerabilities by proof. AI cannot exploit a memory leak or a buffer overflow if it was proven that no memory issues exist. In domains where "probably secure" is not good enough, formal verification remains the gold standard.

A Growing Intersection

What's become increasingly clear is that these two technologies are not competing. The boundary between them is beginning to blur in many ways.

Cryspen and many others have begun experimenting with AI to assist in constructing formal proofs that can then be checked by proof assistants like Lean. Recent work such as lean-zip demonstrates AI-assisted theorem proving in practice, and companies like Harmonic, Logical Intelligence, and Axiom Math are building tools specifically targeting this space.

The Meaningful Connection

AI can be used not just to find bugs and exploits, but to actively accelerate formal verification efforts, and in turn helping eliminate entire classes of vulnerabilities altogether. The result is a more tractable approach to formal verification by reducing the areas that need to be manually verified.

Used aggressively on the offensive side, AI stress-tests software and finds issues faster than ever before. Used in support of formal methods, it helps extend the reach of mathematical guarantees. For the core primitives and critical infrastructure that absolutely cannot fail, the combination of both ensures that no matter how capable AI-driven attacks become, there are simply no bugs to be found.

Author: 

Franziskus Kiefer is a cryptography & security engineer and researcher. He is CEO of Cryspen, a project partner of PROTECT.