TLA+ Specs (docs/internals/specs/tla/*.tla)
                    │ mirrors
         Shared Invariants (invariants/)  ← SINGLE SOURCE OF TRUTH
                    │ used by
    ┌───────────────┼───────────────┬─────────────────────┐
    ▼               ▼               ▼                     ▼
Stateright      DST Tests      Integration          Production Metrics
(exhaustive)    (simulation)   Tests                (Observability)

1. Read TLA+ spec       → Understand invariants
2. Write DST tests      → Encode invariants as executable tests
3. Run tests            → EXPECT FAILURE (no implementation yet)
4. Implement code       → Make tests pass
5. Verify all layers    → DST + Stateright + unit tests
6. Create PR            → Include verification evidence

# Run all DST tests (once the DST crate exists)
cargo test -p quickwit-dst

# Reproduce failure with specific seed
DST_SEED=12345 cargo test -p quickwit-dst

# Verbose fault logging
RUST_LOG=quickwit_dst=debug cargo test -p quickwit-dst

use quickwit_dst::{Simulation, SimConfig, FaultConfig, FaultType};

#[test]
fn test_with_faults() {
    let config = SimConfig::new(12345); // Deterministic seed
    let mut sim = Simulation::new(config)
        .with_fault(FaultConfig::new(FaultType::StorageWriteFail, 0.1));

    sim.run(|env| async move {
        let storage = env.storage();
        // Test logic - fully deterministic
        Ok(())
    }).unwrap();
}

Ingest → Query → Compact → GC → Query Again

                  Runtime Trait
                       │
         ┌─────────────┼─────────────┐
         ▼             ▼             ▼
   SystemRuntime  SimRuntime   (future runtimes)
   (production)   (simulation)

// WRONG: Bypasses Runtime, breaks DST
let now = Instant::now();
let now = Utc::now();
tokio::time::sleep(duration).await;
let rng = thread_rng();

// CORRECT: Goes through Runtime, DST-compliant
let now = runtime.clock().now_instant();
let now = runtime.clock().now();
runtime.clock().sleep(duration).await;
let val = runtime.rng().next_u64();

# DST Bug #NNN: Description

**Status**: Fixed/Open
**Discovered**: YYYY-MM-DD
**Seeds**: comma-separated failing seeds
**Component**: crate::module

## Summary
## Reproduction
## Root Cause
## Fix
## Verification
## Lessons Learned

// Both DST and production code use the same invariant definitions
use quickwit_invariants::{SplitPropertyChecker, PropertyChecker};

let checker = SplitPropertyChecker::new(&state);
let result = checker.no_lost_splits();

if !result.holds {
    println!("{}", result);
    // no_lost_splits: Split abc123 not visible in metastore
}

# Run Stateright model checking
cargo test -p quickwit-dst stateright -- --ignored

impl Model for SplitLifecycleModel {
    type State = SplitState;
    type Action = SplitAction;

    fn init_states(&self) -> Vec<Self::State> { ... }
    fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) { ... }
    fn next_state(&self, state: &Self::State, action: Self::Action) -> Option<Self::State> { ... }

    fn properties(&self) -> Vec<Property<Self>> {
        vec![
            Property::always("no_lost_splits", |_, state| {
                let checker = SplitPropertyChecker::new(state);
                checker.no_lost_splits().holds
            }),
        ]
    }
}

# All proofs
cargo kani

# Specific crate
cargo kani --package quickwit-metastore

# Specific proof
cargo kani --package quickwit-metastore --harness verify_no_lost_splits

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

    #[kani::proof]
    #[kani::unwind(10)]  // Bound loops
    fn verify_my_invariant() {
        let input: u64 = kani::any();
        kani::assume(input > 0);

        let result = my_function(input);

        kani::assert(result > input, "Result must exceed input");
    }
}

// Record invariant check in production
quickwit_observability::record_invariant("no_lost_splits", passed);

// 1. Add verification method
impl SplitMetastore {
    async fn verify_no_lost_splits(&self, ...) -> bool {
        // Check condition
    }
}

// 2. Call record_invariant after operation
let passed = self.verify_no_lost_splits(...).await;
quickwit_observability::record_invariant("no_lost_splits", passed);