Powered by Otters.

Replace:

anchor-lang = "0.26.0"

with

anchor-lang = { package = "onchor", git = "[email protected]:otter-sec/verify.git" }

Otter formal verification for Solana only works on rust code that is using the nightly toolchain. So create a new file rust-toolchain in the root of your project with the following contents:

[toolchain]
channel = "nightly"

Then, add the otter-solana-verify to your Cargo.toml dependencies:

cargo add otter-solana-verify

Invariants are properties that should always be true. For example, the balance of a token account should never be negative. There are two types of invariants in the Solana programs: account invariants and instruction invariants.

An instruction invariant specifies sufficient conditions for an instruction to succeed (or fail). These are specified as succeeds_if or errors_if macro annotations on the instruction handler.

• succeeds_if - The instruction should succeed if and only if the given condition is true.

#[succeeds_if(
    ctx.user.balance > amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
    // ...
}

• errors_if - The instruction should fail if and only if the given condition is true.

#[errors_if(
    ctx.user.balance < amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
    // ...
}

The other type of invariant is an Account Invariant. This invariant describes some property of an account that should always hold. We use the invariant macro to specify these invariants.

• invariant - The account invariant should hold if and only if the given condition is true.

#[account]
#[invariant(
    self.balance >= 0
)]
struct User {
    pub balance: i64,
}