Use when sanity-checking coordination changes before commit, before merging coordination PRs, when a coordination bug is suspected, or when verifying a simulation-found fix. Progressive DST execution with seed management and fault injection.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
Use when sanity-checking coordination changes before commit, before merging coordination PRs, when a coordination bug is suspected, or when verifying a simulation-found fix. Progressive DST execution with seed management and fault injection.
user-invocable
true
Run Deterministic Simulation Tests
Execute simulation tests with progressive difficulty levels, inspired by
TigerBeetle's VOPR three-level system. Manages seeds, selects workloads,
injects faults, and reports invariant violations.
Storage corruption, cascading failures, Byzantine faults, all Level 2 combined
1000+
Pre-release, deep exploration
If the user doesn't specify a level:
Default to Level 1 for quick checks
Recommend Level 2 if the change touches lease/fence/split logic
Recommend Level 3 if the change is a significant architectural modification
Step 2: Select Workload Templates
Each workload template exercises a specific coordination scenario. Select all
that are relevant to the changed code, or run all for comprehensive coverage.
Template
Exercises
Priority
Full scan lifecycle
Acquire โ checkpoint x N โ complete
ALWAYS
Lease expiry during checkpoint
Acquire โ delay โ checkpoint with stale lease
HIGH โ etcd Jepsen 3.4.3 pattern
Split during active scan
Acquire โ checkpoint โ split โ verify children
HIGH โ shard coverage invariant
Concurrent acquisition
2+ workers acquire same shard
HIGH โ fence monotonicity
Ambiguous failure
Network drop after mutation succeeds
MED โ Jepsen Redis-Raft pattern
Park and unpark
Active โ Parked โ Active (reacquire)
MED โ state machine completeness
Mass restart
All workers restart simultaneously
MED โ Serf/memberlist edge case
Asymmetric partition
AโB works, BโA drops
LOW โ Lifeguard false positives
Step 3: Run Simulation
Execute tests with the selected level and seeds:
# Level 1 (Sunny Day) โ quick sanity check
cargo test --features test-support -- --test-threads=1 sim::level1
# Level 2 (Stormy) โ fault injection
SIM_SEEDS=100 SIM_LEVEL=2 cargo test --features test-support -- --test-threads=1 sim::level2
# Level 3 (Radioactive) โ maximum chaos
SIM_SEEDS=1000 SIM_LEVEL=3 cargo test --features test-support -- --test-threads=1 sim::level3
# Reproduce a specific failure
SIM_SEED=12345 cargo test --features test-support -- --test-threads=1 sim::specific_test
Key flags:
--test-threads=1: Required for deterministic execution (no thread interleaving)
SIM_SEEDS: Number of random seeds to explore
SIM_LEVEL: Fault injection intensity
SIM_SEED: Specific seed for reproduction
Step 4: Analyze Results
On success (all seeds pass):
SIMULATION REPORT โ Level {N}
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
Result: PASS
Seeds tested: {count}
Wall time: {duration}
Sim time: {total simulated time}
Time compression: {sim_time / wall_time}x
Workload coverage:
[x] Full scan lifecycle โ {N} occurrences
[x] Lease expiry during checkpoint โ {N} occurrences
[x] Split during active scan โ {N} occurrences
[x] Concurrent acquisition โ {N} occurrences
[ ] Asymmetric partition โ 0 occurrences (not exercised)
Invariants verified:
- Mutual exclusion (lease) โ checked {N} times
- Fence monotonicity โ checked {N} times
- Shard coverage (no gaps) โ checked {N} times
- Terminal irreversibility โ checked {N} times
Minimize: Use proptest shrinking to find the minimal reproduction case
Classify: Is this a real bug or a simulation artifact?
Root cause: Trace the failure to specific code
Fix: Apply the fix
Verify: Re-run with the failing seed AND fresh seeds
Do NOT save the specific seed as a regression test โ seeds break on
code changes (Eaton, Antithesis). Instead, ensure the invariant check
catches the class of bug under continuous exploration.
Step 6: Coverage Assessment
After the run, assess workload coverage:
Well-covered: Workload generated sufficient occurrences across seeds
Under-covered: Workload generated fewer than 5 occurrences across all seeds
โ May need to tune workload generation probabilities
Not exercised: Workload never triggered
โ May need explicit workload scenario or higher seed count
If critical workloads are under-covered, recommend:
Increasing seed count
Adding targeted workload scenarios
Adjusting fault injection probabilities
Fault Injection Reference
Level 2 (Stormy) Faults
Fault
Description
Implementation
Network partition
Messages between node subsets are dropped
NetworkFaults.partitions
Message loss
Random message drops (10-30%)
NetworkFaults.drop_rate
Message reorder
Messages arrive out of order
Random delay in event queue
Lease expiry
Force lease timeout mid-operation
Advance clock past lease deadline
Process pause
Freeze a worker for N ticks
Skip node in simulation loop
Clock skew
Nodes disagree on current time
Per-node clock offset
Level 3 (Radioactive) Faults
All Level 2 faults plus:
Fault
Description
Implementation
Storage corruption
Backend returns garbage data
Mock backend returns corrupted state
Cascading failure
Failure of one node triggers failures in others
Fault propagation rules
Byzantine
Node sends conflicting messages to different peers
Duplicate + modify messages
Split brain
Two partitions each believe they're the majority
Symmetric partition
Repeated crash-restart
Node crashes and restarts multiple times
Reset node state periodically
Invariant Catalog
These are the core invariants that every simulation run must verify. They map
to the phase 2 spec invariant catalog.
ID
Invariant
Check
S1
Mutual exclusion โ at most one active lease per shard
Count active leases per shard โค 1
S2
Fence monotonicity โ epochs never decrease
Track max epoch per shard, assert non-decreasing
S3
Terminal irreversibility โ Done/Failed shards never transition
Assert no transitions from terminal states
S4
Shard coverage โ split children cover parent range exactly
Verify range algebra on split
S5
Idempotency โ duplicate OpId returns same result
Replay operations, assert identical results
S6
Progress โ under fair scheduling, work eventually completes
Assert completion within bounded time
L1
Lease exclusivity โ stale-epoch checkpoints are rejected
Attempt checkpoint with old epoch, assert rejection
L2
Zombie rejection โ restarted worker cannot use old lease
Kill and restart worker, assert old operations fail
