Formal Verification

The MOVE prover allows for formal specifications to be written on MOVE code, which can provide guarantees on function behavior.

During the audit period, we provided Move Labs with Move prover specifications, a form of formal verification. We found the prover to be highly effective at evaluating the entirety of certain functions' behavior and recommend the Move Labs team to add more specifications to their code base.

One of the issues we encountered was that the prover does not support recursive code yet. We suggest replacing the recursive functions, specifically the math::pow functions to a loop form so additional specs can be written on the project.

The following is a sample of the specifications provided.

tortuga::stake_router

Verifies the result is a multiplication-divide:

spec calc_shares_to_value {
    requires t_apt_supply != 0;
    aborts_if t_apt_supply < num_shares;
    ensures result <= MAX_U64;
    ensures result == num_shares * total_worth / t_apt_supply;
}

Verifies the following resources are created upon initialization:

spec initialize_tortuga_liquid_staking  {
    ensures exists<StakedAptosCapabilities>(signer::address_of(tortuga));
    ensures exists<StakingStatus>(signer::address_of(tortuga));
    ensures exists<validator_router::Status>(signer::address_of(tortuga));
    ensures exists<validator_router::DelegationAccounts>(signer::address_of(tortuga));
}

Verifies values were mutated:

spec set_min_transaction_amount {
    ensures borrow_global_mut<StakingStatus>(signer::address_of(tortuga)).min_transaction_amount == value;
}

spec set_cooldown_period {
    ensures borrow_global_mut<StakingStatus>(signer::address_of(tortuga)).cooldown_period == value;
}

spec set_reward_commission {
    ensures borrow_global_mut<StakingStatus>(signer::address_of(tortuga)).reward_commission == value;
}

helpers::circular_buffer

Verifies the buffer always contains the latest value pushed:

spec push {
    ensures len(old(cbuffer.buffer)) < max_length && cbuffer.last_index + 1 > len(cbuffer.buffer) ==> contains(cbuffer.buffer, value);
}

Verifies the empty function returns an empty buffer:

spec empty {
    ensures len(result.buffer) == 0;
    ensures result.last_index == 0;
}

Verifies the length of cbuffer:

spec length {
    ensures len(cbuffer.buffer) == result;
}

Verifies borrow_oldest and round_robin behavior:

spec fun helper_round_robin(a: u64, b: u64): u64 {
    assert!(b > 0 && a <= b, error::invalid_argument(EARITHMETIC_ERROR));
    if (a < b) {
        a
    }
    else {
        0
    }
}
spec round_robin {
    aborts_if b > 0 || a <= b;
}

spec borrow_oldest {
    // Verifies behavior about the borrow_oldest function in circular_buffer
    aborts_if cbuffer.last_index + 1 > len(cbuffer.buffer);
    aborts_if len(cbuffer.buffer) == 0;
    let oldest_index = helper_round_robin(cbuffer.last_index +1, len(cbuffer.buffer));
    ensures result == cbuffer.buffer[oldest_index];
}

tortuga::staked_aptos_coin

Verifies StakedAptosCoin exists after initialization:

spec register_for_t_apt {
    ensures exists<coin::CoinStore<StakedAptosCoin>>(signer::address_of(account));
}

helpers::math

Verifies when mul_div aborts and the resulting output:

spec mul_div {
    aborts_if c == 0;
    aborts_if a * b / c > MAX_U64;
    ensures result <= MAX_U64;
}

Verifies it never aborts, thus actually safe:

spec safe_sub_u128 {
    aborts_if false;
}