Stellar Community Fund

By Komet: Formal Verification

Kasmer: Formal Verification

SCF #28

$50.0K

Legacy v5.0 Activation Award

Awarded

Opensource tool for Soroban smart contract developers, enabling them to perform robust formal verification.

Products & Services

The product we are building is Kasmer for Soroban. The product is property-testing based formal verification for Soroban smart contracts. This enables developers to write Rust property tests and not just fuzz over them, but formally verify them, to achieve the highest level of assurance for their codebase.

The problem being solved is that formal verification is difficult for many engineers to get started with, but by taking a property-testing approach, Runtime Verification is lowering the barrier to entry. This allows developers to include formal verification in their normal quality assurance processes, even enabling it on CI, using our open source tooling. One example of the success of this is when Amazon enabled formal verification of C code using C property tests (and CBMC for model checking). They had great success getting normal C developers to do formal verification at a much larger scale than previously by using the property-testing based approach.

Our tool uses KWasm to do symbolic execution of compiled Soroban smart contracts. There is tooling for turning Rust-level property tests into WebAssembly code (via the compiler), and then into KWasm based verification challenges. Once the verification is complete (passed, failed, or unsure), the result is translated back to the Rust level for developers to understand the next step. This keeps developers in their own workflow, rather than asking them to step outside of it. This first activation award is focused on specializing KWasm to Soroban by implementing the Soroban host functions.