SAN FRANCISCO, CA, October 11, 2023 —Today, Stellar Development Foundation and Certora announced security support for Soroban, the Stellar network's smart contract platform with cutting-edge formal verification capabilities. Soroban is the first WASM-powered platform to be supported by Certora, traditionally associated with the Ethereum Virtual Machine (EVM).
In the adversarial world of smart contracts, security is paramount. Smart contracts, which automate transactions and processes on blockchain platforms, are sensitive. They handle a significant amount of capital, are entirely transparent – so anyone can see code and bugs – and are immutable, which means that bug mitigation requires lengthy governance processes. This environment makes security non-negotiable and the correctness of code crucial to preventing vulnerabilities in order to help safeguard user assets. Certora, a pioneering formal verification tool, has been at the forefront of this effort, providing developers with the means to verify their code.
One of the lessons learned from our experience in DeFi is that tools and auditing come too late in the development process. This oversight increases software costs and leads to bugs being detected only after vulnerabilities have been exploited. Certora's tools can help developers write specifications before the code is complete to ensure safe, reliable applications. We are excited to join the Soroban ecosystem.
Mooly Sagiv, CEO of Certora
Certora's powerful software leverages 20 years of academic research and unique technologies that scale Formal Verification to real programs, ensuring the safety and reliability of smart contracts. Formal Verification goes beyond traditional testing methods. The mathematical process rigorously checks code against its intended specification, just like a proofreader reviewing an essay for grammar errors, and helps identify and eliminate potential issues. This approach provides a higher level of confidence in the correctness and security of smart contracts, preventing bugs such as the recent Vyper compiler error from ever being included. Over the last four years, Certora has secured customers' code and prevented more than 100 high-security bugs in leading DeFi protocols such as Aave V2, Balancer V2, Aave V3, Compound V2, Compound V3, Gnosis Safe, SushiSwap ConstantPool, and Lido. Certora secures $25 billion of total value locked on Ethereum, according to DefiLlama.
But Certora's formal verification tools go further than checking the code once. It provides a continuous integration service. Whenever code is changed, it aligns with the specifications. This proactive approach to verification helps prevent bugs and vulnerabilities from entering the codebase in the first place, saving both time and resources in the long run. It integrates into the normal development pipeline.
Soroban's focus on scalability, sustainability, and testing marks a new generation of smart contracts. With WASM, a portable binary-code format well-suited for blockchain environments, Soroban opens the door to a wide range of programming languages and tools, including testing, making it easier for developers to build on the Stellar network. And now, with Certora's support, Soroban further enhances its appeal to developers. Certora's formal verification capabilities will help developers on the Soroban platform ensure the reliability and security of their smart contracts, giving users greater confidence in the applications they ultimately interact with.
Certora's support of Soroban will give the more than 100 projects already on the platform access to innovative verification tools built to help achieve software correctness. Coupled with the built-in testing and security of Soroban, developers have the tools needed to avoid the vulnerabilities we have seen make headlines in the past and make way for a secure DeFi ecosystem from the start.
Tomer Weller, VP of Product at Stellar Development Foundation
In addition to creating a Soroban-specific formal verification tool, the Certora security team will participate in the Soroban Audit Bank Initiative, investing time and funds into training the Soroban ecosystem on using this new service.