Formal Verification

The MOVE prover allows for formal specifications to be written on MOVE code, which can provide guarantees on function behavior as these specifications are exhaustive on every possible input case.

During the audit period, we provided Laminar 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 Laminar 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 and thus such places had to be ignored. Nevertheless, recursive support is coming prompty as seen in this commit here↗.

The following is a sample of the specifications provided.

dex::order

Verifies setter functions:

spec set_size {
    aborts_if false;
    ensures order.size == size;
}

spec set_price {
    aborts_if false;
    ensures order.price == price;
}

dex::instrument

Verifies resources exist and return value upon function invocation:

spec create {
    ensures result.price_decimals == price_decimals;
    ensures exists<coin::CoinStore<Base>>(signer::address_of(account));
    ensures exists<coin::CoinStore<Quote>>(signer::address_of(account));
}

dex::coin

Verifies coin of type T exists after registration:

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

flow::guarded_idx

Verifies when guards behavior:

spec guard {
    aborts_if value == SENTINEL_VALUE;
    ensures result == GuardedIdx {value};
}

spec unguard {
    aborts_if is_sentinel(guard);
    ensures result == guard.value;
}

spec try_guard {
    aborts_if false;
    ensures value != SENTINEL_VALUE ==> result == GuardedIdx {value};
}

spec fun spec_none<Element>(): Option<Element> {
    Option{ vec: vec() }
}
spec fun spec_some<Element>(e: Element): Option<Element> {
    Option{ vec: vec(e) }
}

spec try_unguard {
    ensures guard.value == SENTINEL_VALUE ==> result == spec_none();
    ensures guard.value != SENTINEL_VALUE ==> result == spec_some(guard.value);
}

flow::queue

Verifies nodes are initialized correctly:

spec create_node {
    ensures result == Node<V> {
        value: spec_some(value),
        next: guarded_idx::sentinel()
    };
}

Verifies peeking behavior for the queue:

spec fun spec_some<Element>(e: Element): Option<Element> {
    Option{ vec: vec(e) }
}


spec peek_iter_index {
    ensures (guarded_idx::is_sentinel(iter.current)) ==> result == option::none();
    ensures !(guarded_idx::is_sentinel(iter.current)) ==> result == spec_some(guarded_idx::unguard(iter.current));
}