# 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

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

## Running Proofs

```bash
# 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`:

```yaml
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

```rust
#[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](https://model-checking.github.io/kani/)
- [AWS Kani Blog](https://aws.amazon.com/blogs/opensource/how-we-use-kani/)
- [Kani GitHub](https://github.com/model-checking/kani)