How to get started with Komet - Property Testing and Formal Verification for Soroban

At Runtime Verification, we're dedicated to pushing the boundaries of software verification and analysis. Our new tool, Komet, is tailored for developers working with Soroban. Soroban is the smart contract platform on the Stellar blockchain. Komet is supported by the Stellar Foundation and aims to offer enhanced verification capabilities using formal methods to help developers secure their smart contracts.

Why We’re Building Komet

With the increasing complexity of DeFi and other blockchain applications, the need for secure smart contracts has become critical. Hacks on smart contracts in the past have shown that vulnerabilities can lead to major lost funds. Komet was developed to equip developers with the testing and formal verification tools needed to build safer, more resilient dApps.

Soroban is Stellar's platform, where smart contracts are written in Rust and compiled to WebAssembly (Wasm). Komet is built on top of KWasm—a WebAssembly formal semantics framework developed in K. It provides Soroban developers with two powerful techniques for ensuring the correctness of their contracts: fuzzing and symbolic execution.

Komet’s seamless integration with the Rust ecosystem is one of its key advantages. Developers can write property-based tests in Rust, using the same language they already use for Soroban smart contract development. Then, they can execute the tests using fuzzing to explore a wide variety of possible inputs, and symbolic execution to formally verify the contract's behavior across all inputs. This combination ensures that Soroban contracts are thoroughly tested and verified, making them more secure.

Understanding Property Testing and Verification

Traditional testing relies on manually crafted test cases with fixed inputs. However, this approach often fails to explore the full range of possible inputs a program might encounter. In contrast, property-based testing shifts the focus from specific inputs to the broader behaviors the system should exhibit. Instead of trying to guess which inputs might cause failures, developers define the properties of the system, and tests are automatically run with randomized inputs. This approach uncovers edge cases that manual tests could miss, and ensures that the system's properties hold across a wide range of scenarios, offering a more thorough and dynamic testing process.

With Komet, you have the flexibility to run your property tests using either fuzzing or symbolic execution. While fuzzing tests the contract with randomized inputs, providing a probabilistic level of confidence, symbolic execution is far more powerful. To learn more about symbolic execution, you can check out Raoul Schaffranek's presentation on formal methods. To summarize, formal verification uses symbolic inputs representing all possible values, allowing Komet to verify that the contract meets the specified properties across every potential input. This guarantees a higher degree of confidence in the correctness of the contract by ensuring no edge cases are missed.

Installation

The easiest way to install Komet is via the kup package manager. Follow the steps below to install kup and then Komet:

1. Install kup by running the following command:

bash <(curl https://kframework.org/install)

2. Once kup is installed, you can install Komet with this command:

kup install komet

3. After the installation is complete, verify it by checking the help menu:

komet --help

Case Study: Testing the adder Contract

(Source: https://github.com/runtimeverification/komet-demo)

To illustrate how Komet can be used to test Soroban contracts, let’s look at a simple example. We’ll be working with a basic contract called adder, which features a single function that adds two numbers and returns their sum. In Komet, we write our tests as contracts that interact with the contract we want to test. For this example, we will create a test_adder contract to verify the behavior of the adder contract.

The project structure for this example looks like this:

.
├── contracts
│ ├── adder
│ │ ├── src
│ │ │ └── lib.rs
│ │ └── Cargo.toml
│ └── test_adder
│ ├── src
│ │ ├── lib.rs
│ │ └── komet.rs
│ ├── Cargo.toml
│ └── kasmer.json
├── Cargo.toml
└── README.md

The adder Contract

The adder contract is a simple, stateless contract with a single endpoint, add. This function takes two numbers as input and returns their sum. The result is returned as a u64 to avoid overflows. Since the contract doesn't maintain any internal state or use storage, its behavior is straightforward and purely based on the inputs provided.

#![no_std]

use soroban_sdk::{contract, contractimpl, Env};

#[contract]

pub struct AdderContract;

#[contractimpl]

impl AdderContract {
   pub fn add(_env: Env, first: u32, second: u32) -> u64 {
      first as u64 + second as u64
   }
}

Writing the Test Contract

Test contracts typically have an init function for setting up the initial state, such as deploying contracts or preparing the blockchain environment. They also include functions with names starting with test_ to define properties and run test cases against the contract being tested. Test contracts have special abilities that normal contracts do not, provided by our framework through custom WebAssembly hooks. These hooks, declared as extern functions in komet.rs, enable advanced operations like contract creation and state manipulation.

Setting the Initial State: The init Function

In the context of testing the adder contract, the init function is specifically responsible for deploying the adder contract and saving its address within the test contract’s storage.

#[contract]

pub struct TestAdderContract;

#[contractimpl]

impl TestAdderContract {
   pub fn init(env: Env, adder_hash: Bytes) {
       let addr_bytes = b"adder_ctr_______________________";
       let adder = komet::create_contract(&env, &Bytes::from_array(&env, addr_bytes), &adder_hash);
       env.storage().instance().set(&ADDR_KEY, &adder);
   }
   // other functions
}

We are using the create_contract function from komet.rs for deploying a contract with a specified address and a Wasm hash. The hash represents the Wasm code of the target contract (in this case, the adder contract). The Wasm hash provided to the init function is derived from the kasmer.json file, which contains a relative path to the compiled adder contract. This file enables Komet to locate the WFasm file, register the Wasm module, and pass its hash to the init function.

{
 "contracts": [
   "../../target/wasm32-unknown-unknown/release/adder.wasm"
 ]
}

Once the init function has successfully completed, all subsequent test cases are executed based on this predefined initial state, ensuring consistency and allowing tests to be performed under controlled conditions.

Defining Contract Properties: Test Endpoints

In Komet, test cases are defined as contract endpoints with names starting with the test_ prefix. These endpoints specify properties of the contract being tested, and return a boolean to indicate whether the test passed or failed.
For instance, in the test_adder contract, the test_add function verifies the adder contract’s behavior by using its address—set up in the init function—to invoke the add method and check whether the adder contract correctly computes the sum of two numbers.

impl TestAdderContract {
   // Initialization code...
  
   pub fn test_add(env: Env, x: u32, y: u32) -> bool {
       // Retrieve the address of the `adder` contract from storage
       let adder: Address = env.storage().instance().get(&ADDR_KEY).unwrap();
      
       // Create a client for interacting with the `adder` contract
       let adder_client = adder_contract::Client::new(&env, &adder);


       // Call the `add` endpoint of the `adder` contract with the provided numbers
       let sum = adder_client.add(&x, &y);
      
       // Check if the returned sum matches the expected result
       sum == x as u64 + y as u64
   }
}

Running Tests

Once the test contract is written, the next step is to compile and run it. Here's how you can execute the tests using Komet.

1. Compile the Project

Before running any tests, compile the project from the workspace's root directory:

soroban contract build

This command will build both the adder and test_adder contracts.

2. Navigate to the Test Contract Directory

After compiling the project, change directories into the test_adder contract folder:

cd contracts/test_adder/

3. Running Tests with Fuzzing

To run the tests using fuzzing (which generates random inputs for testing), use the following command:

komet test

After some compilation logs, you should see an output like this:

Processing contract: test_adder
Discovered 1 test functions:
	- test_add

  Running test_add...
	Test passed.

This indicates that Komet discovered the test_add function and successfully executed the test using randomized inputs.

4. Running Tests with Symbolic Execution (Proving)

To run tests with symbolic execution, which verifies the contract's behavior for all possible inputs, use the following command:

komet prove run

This method will run the proof for all test functions in the contract. It ensures that the property being tested holds true across all input combinations, providing thorough verification of the contract's correctness.
Additionally, you can explore more proving options by using the --help flag to see available commands and arguments:

$ komet prove --help
usage: komet prove [-h] [--wasm WASM] [--proof-dir PROOF_DIR] [--id ID] COMMAND

positional arguments:
  COMMAND           	Proof command to run. One of (run, view)

options:
  -h, --help        	show this help message and exit
  --wasm WASM       	Prove a specific contract wasm file instead
  --proof-dir PROOF_DIR
                    	Output directory for proofs
  --id ID           	Name of the test function in the testing contract

After running the proof with the --proof-dir option, you can use the view command to inspect the proof tree and examine the details of symbolic execution.

Conclusion

Komet brings formal verification directly into the existing Soroban development workflow, allowing developers to ensure the correctness of their contracts with both broad, randomized testing through fuzzing, and deep, exhaustive verification using symbolic execution. Since all testing is done in Rust using existing Soroban APIs, it’s easy for developers to adopt the tool without needing to learn a new language or system.

By using Komet, developers can focus on building innovative solutions for the Stellar ecosystem while ensuring their contracts are rigorously verified.