What is formal verification, and why does Vitalik Buterin think AI can help?

1. Can AI and formal proofs eliminate crypto bugs?

Vitalik Buterin suggests that AI could improve crypto security through formal verification. In a recent blog post, he argued that AI-assisted verification could become an important safeguard against increasingly sophisticated software attacks.

The concept is compelling: AI generates or examines code, while mathematical proofs confirm that software behaves precisely as intended. In principle, this approach could reduce severe smart contract flaws, exchange vulnerabilities and consensus failures.

However, a significant limitation remains. Even if AI advances formal verification, crypto systems cannot realistically guarantee completely bug-free software. Real-world blockchains depend on multiple assumptions, hardware components, external connections, governance mechanisms and human decisions that mathematics alone cannot fully protect.

Buterin’s idea could substantially improve crypto security. It is unlikely to eliminate the possibility of failure altogether.

2. What is formal verification?

Formal verification involves mathematically demonstrating that software follows specified rules within defined parameters.

Rather than relying solely on human reviewers or testing environments, developers create mathematical descriptions of how a system is expected to behave. Specialized tools then check whether the code consistently meets those requirements.

For example, a formally verified smart contract might mathematically establish that:

• Assets cannot be withdrawn without proper authorization.
• A token’s total supply cannot exceed a fixed cap.
• A validator cannot make unauthorized state changes.
• Specific attack vectors are not possible under the stated conditions.

In simple terms, testing asks whether the code works correctly in selected cases. Formal verification asks whether the code can break the rules under any conditions covered by the proof.

This technique is already used in aviation, defense systems and other critical hardware and software contexts. Crypto developers are increasingly adopting it for critical security components because blockchain transactions are often irreversible and can involve substantial amounts of money.

3. Why Buterin believes AI changes the equation

In his May 2026 article, Buterin argued that AI could significantly reduce one of formal verification’s main drawbacks: its complexity.

Traditional formal verification can be expensive and time-consuming, and it requires specialized expertise. Practitioners often need advanced knowledge of theorem provers, proof systems and mathematical logic. Writing proofs can sometimes require more effort than developing the original software.

Buterin expects AI to simplify parts of this workflow.

He described a scenario in which developers write code in lower-level languages or use proof-oriented tools such as Lean, while AI assists with generating proofs, identifying inconsistencies and checking correctness with less manual effort.

The central idea is that AI may not only accelerate software development. It could also help support the mathematical validation of software security properties.

Buterin framed this approach as a defensive response to the growing use of AI in software analysis. If malicious actors can use AI to identify vulnerabilities more quickly, defenders may need stronger mathematical assurances rather than relying only on traditional code reviews.

4. Why crypto platforms are vulnerable to software flaws

Traditional banks can often reverse or recover fraudulent transfers through established processes, but blockchain-based systems typically provide fewer options once a transaction is finalized.

Even a small programming error in a decentralized finance (DeFi) protocol can lock assets, create unauthorized tokens or allow attackers to drain liquidity pools within minutes. Past crypto exploits have repeatedly shown that even extensively reviewed code can fail under unexpected conditions.

Formal verification is particularly relevant because many crypto components operate through strict mathematical or logical rules:

• Consensus mechanisms follow defined protocols.
• Smart contracts execute deterministic operations.
• Zero-knowledge protocols depend on cryptographic correctness.
• Bridges and rollups rely on verifiable state changes.

Buterin identified areas such as STARKs, ZK-EVMs, consensus protocols and post-quantum cryptography as promising candidates for AI-assisted verification.

These systems can be so complex that manual review alone may not scale effectively.

Did you know? Formal verification has long been applied to high-assurance systems, including aircraft software, defense systems and nuclear reactor protection systems, where software failures can have severe real-world safety consequences. 

5. Why formal verification cannot guarantee complete crypto security

Despite its promise, formal verification has important limitations. The primary challenge is that proofs confirm only what has been explicitly defined in a model.

If the underlying assumptions are incomplete, incorrect or unrealistic, even verified code can still fail. A proof is only as reliable as the specification it is built on.

For example, verified code might still fail because of:

• Incorrect assumptions about user behavior
• Flawed external data feeds
• Hardware vulnerabilities
• Compiler errors
• Side-channel attacks
• Governance interference
• Failures in cross-chain connections
• Financial attacks outside the model’s scope

Buterin has also noted that formal verification can overlook “unmodeled assumptions” and other unaddressed components.

A mathematically verified bridge contract could still encounter problems if:

• Validators collude maliciously.
• The underlying cryptography becomes vulnerable.
• External components behave unexpectedly.
• The specification contains logical gaps.

Formal verification can reduce software-related risks. It cannot eliminate broader systemic risks.

Did you know? Some smart contract exploits have occurred despite multiple professional audits. Audits typically examine likely attack paths, while formal verification attempts to mathematically prove that entire categories of failure are impossible under specific assumptions.

6. AI introduces new challenges

AI-assisted verification also introduces additional concerns. Large language models can produce logic that appears convincing but is incorrect. Experts continue to highlight risks such as hallucinations, unreliable proofs and mismatches between natural-language descriptions and formal specifications.

Research indicates that AI-generated proofs can struggle with:

• Complex interdependencies
• Changing code structures
• Ambiguous requirements
• Long chains of reasoning
• Updates to development tools

AI may accelerate verification processes, but it cannot fully replace skilled human oversight.

There is also a broader concern. AI-assisted verification tools could become so complex that only a small group of technical specialists can meaningfully understand or evaluate them. This could conflict with the transparency and broad participation often associated with crypto systems.

Did you know? AI systems are increasingly being used by both attackers and defenders in cybersecurity. While developers hope AI can help verify code safety more quickly, attackers may also use AI tools to identify vulnerabilities, automate parts of exploit discovery and analyze protocol weaknesses at scale.

7. Why “sufficiently safe” matters more than “completely bug-free”

Crypto security may eventually focus less on achieving perfection and more on reducing the likelihood of major failures.

Formal verification already allows developers to demonstrate important properties of smart contracts and protocols. AI could make these methods faster, more affordable and easier to scale.

This progress alone could improve security across:

• Wallet applications
• Layer-2 networks
• Zero-knowledge systems
• Stablecoin infrastructure
• Consensus software
• Post-quantum cryptographic systems

However, “mathematically proven” must not be mistaken for “incapable of failing.”

Real-world systems combine code, people, financial incentives and governance structures. Mathematics can strengthen one part of this system, but it cannot eliminate every source of uncertainty.

Buterin’s proposal could help crypto develop more reliable foundations. It is unlikely to create an ecosystem free from all hacks, attacks and system failures.

AI-assisted formal verification could become a valuable addition to crypto security practices, rather than a complete solution to software vulnerabilities and broader systemic risks.