synor/formal/kani

Kani Formal Verification for Synor

This directory contains Kani model checking proofs for critical Synor components.

What is Kani?

Kani is a bit-precise model checker for Rust. It can verify that Rust programs are free of:

• Runtime panics
• Memory safety issues
• Assertion violations
• Undefined behavior

Unlike property testing (proptest), Kani exhaustively checks all possible inputs within defined bounds.

Installation

# Install Kani
cargo install --locked kani-verifier
kani setup

Running Proofs

# Run all Kani proofs in a crate
cd crates/synor-consensus
kani --tests

# Run specific proof
kani --harness utxo_add_never_overflows

# Run with bounded loops (for performance)
kani --harness utxo_conservation --default-unwind 10

Proof Structure

Each proof harness:

1. Uses kani::any() to generate arbitrary inputs
2. Sets up preconditions with kani::assume()
3. Executes the code under test
4. Asserts postconditions with kani::assert() or standard assert!

Proofs Included

UTXO Module (crates/synor-consensus/src/utxo_kani.rs)

• utxo_add_never_overflows - Adding UTXOs cannot overflow total value
• utxo_conservation - Total value is conserved across operations
• utxo_no_double_spend - Same outpoint cannot exist twice

Difficulty Module (crates/synor-consensus/src/difficulty_kani.rs)

• difficulty_bits_roundtrip - bits conversion is approximately reversible
• difficulty_bounded_adjustment - adjustment stays within bounds
• target_difficulty_inverse - higher difficulty = smaller target

Amount Module (crates/synor-types/src/amount_kani.rs)

• amount_checked_add_sound - checked_add returns None on overflow
• amount_saturating_sub_bounded - saturating_sub never exceeds original
• amount_max_supply_respected - operations respect MAX_SUPPLY

CI Integration

Add to .github/workflows/kani.yml:

name: Kani Verification
on: [push, pull_request]

jobs:
  kani:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: model-checking/kani-github-action@v1
      - run: kani --tests --workspace

Writing New Proofs

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

    #[kani::proof]
    fn my_function_never_panics() {
        let input: u64 = kani::any();
        // Preconditions
        kani::assume(input < MAX_VALUE);

        // Code under test
        let result = my_function(input);

        // Postconditions
        assert!(result.is_ok());
    }
}

Limitations

• Kani has bounded model checking, so loops need unwinding limits
• Complex floating point is approximated
• External FFI calls are stubbed
• Network/filesystem operations are not verified

References

• Kani Documentation
• AWS Kani Blog
• Kani GitHub