--- title: "Vitalik Buterin Says AI Formal Verification Could Help Prevent Multi-Million Dollar Crypto Hacks Across Ethereum Ecosystem" type: "News" locale: "en" url: "https://longbridge.com/en/news/287031704.md" description: "Ethereum co-founder Vitalik Buterin advocates for AI-assisted formal verification to enhance security in the crypto ecosystem, arguing it can help developers prove software safety before launch. Amid rising cyberattacks, including a recent $76 million hack, Buterin emphasizes that AI could eliminate coding flaws. He acknowledges the limitations of formal verification but believes it can significantly improve security, especially in complex systems. Several Ethereum projects are already testing this approach, aiming for a future where code is shipped with machine-checkable proofs of correctness." datetime: "2026-05-20T08:30:40.000Z" locales: - [zh-CN](https://longbridge.com/zh-CN/news/287031704.md) - [en](https://longbridge.com/en/news/287031704.md) - [zh-HK](https://longbridge.com/zh-HK/news/287031704.md) --- # Vitalik Buterin Says AI Formal Verification Could Help Prevent Multi-Million Dollar Crypto Hacks Across Ethereum Ecosystem Ethereum co-founder Vitalik Buterin believes the same artificial intelligence systems feared for accelerating cyberattacks could eventually become one of crypto’s strongest security tools. As hackers continue draining millions from vulnerable blockchain platforms, Buterin is pushing for a future where AI helps developers mathematically prove software is safe before it ever goes live. His argument comes as the crypto industry faces mounting pressure over repeated exploits, including more than $76 million stolen from Echo Protocol’s cross-chain bridge in recent days, alongside attacks targeting THORChain and the Verus-Ethereum Bridge. ## Can AI Stop The Next Crypto Exploit Rather than seeing AI purely as a threat, Buterin argued that the technology could help eliminate many of the coding flaws that continue to plague crypto infrastructure. His focus is on “formal verification,” a method where software is paired with mathematical proofs that confirm the code behaves exactly as intended. > Vitalik Buterin believes AI could become one of crypto’s biggest security upgrades. > > According to him, AI-assisted formal verification may help Ethereum and other blockchain infrastructure detect vulnerabilities before hackers can exploit them. > > As the industry grows, smarter… pic.twitter.com/sSAWRnpaig > > — 𝗔𝗹𝗶𝗸𝗼-𝗱𝗮𝗻𝗴𝗼𝘁𝗲 (@alikodangote9) May 19, 2026 While the concept has existed for decades, it remained too difficult and time-consuming for most developers to use at scale. According to Buterin, AI could finally make the process practical. Instead of engineers manually writing proofs line by line, developers could increasingly rely on AI systems to generate both the software and the accompanying mathematical checks. Humans would then verify that the final proof actually reflects the intended behaviour of the system. > Many people have claimed that with AI-assisted bug finding, secure code (and hence trustless anything) will be impossible. > > I have a much more optimistic take, and AI-assisted formal verification is a major part of the reason why:https://t.co/0ceMBZ6uqj > > — vitalik.eth (@VitalikButerin) May 18, 2026 Buterin wrote, > “If you formally verify end-to-end, then you are proving not just that some description of the protocol is secure in theory, but that the specific piece of code that the user runs is secure in practice.” He added that users would no longer need to audit huge amounts of code themselves, saying, > “you simply need to check over the statements that are proven about it.” ## Ethereum Projects Already Testing AI Verification Buterin pointed to several Ethereum-related projects already experimenting with the approach. One example is Arklib, which is attempting to create a fully formally verified STARK implementation. Another is evm-asm, a project building an Ethereum Virtual Machine in low-level RISC-V assembly while mathematically checking it against a readable reference version. He also said newer AI systems are already proving useful for proof generation. According to Buterin, both Claude and DeepSeek 4 Pro have performed well when writing Lean proofs, while Leanstral, a smaller specialised model, can run locally and outperform larger general-purpose AI systems on formal verification tasks. The Ethereum co-founder described this model as a possible “final form of software development,” where highly optimised code is shipped alongside machine-checkable proofs of correctness. ## Why Buterin Still Does Not Trust AI Completely Despite his optimism, Buterin repeatedly warned that formal verification is not a complete answer to cybersecurity problems. He highlighted previous failures involving verified compilers, incomplete proofs, and cases where developers mathematically proved the wrong thing because the specification itself failed to reflect the intended behaviour. He wrote, > “Formal verification is not a panacea.” He argued that the method works best when the desired outcome is simpler than the complexity of the software being built. > people say ai makes secure code impossible > > vitalik disagrees and so do i. > > here's what i learned from his new post on formal verification: > > \> ai writes the code (even raw assembly) > \> lean writes the proof that the code is correct > \> computer verifies the proof automatically > \>… https://t.co/nw0T2id727pic.twitter.com/uP6U3kHFHn > > — Rohit Purkait (@codeswithroh) May 18, 2026 He specifically pointed to quantum-resistant signatures, STARKs, consensus algorithms and ZK-EVMs as areas where formal verification could become especially valuable. Buterin said, > “A huge part of the value-add is that the proofs are truly end-to-end. Often, the nastiest bugs are interaction bugs that sit at the edge of two sub-systems that are considered separately.” He also rejected growing fears that increasingly advanced AI cyberattacks could eventually make open-source systems impossible to secure. He wrote, > “The entire cypherpunk ethos is fundamentally based on the idea that on the internet, the defender has an advantage.” ## Crypto Hacks Add Pressure On Ethereum Security The discussion arrives during one of the industry’s most difficult periods for cybersecurity. Echo Protocol recently lost more than $76 million after attackers breached its cross-chain bridge infrastructure. Earlier attacks targeted THORChain, which lost over $10 million, while the Verus-Ethereum Bridge exploit resulted in another $11.58 million in stolen funds after hackers abused missing validation checks. Buterin suggested that some of these failures may have been avoidable with stronger proof-based verification systems. The wider threat environment is also becoming more serious as AI models improve at finding software vulnerabilities. Anthropic reportedly restricted access to its cybersecurity-focused Claude Mythos model after internal testing showed the system could autonomously identify and exploit vulnerabilities at levels far beyond earlier public AI systems. Researchers also claimed the model identified 271 vulnerabilities in Mozilla Firefox during testing, while separate reports linked AI-assisted research to exploits involving Apple’s M5 chip protections. Meanwhile, security researchers at the U.K. AI Security Institute reportedly found that OpenAI’s GPT-5.5 demonstrated increasingly advanced offensive cyber capabilities. Buterin wrote, > “Bugs in computer code are scary.” ## Inside Buterin’s Private AI Setup Alongside his warnings about AI security risks, Buterin also revealed details of the personal AI system he runs entirely on his own hardware. He operates an open-source Qwen3.5:35B model through llama-server on a laptop equipped with an Nvidia 5090 GPU. According to Buterin, the system generates roughly 90 tokens per second, making it fast enough for everyday use without relying heavily on cloud services. > Update: I switched to llama-swap, and the 35B runs at 90 tok/sec now. > > — vitalik.eth (@VitalikButerin) March 9, 2026 His setup includes locally stored copies of Wikipedia and technical documentation to reduce internet searches, which he considers a privacy risk because they expose user behaviour. Buterin also connected the AI system to his Ethereum wallet and messaging accounts, though with strict restrictions in place. He developed a tool allowing the AI to read Signal messages and emails, but any outbound messages or higher-risk actions require manual approval. > Vitalik Buterin says AI should run locally on personal devices, not in the cloud. > > • Cloud AI creates single points of failure and surveillance > • Local models preserve privacy and user sovereignty > • Crypto + local AI = verifiable, censorship resistant compute > > When the… pic.twitter.com/no1QMVvXZA > > — THE BLOCKOPEDIA (@theblockopedia\_) April 3, 2026 He said the same logic should apply to crypto wallets connected to AI systems. Any autonomous AI spending should be capped at $100 per day, while larger transactions should require human confirmation. The approach mirrors how he secures his own cryptocurrency holdings. Around 90% of his funds are reportedly stored in a multisig Safe wallet, where multiple trusted parties control access rather than a single individual. > Vitalik Buterin doesn't use a cold wallet for his own personal crypto. > > This is how he keeps his crypto safe: > > The founder of Ethereum, Vitalik Buterin revealed that he keeps 90% of his crypto funds in a mutisig Safe wallet. > > "M-of-N, some keys held by you (but not enough to… pic.twitter.com/CTx5tuP87k > > — Talha (@talhaasiiif) May 7, 2024 His concerns intensified after researchers discovered that around 15% of third-party tools linked to OpenClaw, one of GitHub’s fastest-growing repositories, allegedly contained hidden malicious instructions that quietly transmitted user data to external servers. Buterin warned that while end-to-end encryption and locally run software had finally started reaching mainstream adoption, cloud-based AI services risk reversing that progress. ### Related Stocks - [COIN.US](https://longbridge.com/en/quote/COIN.US.md) - [ETHE.US](https://longbridge.com/en/quote/ETHE.US.md) - [GBTC.US](https://longbridge.com/en/quote/GBTC.US.md) - [BLCN.US](https://longbridge.com/en/quote/BLCN.US.md) - [ARKB.US](https://longbridge.com/en/quote/ARKB.US.md) - [BTCO.US](https://longbridge.com/en/quote/BTCO.US.md) - [BRRR.US](https://longbridge.com/en/quote/BRRR.US.md) - [ETHHKD.VAHK](https://longbridge.com/en/quote/ETHHKD.VAHK.md) - [ETHUSD.VAHK](https://longbridge.com/en/quote/ETHUSD.VAHK.md) ## Related News & Research - [OpenAI tests ChatGPT finance tool linking to bank accounts](https://longbridge.com/en/news/286685720.md) - [CME to launch AI computing power futures market; BlackRock to further develop tokenized fund structure.](https://longbridge.com/en/news/286171119.md) - [Flare to Be Integrated With D’CENT Wallet](https://longbridge.com/en/news/286972571.md) - [Ethereum Community Debates Changes To Staking Model As ETH Remains Stuck Below $2,300](https://longbridge.com/en/news/286153164.md) - [ZAWYA: OKX launches USDSⓈ-M options on Bitcoin and Ether](https://longbridge.com/en/news/286889580.md)