Crate moloch_verify 

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());

Re-exports

pub use invariants::BlockInvariant;

pub use invariants::ChainInvariants;

pub use invariants::EventInvariant;

pub use invariants::Invariant;

pub use invariants::InvariantViolation;

pub use invariants::MmrInvariant;

pub use properties::Property;

pub use properties::PropertyResult;

pub use properties::PropertyTest;

pub use runtime::CheckResult;

pub use runtime::RuntimeCheck;

pub use runtime::RuntimeMonitor;

pub use specs::SpecViolation;

pub use specs::Specification;

Modules

invariants

Chain invariants for formal verification.

prelude

Prelude for convenient imports.

properties

Property-based testing for chain operations.

runtime

Runtime invariant checking and monitoring.

specs

Formal specifications for chain behavior.

Traits

ChainState

Trait for chain state that can be verified.

Functions

verify_transition

Verify a state transition satisfies all invariants.