Introducing Komet: Smart Contract Testing & Verification Tool for Soroban, Created by Runtime Verification
At Runtime Verification, we have spent years developing tools and methods to enhance the security and correctness of blockchain systems. One of our core areas of expertise is WebAssembly (WASM) semantics, where we’ve worked on groundbreaking projects like Kontrol, which brings formal verification to Solidity developers working with Foundry. Kontrol has enabled developers to symbolically execute their tests and ensure that their smart contracts behave as expected under all conditions. With this extensive background, we’re excited to introduce our latest tool: Komet, a formal verification and fuzzing tool designed specifically for Soroban smart contracts on the Stellar blockchain.
Funded by the Stellar Community Fund, Komet is made possible through the generous support of the Stellar community. The grant has allowed us to kickstart development, but there’s still more work to be done. The next phase of Komet requires continued community backing to fully realize its potential. We’re calling on the Stellar community to help us push this tool forward, to ensure that developers building on Soroban have access to the highest level of security through formal verification and fuzzing.
Why Formal Verification Matters
Blockchain systems, especially smart contracts, operate in a highly adversarial environment where any vulnerabilities can cause immediate loss of funds. With billions of dollars of value locked in smart contracts, thorough testing and verification methods are critical for the Soroban ecosystem to flourish. Formal verification offers a mathematical guarantee that smart contracts will behave as intended, eliminating vulnerabilities that traditional testing or auditing methods might miss. This added layer of security is vital for ensuring that smart contracts, which are often responsible for managing and securing vast amounts of assets, are safe from attacks. For more information, see some of our blog posts on Why Formal Verification Matters and Intro Lore on Formal Verification.
What is Komet?
Komet is a tool specifically designed for Soroban, enabling developers to verify and fuzz their smart contracts. Komet’s current capabilities are based on Runtime Verification’s work in auditing specific Soroban functions. While only a limited set of functions are currently supported, the next release of Komet will include fuzzing and formal verification for the entire set of Soroban host functions. This will allow developers to fully verify their smart contracts, making them more secure and reliable in the ever-challenging landscape of blockchain development.
In the coming months, we will continue to expand Komet’s functionality, and we look forward to sharing updates with the community. To learn more about Komet or to get involved, visit Komet’s website, where you’ll find more information on how the tool works, a demo of what the tool can do, and how you can support its ongoing development.
Support Komet for a more secure Stellar ecosystem
The Stellar ecosystem has a unique opportunity to benefit from the cutting-edge formal verification technology that Komet offers. We want to extend our deepest thanks to the Stellar Community Fund (SCF) for supporting the initial research and development of this tool. Komet has the potential to revolutionize how Soroban smart contracts are secured, and with continued community support, it can become a cornerstone of trust and security for Stellar-based projects.
We encourage developers to try Komet for themselves by following our detailed instructions in the documentation, and to spread the word on Twitter to help grow awareness. Your feedback is invaluable—please don’t hesitate to reach out with your thoughts and suggestions. Let’s work together to ensure Soroban smart contracts remain secure and resilient as the Stellar ecosystem continues to grow.
