Formal Verification of Soroban Contracts with Kani

// contracts/kani-poc/src/lib.rs — verified with Kani, pure primitives only

/// Attempt to initialise the token contract.
pub fn initialize_pure(is_initialized: bool) -> Result<(), &'static str> {
    if is_initialized {
        return Err("already initialized");
    }
    Ok(())
}

/// Transfer: deduct from sender, add to receiver.
pub fn transfer_pure(
    balance_from: i128,
    balance_to: i128,
    amount: i128,
) -> Result<(i128, i128), &'static str> {
    if amount <= 0 {
        return Err("Amount must be positive");
    }
    let new_from = balance_from
        .checked_sub(amount)
        .ok_or("Insufficient balance")?;
    let new_to = balance_to
        .checked_add(amount)
        .ok_or("Receiver balance overflow")?;
    Ok((new_from, new_to))
}

/// Mint: add to a balance.
pub fn mint_pure(balance: i128, amount: i128) -> Result<i128, &'static str> {
    if amount <= 0 {
        return Err("Mint amount must be positive");
    }
    balance.checked_add(amount).ok_or("Mint overflow")
}

/// Burn: subtract from a balance.
pub fn burn_pure(balance: i128, amount: i128) -> Result<i128, &'static str> {
    if amount <= 0 {
        return Err("Burn amount must be positive");
    }
    balance
        .checked_sub(amount)
        .ok_or("Insufficient balance to burn")
}

// contracts/kani-poc/src/lib.rs — NOT verified, uses Host types
#[contractimpl]
impl TokenContract {
    pub fn initialize(env: Env, _name: Symbol) {
        let already: bool = env
            .storage()
            .instance()
            .get(&symbol_short!("init"))
            .unwrap_or(false);
        initialize_pure(already).expect("already initialized");
        env.storage().instance().set(&symbol_short!("init"), &true);
    }

    // set_admin uses Env and Symbol — Kani cannot verify this
    pub fn set_admin(env: Env, new_admin: Symbol) {
        env.storage()
            .instance()
            .set(&symbol_short!("admin"), &new_admin);
    }
}

#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    fn verify_transfer_pure_conservation() {
        let balance_from: i128 = kani::any();
        let balance_to: i128 = kani::any();
        let amount: i128 = kani::any();

        kani::assume(amount > 0);
        kani::assume(balance_from >= amount);
        kani::assume(balance_from <= i128::MAX);
        kani::assume(balance_to >= 0);
        kani::assume(balance_to <= i128::MAX - amount);
        kani::assume(balance_from <= i128::MAX - balance_to);

        let Ok((new_from, new_to)) = transfer_pure(balance_from, balance_to, amount) else {
            panic!("transfer_pure failed despite valid preconditions");
        };

        assert!(new_from == balance_from - amount);
        assert!(new_to == balance_to + amount);
        assert!(
            new_from + new_to == balance_from + balance_to,
            "Conservation of supply"
        );
    }
}