Formal Methods for Stellar DeFi: Verifying Lending Protocol with Certora Sunbeam Prover

Hello! My name is Kirill Ziborov, and I’m a formal verification engineer and security researcher at Positive Web3. From February 24 to March 18, an audit contest for the Blend protocol on the Stellar blockchain was held on the Code4rena. In addition to the traditional manual audit, the competition included a formal verification track using the Certora Sunbeam Prover. This was the first contest of its kind on the Stellar blockchain, and our team placed 4th. In this article, I want to share my experience and impressions of the tool, as well as discuss formal verification of smart contracts on the Stellar blockchain in general.

Introduction

In my previous article, I described what formal verification of smart contracts is and its value in the context of blockchain security. Briefly, formal verification is a set of mathematical methods that ensure a program meets a given specification. In that article, I used the ConCert framework, implemented on top of the Coq (Rocq) proof assistant, for interactive proof of properties of a DEX/AMM protocol written in Solidity. During an interactive proof in proof assistants, the engineer writes formal specifications as theorems and proves them using tactics, which are interactively checked by the proof checker.

In contrast, Certora’s tools allow security researchers the ability to automatically check formal specifications. Many readers have probably heard of the Certora Prover for Ethereum and Solana smart contracts. This tool is already actively used by many auditors and has been competitively applied in public audit contests for protocols such as Euler, Uniswap v4, and Aave. If not, you can get acquainted with it in detail using the developer article and documentation. To verify a property of a Solidity smart contract with Prover, the engineer needs to formally specify the property in CVL (Certora Verification Language) and run the tool. The smart contract code and the specification are then transformed into a logical formula whose satisfiability is automatically checked by an SMT solver.

Certora Sunbeam Prover is a tool for automatic verification of smart contracts on the Stellar blockchain. It implements a pipeline analogous to Certora Prover for EVM contracts, but for Soroban contracts (a Rust dialect). Both tools operate at a low level: for EVM contracts, at the EVM bytecode level, while Sunbeam works at the WebAssembly (WASM) level for Soroban.

Installation

Follow the official Sunbeam installation guide to set up the tool.

Applying Certora Sunbeam for Formal Verification of Blend Smart Contracts

The process of formal verification can be divided into three stages: modeling, specification, and verification. In the first stage, we model or translate the source code into the representation that will ultimately be verified. In the second stage, we formally describe the code properties, and finally, in the third, we check that the code or its model satisfies these properties. Certora’s tools automate the modeling stage by transforming bytecode (or WASM code) into an internal intermediate representation. The verification stage is also automated via SMT solvers. The engineer only needs to write a correct formal specification, and the tool will automatically check code satisfiability against it.

For EVM contracts, Prover users write code in Solidity and specifications in CVL, which is syntactically similar to Solidity. Sunbeam, in turn, allows users to write correctness properties using a lightweight specification language called Cavalier, embedded in Rust.

Basically, in formal verification we check properties at two levels. First, we must ensure that the contract never reaches an invalid state. For this, we need invariants — properties that must hold in every reachable state of the contract for all possible inputs. In CVL for Solidity, Certora Prover provides automatic setup for verifying invariants. The Sunbeam specification language currently does not explicitly support invariants, but users can implement custom macros for invariant specification. Examples of such implementations can be found in Certora’s repositories (1), (2).

The other type of properties we check must guarantee the correctness of state changes when a function (or sequence of functions) is called. Such properties are called rules and essentially represent Hoare triples: precondition, function call, postcondition. Preconditions are written with cvlr_assume!, and postconditions with cvlr_assert! or cvlr_satisfy! statements.

Let’s move on to examples of rules we developed for the Blend protocol module in the verification contest.

About Blend Protocol

Blend is a leading DeFi lending protocol in the Stellar ecosystem. It allows any entity to create or utilize an immutable, permissionless lending market that fits its needs. The protocol features isolated lending pools with mandatory insurance, reactive interest rate mechanisms, and permissionless pool creation.

For this formal verification competition, only the backstop module was in scope. A backstop module is a crucial part of each Blend lending pool, which protects the lending pool from bad debt by providing first-loss capital. If a user incurs bad debt because their positions aren’t liquidated quickly enough, their bad debt is transferred to the backstop module, which pays it off by auctioning off its deposits. Users can backstop pools by depositing BLND:USDC 80:20 weighted liquidity pool shares into their backstop module, thus participating in insuring the lending pool. Backstoppers receive a percentage of interest paid by pool borrowers based on the pool’s rate. However, if a pool incurs bad debt, backstop deposits will be auctioned to cover losses proportionally. Withdrawals from backstop require a 21-day waiting period.

Diving Deeper

Let’s dive deeper into the backstop module’s logic. As an example, consider the backstop/user.rs file, which handles user balance changes and withdrawal queue management.

The main structure, UserBalance, stores the user’s total shares and a queue of pending withdrawal requests in a vector. Each queue element of type Q4W consists of an amount and an exp unlock timestamp (withdrawal is available after 21 days).

/// A deposit that is queued for withdrawal
#[derive(Clone)]
#[contracttype]
pub struct Q4W {
pub amount: i128, // the amount of shares queued for withdrawal
pub exp: u64, // the expiration of the withdrawal
}

impl cvlr::nondet::Nondet for Q4W {
fn nondet() -> Self {
Self {
amount: cvlr::nondet(),
exp: cvlr::nondet()
}
}
}

/// A deposit that is queued for withdrawal
#[derive(Clone)]
#[contracttype]
pub struct UserBalance {
pub shares: i128, // the balance of shares the user owns
pub q4w: Vec<Q4W>, // a list of queued withdrawals
}

impl cvlr::nondet::Nondet for UserBalance {
fn nondet() -> Self {
Self {
shares: cvlr::nondet(),
q4w: nondet_vec()
}
}
}

Notice the nondet implementations. This is a common summary which allows the prover to use a non-deterministically chosen value instead of performing a more complex computation or function call. Cavalier provides nondet implementations for various primitive types. Additional ones for Soroban are also provided in cvlr-soroban library.

Let’s consider the function queue_shares_for_withdrawal, responsible for queuing user shares for withdrawal. Its logic is as follows: the requested amount is added to the user’s q4w queue if it does not exceed the user’s total shares and the queue is not full (maximum 20 elements). The total number of shares is then decreased by the requested amount.

pub fn queue_shares_for_withdrawal(&mut self, e: &Env, to_q: i128) {
if self.shares < to_q {
panic_with_error!(e, BackstopError::BalanceError);
}
if self.q4w.len() >= MAX_Q4W_SIZE {
panic_with_error!(e, BackstopError::TooManyQ4WEntries);
}
self.shares = self.shares - to_q;

// user has enough tokens to withdrawal, add Q4W
let new_q4w = Q4W {
amount: to_q,
exp: e.ledger().timestamp() + Q4W_LOCK_TIME,
};
self.q4w.push_back(new_q4w.clone());
}

Let’s write rules for this function. Rules in Sunbeam are ordinary Rust functions annotated with #[rule]. We implement a non-deterministic selection of UserBalance using nondet, and declare the precondition with cvlr_assume!. The precondition here ensures that all checks pass and the function does not panic, but it’s not mandatory: remember that during verification, a rule is translated into an implication, and if the function execution fails, the implication’s antecedent is false, so the rule trivially holds.

#[rule]
pub fn queue_shares_for_withdrawal_correct(e: &Env, to_q: i128) {
let mut user_balance: UserBalance = cvlr::nondet();
cvlr_assume!(to_q <= user_balance.shares &&
user_balance.q4w.len() < MAX_Q4W_SIZE &&
to_q > 0);
let user_shares_before = user_balance.shares;
let q4w_before = user_balance.q4w.clone();

user_balance.queue_shares_for_withdrawal(e, to_q);

let user_shares_after = user_balance.shares;
let q4w_after = user_balance.q4w.clone();
let new_q4w = q4w_after.last().unwrap_optimized();

cvlr_assert!(user_shares_after == user_shares_before - to_q);
cvlr_assert!(q4w_after.len() == q4w_before.len() + 1);
cvlr_assert!(new_q4w.amount == to_q);
cvlr_assert!(new_q4w.exp == e.ledger().timestamp() + Q4W_LOCK_TIME);
}

We need to ensure that after a successful call to queue_shares_for_withdrawal, the user’s total shares decrease by the queued amount, and the last element of the queue contains the requested amount and a timestamp equal to the requested time plus 21 days.

Next, write a rule to check that a user cannot dequeue more shares than queued. Dequeuing is done with the dequeue_shares_for_withdrawal function. If we want to verify that the call fails, the postcondition should be cvlr_assert!(false).

#[rule]
pub fn dequeue_more_than_queue_fails(e: &Env, to_q: i128, to_dequeue: i128) {
let mut user_balance: UserBalance = cvlr::nondet();
cvlr_assume!(user_balance.q4w.len() == 0 &&
to_q > 0 &&
to_q <= user_balance.shares &&
to_dequeue > to_q);
user_balance.queue_shares_for_withdrawal(e, to_q);
user_balance.dequeue_shares(e, to_dequeue);
cvlr_assert!(false); //should pass
}

Now consider the withdraw_shares function, which processes withdrawal of unlocked shares from the queue.

/// Withdraw shares from the withdrawal queue
///
/// ### Arguments
/// * `to_withdraw` - The amount of shares to withdraw from the withdrawal queue
///
/// ### Errors
/// If the user does not have enough shares currently eligible to withdraw
#[allow(clippy::comparison_chain)]
pub fn withdraw_shares(&mut self, e: &Env, to_withdraw: i128) {
// validate the invoke has enough unlocked Q4W to claim
// manage the q4w list while verifying
let mut left_to_withdraw: i128 = to_withdraw;
for _index in 0..self.q4w.len() {
let mut cur_q4w = self.q4w.pop_front_unchecked();
if cur_q4w.exp <= e.ledger().timestamp() {
if cur_q4w.amount > left_to_withdraw {
// last record we need to update, but the q4w should remain
cur_q4w.amount -= left_to_withdraw;
left_to_withdraw = 0;
self.q4w.push_front(cur_q4w);
break;
} else if cur_q4w.amount == left_to_withdraw {
// last record we need to update, q4w fully consumed
left_to_withdraw = 0;
break;
} else {
// allow the pop to consume the record
left_to_withdraw -= cur_q4w.amount;
}
} else {
panic_with_error!(e, BackstopError::NotExpired);
}
}

if left_to_withdraw > 0 {
panic_with_error!(e, BackstopError::BalanceError);
}
}

The requested amount must be less or equal than the total unlocked shares in the withdrawal queue. Let’s write the corresponding rule:

// withdraw_shares should fail if amount > available shares in queue
#[rule]
pub fn withdraw_shares_balance_error_fails(e: &Env, to_withdraw: i128) {
let mut user_balance: UserBalance = cvlr::nondet();
let available_shares_before: i128 = user_balance.q4w.iter()
.filter(|x| x.exp <= e.ledger().timestamp())
.map(|x| x.amount)
.sum();
cvlr_assume!(to_withdraw > available_shares_before &&
available_shares_before > 0);
user_balance.withdraw_shares(e, to_withdraw);
cvlr_assert!(false);
}

Configuration

After writing specifications, we move to configuring the tool. It differs slightly from Certora Prover for Solidity.

Specs

All rule files should be Rust programs with the .rs extension, located in project/src/certora_specs.

Confs

For each contract, create a separate configuration file in the confs directory. According to the contest rules, if rules pass verification, the file should end with _verified suffix. If properties are violated, it should end with _violated.

Let’s consider user_verified.conf as an example. We specify the path to certora_build.py. The optimistic_loop option adds a precondition negating the loop’s condition at loop exit. Loop iteration count can be set with loop_iter (default is 1). In the rules block, list the rules to check.

{
"build_script": "../certora_build.py",
"optimistic_loop": true,
"precise_bitwise_ops": true,
"process": "emv",
"rule": [
"queue_shares_for_withdrawal_correct",
"withdraw_shares_balance_error_fails",
"dequeue_more_than_queue_fails"
]
}

Refer to the documentation for the full list of flags and options.

Mutations

In the mutations directory, place modified versions of the original contract code (mutants) to test your rules. Mutations are typically single-line changes that significantly alter contract logic. They’re used in contests to evaluate rule quality alongside real bugs.

For Solidity contracts, mutants can be generated automatically with Gambit; for Soroban, mutants should be created manually. It is a good practice to create and test mutants immediately after writing each rule. This ensures rule correctness and helps debugging.

Finally, our project structure looked like this:

project\
certora_build.py
confs\
mutations\
src\
certora_specs\
mocks\
summaries\

Folders summaries and mocks can contain functions to generalize for verification and mocks, respectively.

Rule Verification and Output

After setting up configuration, we can add mutants to mutations/ folder and list them in our config with the mutations option.

"mutations": {
"manual_mutants": [
{
"file_to_mutate": "../src/backstop/user.rs",
"mutants_location": "../mutations/user"
}
]
}

Now we can start mutation testing with certoraMutate user_verified.conf. To test rules on original code only we may run certoraSorobanProver user_verified.conf.

On the mutation testing page, you’ll see caught mutants on the right and rules on the left.

Rule queue_shares_for_withdrawal_correct catches mutant user_1.rs that breaks balance logic for queuing shares.

pub fn queue_shares_for_withdrawal(&mut self, e: &Env, to_q: i128) {
if self.shares < to_q {
panic_with_error!(e, BackstopError::BalanceError);
}
if self.q4w.len() >= MAX_Q4W_SIZE {
panic_with_error!(e, BackstopError::TooManyQ4WEntries);
}
self.shares = self.shares + to_q; // MUTANT

// user has enough tokens to withdrawal, add Q4W
let new_q4w = Q4W {
amount: to_q,
exp: e.ledger().timestamp() + Q4W_LOCK_TIME,
};
self.q4w.push_back(new_q4w.clone());
}

Rule withdraw_shares_balance_error_fails catches mutant user_3.rs that breaks withdrawal logic in.

A successful mutation test run requires rules to pass on the original code (in other words, the specification should not flag any issues in the original contract).

More Insights

In this article, we touched only on writing Cavalier rules in Certora Sunbeam Prover. This approach enables mutation testing and basic function property checks. For deeper formal verification, consider using invariants and parameterized rules — automatic setup for these kind of properties is not yet in Sunbeam.

Users may also encounter timeouts when verifying complex Soroban functions. In such cases, I recommend breaking the verification tasks into smaller pieces (for example, putting each rule in its own configuration file) and using the smt_timeout and global_timeout flags, and/or other relevant CLI options. It also helps to simplify the rules themselves wherever possible. For instance, you can use ghost variables to avoid extra storage accesses (as we did in some of our Blend backstop rules). For deeper learning, I suggest watching the Certora webinar and studying the related documentation page.

Conclusion

Today, we explored a new tool for formal verification of smart contracts on Stellar — Certora Sunbeam Prover. Our team is convinced that formal methods are essential for DeFi protocol security: only rigorous mathematical guarantees can prevent hacks and multi-million-dollar losses. That’s why we never miss opportunities to try new formal verification tools and conduct our own research in this area.

---

Formal Methods for Stellar DeFi: Verifying Lending Protocol with Certora Sunbeam Prover was originally published in Positive Web3 on Medium, where people are continuing the conversation by highlighting and responding to this story.

The post Formal Methods for Stellar DeFi: Verifying Lending Protocol with Certora Sunbeam Prover appeared first on Security Boulevard.

>>More