AI can help researchers find bugs at scale. It can also help engineers prove that defined classes of failure cannot occur within a model. For onchain systems that hold capital or enforce settlement, that defensive use matters: an accounting, authorization, or state-transition failure can become an irreversible loss.

In a shallow dive into formal verification, Vitalik Buterin made the case for AI-assisted formal verification as part of a more defense favoring future. Formal verification defines required behavior and checks whether the implementation can violate it within the model. AI can accelerate the translation from human requirements into machine-checkable specifications and proofs. The strength of the result still depends on the property, threat model, system boundary, assumptions, and software version.

For onchain systems, the useful question is which failure paths a proof rules out, which assumptions remain exposed, and whether the evidence still applies after the next release. This practical deep dive explains how formal verification works, assesses where AI can help today, and gives protocol teams and institutional reviewers a way to judge whether a proof supports a real security claim.

Start with the failure you want to rule out

Formal verification starts with a claim about how the system must behave. Engineers translate it into a formal specification, model the relevant software, and prove that the implementation satisfies the property across every execution covered by that model. A proof is only as broad as the claim, system boundary, and assumptions used to produce it.

Testing demonstrates that selected examples behave correctly. Fuzzing searches large input spaces for failures. Verification can cover an entire defined class of behavior without sampling each case. Ethereum.org's formal verification documentation explains the main techniques, including model checking, symbolic execution, and theorem proving.

The boundary between verification and validation matters. Verification asks whether the implementation matches the specification. Validation asks whether the specification captures what people actually intended. The first can be mechanized. The second still demands security judgment, domain knowledge, and a realistic model of the adversary.

A formal proof is strongest when its assumptions are easier to audit than the software it protects.

Solvency, permissions, state transitions: where verification pays off

Web3 systems contain several unusually strong targets for formal methods. Smart contracts are one. Others include execution and consensus clients, bridges, cryptographic libraries, zero-knowledge proof systems, rollup state-transition logic, and wallet or key-management components. Many of these systems operate under explicit protocol rules, produce deterministic state transitions within those rules, and control assets or consensus. A defect can produce immediate, irreversible loss.

Formal verification can apply across crypto code, although its leverage varies. The strongest candidates are properties that remain simpler than the implementation:

• Asset conservation and solvency: value cannot be created, lost, or withdrawn outside defined accounting rules.
• Authorization and upgrade control: privileged actions occur only through approved roles, thresholds, and governance paths.
• Protocol and cryptographic integrity: clients, bridges, rollups, and proof systems accept only the state transitions, messages, and proofs permitted by the protocol.

Teams can specify solvency, access control, and state-transition rules for the same system. Checking those properties together can expose conflicting requirements before code reaches production.

This is the source of defensive asymmetry. An attacker needs one exploitable path. A proof can establish that a whole category of paths is unreachable under stated assumptions.

AI can draft the reasoning. The checker decides.

Formal methods have existed for decades. Their limiting resource has been proof engineering: translating intent into formal specifications, generating proof obligations, and guiding proof assistants through long chains of machine-checkable reasoning.

AI can take on parts of that workload. A model can propose invariants, generate proof steps, interpret tool feedback, and revise an argument. Formal tools then check the work and either establish the property, return a modeled counterexample, or leave obligations unresolved.

A peer-reviewed ICLR 2026 study of neural theorem proving introduced a benchmark drawn from verification conditions in Linux, Contiki, and other real software. The results show meaningful progress alongside substantial remaining difficulty. The benchmark supports using AI as an aid to proof work while keeping experts responsible for selecting claims and examining assumptions.

AI-assisted vulnerability discovery is advancing quickly. In February 2026, Anthropic reported that Claude Opus 4.6 helped find and validate more than 500 high-severity vulnerabilities in open-source software, in work focused on memory-corruption flaws. This is first-party research from a model developer, so it should be read as a documented capability demonstration rather than a neutral industry census. The result shows that AI can surface serious flaws in code that has already received extensive testing.

The exploit outside the model

The central weakness is specification risk. A team can prove an incomplete claim with perfect mathematics. A protocol might verify local accounting while omitting oracle manipulation, governance capture, cross-chain disagreement, key compromise, or a failure in deployment configuration.

Protocol teams and institutional reviewers can expose that boundary with three questions:

1. What exact property was proved? Replace broad labels such as “secure” with explicit claims about balances, permissions, state transitions, liveness, or cryptographic behavior.
2. Which components and assumptions sit outside the model? Identify the compiler, proof kernel, oracle, bridge, governance process, hardware, operator, and key-management dependencies that still carry risk.
3. What change invalidates the evidence? Tie every proof to a source revision, build, configuration, and deployment so teams know when verification must run again.

These questions also clarify where testing and independent review add value. Some properties are nearly as complicated as the code they describe. Model checkers encounter state explosion, symbolic execution encounters path explosion, and theorem provers can require extensive guidance. Formal verification delivers the most leverage when the claim is compact, consequential, and stable enough to maintain.

A theorem needs a version number

Protocol security teams and institutional risk committees need versioned control evidence tied to a specific system, threat model, and release. A raw proof count cannot tell them whether a theorem still applies to the software in production.

The process begins with business requirements: assets remain reconcilable, minting requires defined authority, upgrades follow governance, settlement preserves agreed rules, and withdrawals remain available under expected stress. Protocol engineers, security researchers, and risk owners should refine those statements together. That collaboration converts abstract security language into claims a proof system can check and an institution can govern.

Independent reviewers should challenge the specification, inspect the implementation boundary, and record every assumption the theorem depends on. Relevant code, compiler, configuration, or deployment changes should trigger impact analysis and re-verification wherever the proof boundary is affected. The resulting evidence can then support engineering review, change management, operational risk, and external diligence without implying protection beyond the verified scope.

As of September 2026, formal verification is moving closer to the center of protocol engineering. The Ethereum Foundation's latest protocol priorities describe it as cross-cutting tooling for work spanning fast finality, privacy, state, and zkEVM development. The push toward an L1 zkEVM is also advancing formal workflows and verified cryptographic components that can support post-quantum work. This marks a shift toward verification as shared infrastructure for protocol design, extending far beyond deployed contracts.

The rest of the system still needs defending

AI gives defenders two ways to improve their position: search for flaws before attackers do, and rule out defined classes of failure through formal proof. The second advantage holds only while the proof's assumptions match the deployed system.

For protocols and the institutions relying on them, the assurance has to survive the next release. A credible security claim should identify the property, the threat model, the trusted components, the verified release, and the conditions that require re-verification. Formal proof then becomes part of a layered control environment alongside testing, adversarial review, monitoring, governance, and incident readiness.

____________________________________________________________________________________________________________

If your protocol or institution is deciding which properties deserve proof and how that evidence fits alongside audits, monitoring, and incident readiness, contact our team to discuss how those controls fit together.