Certora recently organized the first-ever formal verification contest for Rust using Certora’s open source Prover. We hosted two community contests for Soroban smart contracts with a combined prize pool of 40,000 USDC with audit platforms Code4rena and Cantina. These introduced formal verification to the Soroban developer community and demonstrated its applicability to Rust-based smart contracts. We will dive into examples from our community.

Formal verification is a rigorous method based on mathematical logic for ensuring that a program behaves according to a specification. It is an effective technique for securing smart contracts. At Certora, we have developed tools to secure smart contracts for EVM, Solana, and Stellar with research underway for even more chains.

While the Certora Prover has been at the center of many past Solidity EVM formal verification contests, we have now held the first two contests for code written in Rust, specifically Soroban smart contracts for the Stellar blockchain. Teams writing decentralized finance (DeFi) smart contracts in Rust, as described in our recent blog post, should consider design and coding choices that both reduce the likelihood of logic errors and also make the code easier to formally verify.

We invited all members from the Web3 security community to use our formal verification tool, Sunbeam, that targets Stellar smart contracts written with the Soroban framework. These contracts are written in Rust and deployed as WebAssembly bytecode on Stellar. Users write formal specifications expressing security and correctness-related properties using Certora’s Rust library called CVLR which has macros dedicated for Soroban. Sunbeam compiles the CVLR specifications and smart contract source code to generate WebAssembly bytecode and then formally verifies the bytecode, proving whether or not the code complies with properties in the specification.

Evaluating Specifications

We use mutation testing to evaluate contest participants’ work by assessing the quality of their formal specification. Traditionally, mutation testing injects small, atomic faults in code and runs a test suite to see if the faults are caught. This can be used to improve the test suite coverage by adding test cases that the developer missed. At Certora, we extend this idea to formal verification: we assess the coverage and quality of specifications by applying mutations (individually) to the original smart contract source code and running the Sunbeam prover to see which specifications catch the mutations. 

For Solidity, we built Gambit, a mutant generator that automatically creates mutated variants of a smart contract. For Rust-based smart contracts like Soroban, we use both manually-created mutants and some generated by the Gambit-like tool, universalmutator.

For both contests, we created a set of mutants based on domain knowledge and used them to grade the specifications written by the participants. A specification earned more of the contest rewards by catching more of the mutations. The value of each caught mutation was weighted inversely to the number of participants that caught it, so higher rewards went to specifications with more unique coverage. In addition, participants got significantly more rewards by creating a specification that catches a real vulnerability in the protocol code, as confirmed by the Code4rena and Cantina audit contest judges.

Blend v2 Contest

Our Blend protocol contest was the first ever Rust-based formal verification contest in the DeFi space! We teamed up with Code4rena to organize it during their community audit of Blend v2 smart contracts from February 24 to March 17, 2025.

With the short contest timeline, we narrowed the scope to key files implementing the Backstop contract. We chose this contract due to its importance for the protocol’s solvency since a Backstop insures every Blend lending pool. For this contest, 21 participants created 996 rules in total, 229 of which caught at least one mutant. A report is available here highlighting some of those rules including this one by Zac369 that caught 3 mutations of the pool.rs file:

#[rule]
pub fn deposit_withdraw_equal(e: &Env, pool_balance: &mut PoolBalance, tokens: i128, shares: i128) {
   let pool_tokens_before = pool_balance.tokens;
   let pool_shares_before = pool_balance.shares;

   pool_balance.deposit(tokens, shares);
   pool_balance.withdraw(e, tokens, shares);

   let pool_tokens_after = pool_balance.tokens;
   let pool_shares_after = pool_balance.shares;

   cvlr_assert!(pool_tokens_after == pool_tokens_before);
   cvlr_assert!(pool_shares_after == pool_shares_before);
}

The code above is a CVLR rule that states a simple but important property for many DeFi protocols: a deposit by any user to any pool followed by an equal withdrawal results in no gain nor loss of pool assets. The cvlr_assert!() macro tests a condition and the Prover tries to find any counterexample in which the condition is false. If found, the calltrace of the counterexample can be investigated to see if the behavior indicates a bug in the contract logic. On the other hand, if the Prover completes without finding a counterexample, then the property is proven to be true. In the Blend contest, this rule passed with the original Blend source code but failed when we mutated the pool.rs source, thereby catching the mutations and showing this rule’s value in securing this aspect of the protocol.

Aquarius Contest

Our second contest for formal verification of Rust smart contracts was a joint effort with Cantina’s audit of Aqua Network’s protocol for Soroban, Aquarius, from May 7 to June 18, 2025. 

Aquarius is a decentralized liquidity management platform for Stellar. It supports exchange of tokens with two types of liquidity pools: volatile assets using Uniswap’s pioneering constant product market maker, and stable (or “highly correlated”) assets using Curve’s Stable Swap model for minimal slippage. The scope for formal verification included the fees_collector and access_control contracts, which implement the administration of the protocol including upgrades and ownership transfer. We had 26 participants who altogether wrote specifications with 1627 rules for the contest. Of these, 456 caught at least one mutant. A report of contest results is available here and this is one of the highlighted properties in the report. It was written by AsafDov and caught 4 mutations of fees_collector contract.rs file.

#[rule]
pub fn only_admin_transfers_roles_or_upgrades(e: Env) {
    let acc_ctrl = unsafe { &mut *&raw mut ACCESS_CONTROL }.as_ref().unwrap();

    // Execute any operation, then restrict to those that require Admin
    let action = nondet_func(e.clone());
    cvlr_assume!(
        action == Action::CommitTransfer
            || action == Action::ApplyTransfer
            || action == Action::RevertTransfer
            || action == Action::CommitUpgrade
            || action == Action::ApplyUpgrade
            || action == Action::RevertUpgrade
    );

    let admin: Option<Address> = 
            e.storage().instance().get(&acc_ctrl.get_key(&Role::Admin));
    match admin {
  // If there is an Admin, he must be the sender.
        Some(admin) => cvlr_assert!(is_auth(admin)),
  // Otherwise, the action requiring Admin should have reverted.
        None => cvlr_assert!(false),
    }
}

The CVLR rule above tests a common DeFi governance property: critical actions can only be taken by the administrator. And it does so in a way that allows this one rule to cover the security of multiple actions. The nondet_func() implemented here chooses randomly from a list of functions. This lets the Prover explore all those possible execution paths while evaluating this rule. The rule then limits the search space to only functions that require the Admin role (i.e. transfer or upgrade actions). It gets the current administrator’s address and verifies that any chosen function that executes successfully must be called by the admin. Or, if no admin has been set then execution must revert, preventing cvlr_assert!(false) from being reached.

Similar to the earlier Blend example, this rule passed with the original Aquarius source code but failed when we injected bugs in the contract.rs source file, showing that this rule catches such vulnerabilities if introduced to the governance logic.

Conclusion

Blend and Aquarius are cornerstone protocols for the Stellar chain built with an emphasis on security. These teams engaged Certora, Code4rena, Cantina and the wider DeFi security community for formal verification contests. Certora commends all contest participants for their work and congratulates the top performers, alexzoid and PositiveWeb3, on their rewards earned in the Blend v2 and Aquarius contests respectively. With over 20 competitors in each and a 24% increase from the 1st to 2nd contest, our community of security auditors is up to the challenge of securing Rust smart contracts. We hope this encourages others to organize formal verification contests as well.

Community audits harnessed the knowledge and skills of many to secure the Blend and Aquarius protocols. Adding Certora’s formal verification also leveraged the community’s skills at writing high level properties (over 2600!) into specifications that can rule out the existence of bugs and, when integrated into a project’s development pipeline, automatically block the introduction of bugs in the future.

All smart contract developers should consider formal verification to harden code security, and the Certora Sunbeam prover is a powerful tool for securing Rust smart contracts on the Stellar blockchain.

Acknowledgements

We would like to thank the Stellar Development Foundation, Code4rena, Cantina, the Blend team, the Aquarius team, all the participants, and our developers for their combined efforts in making these contests possible.

References

Blend Documentation: 

• https://docs.blend.capital/users/general-faq
• https://docs.blend.capital/blend-whitepaper#backstop-module

Aquarius Documentation: 

• https://docs.aqua.network/
• https://medium.com/aquarius-aqua/aquarius-amms-updates-and-plans-for-2024-f390e9d06b15