# Synor Formal Verification

This directory contains formal verification artifacts for the Synor blockchain.

## Overview

Formal verification provides mathematical proofs that critical system properties hold for **all possible inputs**, not just tested examples.

## Verification Layers

| Layer | Tool | What It Verifies |
|-------|------|------------------|
| **Specification** | TLA+ | State machine invariants |
| **Code** | Kani | Rust implementation correctness |
| **Property** | Proptest | Random input testing |
| **Mathematical** | Proofs | Algorithm correctness |

## Directory Structure

```
formal/
├── tla/                      # TLA+ specifications
│   ├── UTXOConservation.tla  # UTXO value conservation
│   └── GHOSTDAGOrdering.tla  # DAG ordering determinism
├── kani/                     # Kani proof harnesses
│   └── README.md             # How to use Kani
└── proofs/                   # Mathematical proofs
    └── DifficultyConvergence.md
```

## Critical Invariants Verified

### 1. UTXO Conservation
**Property:** Total value of UTXOs equals total minted (coinbase) minus fees.

**Verification:**
- [x] TLA+ specification (`tla/UTXOConservation.tla`)
- [x] Property testing (`crates/synor-consensus/tests/property_tests.rs`)
- [ ] Kani proofs (TODO)

### 2. No Double-Spend
**Property:** Each UTXO can only be spent once.

**Verification:**
- [x] TLA+ specification (in UTXOConservation.tla)
- [x] Property testing (utxo_add_remove_identity)
- [x] Unit tests

### 3. DAG Ordering Determinism
**Property:** Given the same DAG, all nodes compute identical blue sets and ordering.

**Verification:**
- [x] TLA+ specification (`tla/GHOSTDAGOrdering.tla`)
- [x] Unit tests (65 tests in synor-dag)

### 4. Difficulty Convergence
**Property:** Under stable hashrate, block time converges to target.

**Verification:**
- [x] Mathematical proof (`proofs/DifficultyConvergence.md`)
- [x] Property testing (difficulty_adjustment_bounded)

### 5. Supply Bounded
**Property:** Total supply never exceeds MAX_SUPPLY (21M).

**Verification:**
- [x] TLA+ specification (SupplyBounded invariant)
- [x] Property testing (amount tests)
- [x] Compile-time enforcement

## Running Verification

### TLA+ (TLC Model Checker)

```bash
# Install TLA+ Toolbox or use CLI
tlc formal/tla/UTXOConservation.tla

# Or use online version: https://lamport.azurewebsites.net/tla/toolbox.html
```

### Property Tests

```bash
cargo test -p synor-consensus property
```

### Kani (when installed)

```bash
cargo install --locked kani-verifier
kani setup

cd crates/synor-consensus
kani --tests
```

## Verification Status

| Component | Property | TLA+ | Kani | Proptest | Math |
|-----------|----------|:----:|:----:|:--------:|:----:|
| UTXO | Conservation | ✅ | ⏳ | ✅ | - |
| UTXO | No double-spend | ✅ | ⏳ | ✅ | - |
| DAG | Ordering determinism | ✅ | ⏳ | - | - |
| Difficulty | Convergence | - | - | ✅ | ✅ |
| Difficulty | Bounded adjustment | - | - | ✅ | ✅ |
| Amount | Overflow safety | - | ⏳ | ✅ | - |

Legend: ✅ Done | ⏳ Planned | - Not applicable

## Next Steps

1. **Install Kani** and add proof harnesses to each crate
2. **Run TLC** on TLA+ specs with small model
3. **CI Integration** for property tests and Kani
4. **Expand proofs** for network layer properties

## References

- [TLA+ Hyperbook](https://lamport.azurewebsites.net/tla/hyperbook.html)
- [Kani Documentation](https://model-checking.github.io/kani/)
- [Proptest Book](https://altsysrq.github.io/proptest-book/)
- [Amazon S3 ShardStore TLA+](https://github.com/awslabs/aws-s3-tla)