|
| 1 | +--- |
| 2 | +description: "Verification-first development workflow with TLA+ specs, DST, and formal methods. Use when you want Claude to follow the rigorous plan→spec→test→implement sequence." |
| 3 | +user-invocable: true |
| 4 | +--- |
| 5 | + |
| 6 | +# Sesh Mode — Verification-First Development |
| 7 | + |
| 8 | +Activate this mode when working on features that touch state machines, protocols, or critical data paths. This adds formal verification requirements on top of the base CLAUDE.md. |
| 9 | + |
| 10 | +## Before Writing Any Code |
| 11 | + |
| 12 | +**MUST** follow this sequence before implementation: |
| 13 | + |
| 14 | +1. **Define the plan**: What are you doing and why? What invariants must hold? |
| 15 | +2. **Check ADR/roadmap**: `docs/internals/adr/README.md` → find relevant supplement |
| 16 | +3. **Read the spec**: If touching state machines or protocols, read `docs/internals/specs/tla/*.tla` |
| 17 | +4. **Write tests first**: DST tests define correctness, write them before code |
| 18 | +5. **Only then**: Start implementation |
| 19 | + |
| 20 | +## Three Engineering Pillars |
| 21 | + |
| 22 | +Every code change **MUST** respect all three: |
| 23 | + |
| 24 | +| Pillar | Location | Purpose | |
| 25 | +|--------|----------|---------| |
| 26 | +| **Code Quality** | [CODE_STYLE.md](../../../CODE_STYLE.md) + CLAUDE.md | Coding standards & reliability | |
| 27 | +| **Formal Specs** | `docs/internals/specs/tla/`, `stateright_*.rs` | Protocol correctness | |
| 28 | +| **DST** | DST crate (when created) | Fault tolerance | |
| 29 | + |
| 30 | +**Priority**: Safety > Performance > Developer Experience |
| 31 | + |
| 32 | +## The Verification Pyramid |
| 33 | + |
| 34 | +All verification layers share the same invariants: |
| 35 | + |
| 36 | +``` |
| 37 | + TLA+ Specs (docs/internals/specs/tla/*.tla) |
| 38 | + │ mirrors |
| 39 | + Shared Invariants (invariants/) ← SINGLE SOURCE |
| 40 | + │ used by |
| 41 | + ┌───────────────┼───────────────┐ |
| 42 | + ▼ ▼ ▼ |
| 43 | +Stateright DST Tests Production Metrics |
| 44 | +(exhaustive) (simulation) (Observability) |
| 45 | +``` |
| 46 | + |
| 47 | +## Testing Through Production Path |
| 48 | + |
| 49 | +**MUST NOT** claim a feature works unless tested through the actual network stack. |
| 50 | + |
| 51 | +```bash |
| 52 | +# 1. Start quickwit |
| 53 | +cargo run -p quickwit-cli -- run --config ../config/quickwit.yaml |
| 54 | + |
| 55 | +# 2. Ingest via OTLP |
| 56 | +# (send logs/traces to localhost:4317) |
| 57 | + |
| 58 | +# 3. Query via REST API |
| 59 | +curl http://localhost:7280/api/v1/<index>/search -d '{"query": "*"}' |
| 60 | +``` |
| 61 | + |
| 62 | +**Bypasses to AVOID**: Testing indexing pipeline without the HTTP/gRPC server, testing search without the REST API layer. |
| 63 | + |
| 64 | +## DST (Deterministic Simulation Testing) |
| 65 | + |
| 66 | +- DST tests define correctness for stateful components |
| 67 | +- Write DST tests before implementation for new state machines |
| 68 | +- Shared invariants are the single source of truth across all verification layers |
| 69 | + |
| 70 | +## Architecture Evolution |
| 71 | + |
| 72 | +Quickwit tracks architectural change through three lenses. See `docs/internals/adr/EVOLUTION.md` for the full process. |
| 73 | + |
| 74 | +``` |
| 75 | + Architecture Evolution |
| 76 | + │ |
| 77 | + ┌────────────────────┼────────────────────┐ |
| 78 | + ▼ ▼ ▼ |
| 79 | + Characteristics Gaps Deviations |
| 80 | + (Proactive) (Reactive) (Pragmatic) |
| 81 | + "What we need" "What we learned" "What we accepted" |
| 82 | +``` |
| 83 | + |
| 84 | +| Lens | Location | When to Use | |
| 85 | +|------|----------|-------------| |
| 86 | +| **Characteristics** | `docs/internals/adr/` | Track cloud-native requirements | |
| 87 | +| **Gaps** | `docs/internals/adr/gaps/` | Design limitation from incident/production | |
| 88 | +| **Deviations** | `docs/internals/adr/deviations/` | Intentional divergence from ADR intent | |
| 89 | + |
| 90 | +**Before implementing, check for**: |
| 91 | +- Open gaps (design limitations to be aware of) |
| 92 | +- Deviations (intentional divergence from ADRs) |
| 93 | +- Characteristic status (what's implemented vs planned) |
| 94 | + |
| 95 | +## Additional Commit Checklist (on top of CLAUDE.md MUST items) |
| 96 | + |
| 97 | +These are expected unless justified: |
| 98 | +- [ ] Functions under 70 lines |
| 99 | +- [ ] Explanatory variables for complex expressions |
| 100 | +- [ ] Documentation explains "why" |
| 101 | +- [ ] ADR/roadmap updated if applicable |
| 102 | +- [ ] DST test for new state transitions |
| 103 | +- [ ] Integration test for new API endpoints |
| 104 | +- [ ] Tests through production path (HTTP/gRPC) |
| 105 | + |
| 106 | +## Reference Documentation |
| 107 | + |
| 108 | +| Topic | Location | |
| 109 | +|-------|----------| |
| 110 | +| Verification & DST | [docs/internals/VERIFICATION.md](../../../docs/internals/VERIFICATION.md) | |
| 111 | +| Verification philosophy | [docs/internals/VERIFICATION_STACK.md](../../../docs/internals/VERIFICATION_STACK.md) | |
| 112 | +| Simulation workflow | [docs/internals/SIMULATION_FIRST_WORKFLOW.md](../../../docs/internals/SIMULATION_FIRST_WORKFLOW.md) | |
| 113 | +| Benchmarking | [docs/internals/BENCHMARKING.md](../../../docs/internals/BENCHMARKING.md) | |
| 114 | +| Rust style patterns | [docs/internals/RUST_STYLE.md](../../../docs/internals/RUST_STYLE.md) | |
| 115 | +| ADR index | [docs/internals/adr/README.md](../../../docs/internals/adr/README.md) | |
| 116 | +| Architecture evolution | [docs/internals/adr/EVOLUTION.md](../../../docs/internals/adr/EVOLUTION.md) | |
| 117 | +| Compaction architecture | [docs/internals/compaction-architecture.md](../../../docs/internals/compaction-architecture.md) | |
| 118 | +| Tantivy + Parquet design | [docs/internals/tantivy-parquet-architecture.md](../../../docs/internals/tantivy-parquet-architecture.md) | |
| 119 | +| Locality compaction | [docs/internals/locality-compaction/](../../../docs/internals/locality-compaction/) | |
0 commit comments