Formal Verification: When Intention Is Not Enough
As AI gets better at exploiting the gap between intentions and implementations, formal verification becomes hard to ignore.
I’ll start today’s article off with a definition of formal verification as provided by Keagan McLelland on the Bitcoin Development Mailing List:
Formal Verification is a practice in software development that gives greater assurances than typical testing procedures or forum arguments on how various schemes, protocols, and implementations behave. When we argue about how Bitcoin is designed or how it ought to be designed, engineers will make statements of fact about how the system works, but depending on how much effort is put into the presentation of that argument, it can be difficult to tell if a statement is true, or if it is, why it is true. By formally specifying these statements of fact on how the Bitcoin protocol works we can be precise about what we are saying, what properties we have, what properties we want, and whether the system actually delivers those properties or not.
Normal programming languages do this to an extent, and indeed one of the best ways to settle a dispute is to look at how the code is implemented. However, the nature of C++ can make it difficult to get certainty over certain claims about the behavior of the protocol due to its type system being comparatively weak when judged against the tools typically tasked with this responsibility.
If you want to be able to make specific arbitrary logical statements about Bitcoin or any other software you typically need to specify it in a language with a Dependent Type Theory. The class of tools used for this is called an Interactive Theorem Prover (ITP).
Formal verification has existed for decades, but is not commonly used to verify software protocols for one simple reason: it’s expensive. Designing a model that accurately represents a protocol, its rules, and allowed inputs requires specialized skill and a massive amount of work. For most projects until recently, the potential risks didn’t justify the cost.
AI changes that calculation as it lowers both the cost and potential surface area of attack. Anthropic recently published two cryptanalysis papers: one finds a weakness in the HAWK signature scheme (proposed to be post-quantum-safe) and the other finds a slight speedup in breaking AES (under unrealistic circumstances).
While neither of these introduce groundbreaking discoveries in cryptography or mathematics, what they do prove is the ability for frontier models to essentially “grind out” hard to find weaknesses. It was never impossible for humans to find these results, but they require a massive amount of attention across a large swath of tools and domains.
From Anthropic’s blog post on the papers (emphasis mine):
Mythos Preview achieved these results mostly autonomously and mostly without human intervention. Over the course of a week, one Anthropic researcher worked together with Claude to develop the HAWK attack, and another researcher built a scaffold that allowed Claude to fully autonomously discover the AES attack. Each of the results cost roughly $100,000 in API cost to develop.
It is no longer enough to create tests and inspect a project’s codebase. A motivated attacker with a large enough financial incentive will throw AI resources at relentlessly scanning for weaknesses to exploit. Look no further than recent attacks on the Lightning network:
Work is already underway in the Bitcoin ecosystem, with Keagan McClelland’s btc-verified, focusing first on Bitcoin’s Merkle-root logic. libsecp256k1, the core Bitcoin cryptographic library, has also been the subject of formal verification work.
To be clear, formal verification is not a panacea. Proofs can only show whether a program follows a specification, but not whether the specification itself describes the intended behavior. However, AI is making it nearly impossible for humans to defend their systems through manual review alone. Critical pieces of software will need stronger ways to state what must be true, with a method to mechanically check those claims.
The future of protocols and software is likely one where those critical claims are defined using formal specifications to deterministically verify their properties. Without them, we risk leaving interpretational gaps between what we think a protocol does and what it actually guarantees. AI will be extremely competent at searching that gap.
Mine Print Hash
The US recently intervened in Japan’s Yen market, which is a generational action. Matt Dines reviews those historical intervention to help us understand how this “Yentervention” compares, why it was deemed important to intervene now, and why Japan is a critical nexus in the stablecoin dollar future.
Open Threads
Geopolitical maneuvers to test boundaries and create new trade routes:
China bypasses shipping chokepoints via “Ice Silk Road”. Link
Pentagon drafting new nuclear strike strategy. Link
Component in British naval drones sent signals back to China. Link
Suspected Russian drone explodes at German airport. Link
Syria recontrols its air fields, pushing Russia out of key bases for African missions. Link
Building monetary networks: