Loading...
Supporting developers, startups, and full-fledged companies building on Stellar and Soroban
© 2025 Stellar Development Foundation
Subscribe to the Newsletter
By Komet: Formal Verification
Komet gives developers a tool to fuzz and formally verify Rust code by property testing in Rust, a language they already know
We used the previous Activation Award to build an MVP tool that currently supports a limited set of Soroban host functions in order to demo formal verification features on the fxDAO smart contracts. With this Build Award, we aim to achieve three primary goals:
Yes
$100.0K
Success and impact for Komet would be defined by having auditing firms integrate it into their formal verification process, positioning Komet as the go-to tool for ensuring the security of high TVL protocols on Stellar. The output would be Komet becoming a core part of the audit workflow for protocols, leading to widespread adoption by developers and security teams. Ideally, our goal would be to have four full-time formal verification engineers continuously engaged with large protocols as more value is locked on Stellar. The impact would be significant: by making formal verification the gold standard for Stellar protocols, Komet would reduce the likelihood of security breaches, ultimately protecting user funds and fostering greater confidence in the Stellar ecosystem. This would help drive further adoption of Soroban smart contracts, making Stellar more competitive in the DeFi space and beyond.
Our go-to-market strategy for Komet will follow the blueprint we successfully used for Kontrol, our open-source formal verification tool for Solidity. After building Kontrol, we maintained and improved it through paid formal verification engagements. Developers can freely use the tool, but many projects and protocols hire us to assist with writing tests and proofs and to guide them through the verification process. Additionally, we monetize Kontrol by charging larger protocols for the compute power necessary to run proofs on their extensive codebases, as these often outgrow the developer's local resources. For Komet, we plan to replicate this strategy. After completing the grant project, we will offer Komet to the Stellar community as an open-source tool for developers to use. Beyond that, we will provide services to help projects write formal verification proofs, execute them, and optimize the tool for their specific needs, ensuring the highest level of security. This will allow us to continue developing Komet while building long-term relationships within the Stellar ecosystem.
For prior traction and validation, we would like to highlight our success with Kontrol, a tool similar to Komet but built for Solidity instead of Rust and Soroban. Kontrol has been widely adopted by hundreds of developers, including professional auditing firms, solo auditors, and internal testing teams. Notably, major protocols such as Optimism and Lido have incorporated Kontrol into their security flow. This widespread usage validates the core concept of Komet and demonstrates the demand for such a tool in blockchain ecosystems.
As for Komet itself, we have already begun exploring its application during the FxDAO smart contract audit. During this audit (available here), we discovered 10 informational and 10 potentially critical findings. Of the critical findings, considering the hypothetical creation of tests designed using the invariants raised in the audit, 7 out of the 10 would likely have been discovered using fuzzing, and definitely would have been found using formal verification. While not trivial to be identified during testing, the remaining three could be validated and demonstrated using Komet’s formal verification capabilities. Of the 10 informative findings, three could have been found using either fuzzing or formal verification, and the remaining 7 are related to protocol design or best practices. Not only would Komet help shorten the duration of audits due to the ease of validating invariants, but would also empower developers and engineers to test and protect their own code.
Going forward, we believe that Komet could make all future Soroban audits more efficient, enabling developers and auditors alike to catch critical issues earlier in the development cycle. This validation from both Kontrol’s success and Komet’s real-world applicability shows that Komet is poised to have a substantial impact on the Soroban ecosystem.
Tranche 1 has already been completed using the previous SCF #28 activation award of $50,000. These were the deliverables from the first tranche, all of which have been completed (included links where possible):
[x] Open-source BSD-3 licensed repository with CI setup, importing the KWasm semantics, and including the implemented Soroban host functions. - https://github.com/runtimeverification/komet/ [x] Komet property tests for the selected functions from the FxDAO/vaults contract. - Added to the project repository as CI tests. [x] Clear documentation on the remaining host functions that must be implemented for complete Soroban support. - GitHub issue: https://github.com/runtimeverification/komet/issues/28 [x] CLI tool capable of fuzzing Rust property tests and proving simple properties. - Available via the kup package manager. [x] Documentation with installation and usage instructions. - https://docs.runtimeverification.com/index/komet
We propose to break down the remaining award into 2 tranches, which are outlined below.
Tranche 2 of the Komet project will focus on expanding the tool's capabilities and performance to support all Soroban host functions so that it can handle a wide range of real-world smart contract verifications.
The Mainnet phase will focus on the symbolic execution & the prover. In addition, we will refine the user interface, and gather feedback from early users. This phase will make Komet a production-ready tool for all Soroban developers.
Paul Len
By Komet: Formal Verification
Kasmer: Formal Verification