Formal Verification for Moloch Audit Chain.

Provides compile-time and runtime verification of chain invariants.

Architecture

┌─────────────────────────────────────────────────────────────────────┐
│                     VERIFICATION LAYER                               │
│                                                                      │
│  ┌───────────────────────────────────────────────────────────────┐  │
│  │ INVARIANTS                                                     │  │
│  │  - Chain invariants (append-only, monotonic height)            │  │
│  │  - Event invariants (valid signatures, unique IDs)             │  │
│  │  - MMR invariants (consistent roots, valid proofs)             │  │
│  └───────────────────────────────────────────────────────────────┘  │
│                                                                      │
│  ┌───────────────────────────────────────────────────────────────┐  │
│  │ PROPERTY-BASED TESTING                                         │  │
│  │  - QuickCheck-style property testing                           │  │
│  │  - Shrinking for minimal counterexamples                       │  │
│  │  - Deterministic replay                                        │  │
│  └───────────────────────────────────────────────────────────────┘  │
│                                                                      │
│  ┌───────────────────────────────────────────────────────────────┐  │
│  │ RUNTIME CHECKS                                                 │  │
│  │  - Pre/post condition assertions                               │  │
│  │  - State transition validation                                 │  │
│  │  - Consistency monitors                                        │  │
│  └───────────────────────────────────────────────────────────────┘  │
└─────────────────────────────────────────────────────────────────────┘

Example

use moloch_verify::{Invariant, ChainInvariants, verify_transition};

// Define chain invariants
let invariants = ChainInvariants::new()
    .require_monotonic_height()
    .require_append_only()
    .require_valid_signatures();

// Verify a state transition
let result = verify_transition(&old_state, &new_state, &invariants);
assert!(result.is_ok());