Lumen Loop
All media
VideoYouTubeRuntime VerificationSeptember 15, 20241y ago4:17

Introducing Komet: Formal Verification and Fuzzing for Soroban

Comet is a fuzzing and formal verification tool for Soroban smart contracts. The demo walks through testing a vaults contract using property-based testing, showing how to write test contracts that interact with target contracts and use the Comet CLI to run automated fuzzing on contract functions.

Developer ToolsSmart ContractsSoroban
Lumen Loop's take

Comet is a fuzzing and formal verification tool designed for Soroban smart contract developers. The presentation demonstrates how to use Comet by testing a vaults contract with functions like init, getCoreState, and calculateDepositRatio. Test contracts are written as special contracts that can manipulate blockchain state and interact with target contracts. The demo shows the init setup process, property-based test cases with assumptions to avoid overflow and division by zero errors, and the Comet CLI workflow that compiles test contracts and runs fuzzing with randomly generated inputs. The tool discovers test functions automatically and executes them, with plans to add symbolic execution alongside fuzzing in future versions.

Mentioned projects
1 project linked
R
Runtime VerificationDeveloper Tooling
SCF
SecurityFormal Verification

Open-source tool for Soroban smart contract developers, enabling them to perform robust formal verification.

View →