In May 2016, the newly created Decentralized Autonomous Organization (DAO), an investor-directed venture capital fund built as a smart contract on the Ethereum blockchain, raised around $150 million worth of digital currency. Hopes were high. The fund was to be a fully transparent and decentralized organization, with investment decisions made collectively through member votes, and operations automated based on the smart contract’s predetermined rules.
Just a month later, the DAO was hacked. An attacker drained more than $60 million of Ether by exploiting a re-entrancy vulnerability in the smart contract, a loophole in the code that allowed the attacker to withdraw the same funds multiple times before the smart contract had updated their account balance.
This was more than just a financial disaster; it was a wake-up call for the blockchain community about the critical importance of smart contract security. Re-entrancy is now carefully protected against — some platforms even prevent it by design — but what about the next such vulnerability? Known dangers are easy to mitigate; the challenge of identifying and protecting against unknown vulnerabilities remains a significant concern.
Smart Contract Vulnerabilities Cost Billions
While the DAO hack represents one of the highest-profile smart contract exploits, it is far from the only such case.
“When you start building smart contracts for DeFi (Decentralized Finance), you are moving a lot of money,” explained Galois Research Engineer Santiago Cuellar. “These currencies represent billions of dollars, so they’re very juicy targets for hackers.”
In 2023 alone, blockchain security companies reported around 600 hacks in the crypto space, resulting in around $2.6 billion in losses, with DeFi smart contracts among the primary targets. What’s more, the flaws in the code that leave smart contracts vulnerable to exploitation are often extremely difficult to detect or find, beyond the reach of traditional testing methods. A recent paper entitled “Demystifying Exploitable Bugs in Smart Contracts,” in which researchers dug into 516 exploitable bugs from 167 real-world contracts between 2021-2022, concluded that “more than 80% [of] exploitable bugs are beyond existing tools.”
Testing is Not Enough
The core issue, as with so many software problems, is that smart contracts are written by humans, and no matter how robust the code is, they are not immune to human error. With so much money at stake, hackers work extraordinarily hard to uncover even the tiniest of exploitable flaws.
“Hackers trick the contract with something its creators hadn’t thought about, generally corner cases,” Cuellar explained. “Then they get away with millions of dollars.”
While testing is a fundamental and important step in smart contract development, it’s not foolproof and, as the evidence increasingly demonstrates, it’s simply not enough to protect smart contracts. Finite by nature, testing can’t replicate every possible environment, find every remote edge case, or predict the cunning of malicious actors. Code reviews, though beneficial, are just as subject to human error as code writing, leaving potential gaps in security. The world of DeFi and blockchain thus faces a critical question: How can we do better?
Formal Methods Offer a Better Way Forward
Galois’s answer: formal verification of smart contracts.
“With testing, you cover a lot of cases and hope that’s good enough,” Cuellar said. “With formal methods, we try to cover all possible cases, eliminating whole classes of errors and leaving nothing to chance.”
At its most basic level, formal verification involves creating a mathematical model, called a specification, outlining how a program should and should not perform. The specification is then compared to the actual software implementation to check for correctness and security. While this process can traditionally be quite expensive and time-consuming, Galois’s Software Analysis Workbench (SAW) leverages SMT solvers to automate much of the verification process, allowing it to scale to complex systems.
Over the years, Galois has put SAW to work in national security, fintech, and cloud computing applications (including verifying AWS’s cryptographic library) to keep citizens, systems, and data safe; secure financial transactions, and protect the privacy of millions of people across the globe. Now, building upon its established expertise, Galois is bringing formal verification to the world of smart contracts with a new tool called Formal Verso.
Verifying Soroban Smart Contracts with Formal Verso
“Formal Verso is a Rust front end built on top of Galois’s Software Analysis Workbench (SAW),” explained Cuellar.
While different smart contracts are written in different programming languages, smart contract platform Soroban embraces Rust’s security-forward design. With Formal Verso, Soroban has the ability to root out and fix any vulnerabilities in the smart contract’s code – even those that are difficult or impossible to detect with conventional testing methods. In other words, Formal Verso leverages the full power of formal verification techniques to future-proof Soroban smart contracts from the clear, present, and growing danger of blockchain hacks, safeguarding millions of dollars and avoiding the loss of both finances and trust in the platform.
Our Vision of the Future: A Higher Assurance Blockchain
Though currently tailored only for smart contracts written in Rust, Formal Verso’s potential is far-reaching. Because Formal Verso is built on top of SAW, a similar front end could be designed for smart contracts written in any language – including custom languages often used by major players such as Solana and Ethereum. Here, the underlying SAW engine would operate exactly the same, and provide the same level of assurance.
This adaptability suggests that custom-engineered versions of Formal Verso have the potential to prevent future catastrophic smart contract exploits, saving billions of dollars of stolen digital currency every year. Had a version of Formal Verso tailored to the Ethereum blockchain been available in 2016, it could have detected the exploit that led to the DAO hack, preventing the theft of tens of millions of dollars. We hope Formal Verso will be there to prevent the next one. Even now, with Formal Verso and SAW, Galois has the potential ability to identify the vast majority of the exploitable bugs highlighted in “Demystifying Exploitable Bugs in Smart Contracts” and judged “beyond existing tools.”
To put it simply: in Formal Verso, the tool for rooting out exploitable bugs in smart contracts now exists.
Formal verification is no longer a luxurious add-on; it’s rapidly becoming a necessity within the blockchain development process. Formal Verso is not merely about pushing the boundaries of secure coding for the sake of the puzzle (though it is quite fun)—it’s about crafting a solid foundation on which the next generation of blockchain applications can safely and reliably be built. As smart contracts continue to manage more assets and execute increasingly complex transactions, the technology that secures these contracts must not just evolve but be ahead, ready to mitigate the risks of an ever-expanding digital finance landscape.
Learn more on the Formal Verso Project Page.