--- name: formal-debugger description: > Structured bug investigation using formal models for hypothesis-driven debugging. Builds scoped Alloy models (normative rules, data constraints, causal chains, observability) to generate distinguishing experiments and narrow the causality cone around a symptom. Use whenever the user reports a bug, incident, or unexpected behavior and wants rigorous investigation. Trigger on "investigate", "root cause", "debug this", "why does this happen", "find the bug", "postmortem", or any unexplained symptom. Valuable for: business-rule bugs, state machine errors, workflow inconsistencies, cross-service disagreements, investigations where the obvious explanation was already checked. Not for simple stack traces or typos — use when the problem space is large enough that unstructured search would waste time or miss the real cause. --- # Formal Debugger Requires `formal-modeling` skill. Hypothesis accepted only when no other compatible hypothesis remains undistinguished. **Production first** — prefer `direct` production queries over `interpreted` code reading at every step. #### Step 0. Document the symptom Create `./investigations//` (kebab-case from symptom) with this layout: 1. `investigation-report-_.md` — versioned narrative snapshots (PW1). Multiple files: `investigation-report-1_.md` at Step 0 (symptom only), `investigation-report-2_.md` after Step 0b, additional versions as the investigation progresses, and a final version at termination. 2. `evidence/` — one file per evidence entry E (PW1) 3. `hypothesis/` — one file per hypothesis event H- (PW3) 4. `model-changes/` — one file per model change M (PW2) Formal model files (`.dfy`, `.als`) go at the investigation root. **Report versioning.** Reports are immutable once written; new information produces a new versioned file rather than an edit in place. Each report from version 2 onward carries a `PrevReportHash:` field = `sha256(previous-report-file-bytes)`, forming a report chain parallel to the hypothesis and model chains. The first report (`investigation-report-1_*`) has no `PrevReportHash:`; it is the genesis anchor for all three chains — hypothesis, model, and report. Each record is its OWN file — no monolithic append logs. Filename format: `E1_2026-04-25T10-30-45-123Z.md`, `H1-2_2026-04-25T10-31-00-456Z.md`, `M1_2026-04-25T10-40-00-789Z.md`. The suffix is an ISO 8601 timestamp with millisecond precision, using `-` in place of `:` and `.` (filesystem-safe, sortable, greppable). Each record also carries a `Timestamp:` field with the full ISO 8601 value (with colons and decimal ms) INSIDE the file, e.g., `Timestamp: 2026-04-25T10:30:45.123Z`. **Chain structure — three relationships, not one flat chain.** 1. **Hypothesis events chain to each other** — the causal-reasoning trail. Each hypothesis record (H-) carries `PrevHypHash:` = `sha256(previous-hypothesis-event-file)`, where "previous" is the H event with the next-lower `Timestamp:`. The first H event's `PrevHypHash:` anchors to `sha256(investigation-report-1_*.md)` — the first (genesis) report. 2. **Evidence attaches to a hypothesis event** — evidence exists to serve a specific check or state transition. Each E record carries `ParentHypEvent: H-` identifying the hypothesis event it was collected for, and `ParentHypHash: sha256(parent-file)` snapshotting that parent at collection time. Evidence does NOT chain to other evidence. 3. **Model-changes both chain and attach** — each M record carries `PrevModelHash:` (sha256 of previous M, anchored on `sha256(investigation-report-1_*.md)` for the first) AND `ParentHypEvent:` / `ParentHypHash:` identifying which hypothesis context triggered the model iteration. 4. **Reports chain to each other** — each `investigation-report-_*.md` with N≥2 carries `PrevReportHash:` = `sha256(investigation-report-_*.md)`. The first report has no `PrevReportHash:`; it is the genesis for all three parallel chains. **State-change events freeze their evidence.** When a hypothesis record is a `status-changed` event (to `compatible`, `weakened`, `rejected`, `undistinguished`, `accepted`), it carries `Evidence: [E, E, ...]` listing the specific evidence it rests on, plus `EvidenceHash:` = `sha256(sorted-concat-of-evidence-file-sha256s)`. Any later edit to any referenced evidence record invalidates the state-change's `EvidenceHash` — evidence becomes immutable once cited in a state transition. **Symptom-verification anchor.** At Step 0b, before collecting E1, write `H0-1: symptom-claimed` as the root anchor event. Its `PrevHypHash:` = `sha256(investigation-report-1_*.md)`. E1 then links to H0-1 as its `ParentHypEvent:`. This keeps the "evidence must attach to a hypothesis event" rule consistent from the very first evidence. **Precondition.** Before writing any record, its parent (or chain predecessor) must exist on disk with ALL required fields. You cannot write H1-2 without H1-1 being complete; you cannot write E3 without its parent H event being complete; you cannot write a `status-changed` event without its cited evidence being complete. This makes construction sequential by necessity and makes the dependency graph explicit. Why this works instead of forcing sleeps: batch-flushing the whole structure at session end requires either (a) honest `Timestamp:` values matching wall-clock during the flush — caught by filesystem-provenance — or (b) backdated timestamps — also caught by filesystem-provenance. Meanwhile, the chain and reference hashes prevent any retroactive insert, reorder, or edit of a record that has already been cited or chained from. **Blocking precondition (PW0-init).** Before proceeding to Step 0a, Codex MUST create `investigation-report-1_.md` (the first report, with just the symptom sketch) plus the three subdirectories (`evidence/`, `hypothesis/`, `model-changes/`) on disk. Codex MUST NOT collect evidence, read code, or run queries before these exist on disk. Verify with a directory listing and show it to the user. Retroactive stub creation does not satisfy this rule. Pin down the symptom — ask and record: **What** (exact wrong behavior), **Where** (service, endpoint), **When** (always? intermittent?), **For whom** (all users? specific?), **What is NOT the symptom** (adjacent things that work). Assess severity: data exposure → security-critical, financial impact → business-critical, data loss → data-integrity-critical, compliance (GDPR, SOC2, PCI-DSS) → note explicitly. Write `## Symptom` + `**Severity:**` into the report. #### Step 0a. Inventory tooling Check `investigations/tooling-inventory.md` first (template at `/templates/tooling-inventory.md`). Determine: production DB, logs, metrics, tracing, error tracking, live API, config, queues, repo, CI/CD. Write `## Tooling` noting `direct` vs `inferred` per tool. #### Step 0b. Verify the symptom **S0-V — symptom verification required.** Confirm the symptom with at least one `direct` fact (production DB query, log, or live API observation) before Step 1. `interpreted` sources (reports, specs, prior investigations) must be re-verified against production. First write `hypothesis/H0-1_.md` with `Event: symptom-claimed` and `PrevHypHash: sha256(investigation-report-1_*.md)` — this anchors the hypothesis chain. Then write `evidence/E1_.md` with `ParentHypEvent: H0-1` and `ParentHypHash:` set to the sha256 of H0-1's file bytes. Then write `investigation-report-2_.md` (the updated narrative now including `**Verified by:** E1`) with `PrevReportHash:` = sha256 of `investigation-report-1_*.md`. Do NOT edit the first report — write a new version. **S0-V.1 — Symptom proximity check.** If the symptom is transport-shaped (DNS failure, `gaierror`, connection refused, socket timeout, 5xx, health-check fail, "host not found"), the first hypothesis MUST include "target process never started or crashed during startup." Before investigating the transport layer, gather `direct` evidence of upstream liveness: startup logs, container state, readiness probe, process list. If that evidence is unavailable, Step 1 is observability (expose startup output), not topology. #### Step 1. Build the minimal model Requires `formal-modeling` skill. Check production logs/traces for the actual execution path before writing model code. Record any findings as `E` files under `evidence/`. **Locating modeling tooling.** The `formal-modeling` skill ships the Alloy/Dafny runners (`alloy_run.sh`, `dafny_run.sh`, `verify.sh`) and reference `.als`/`.dfy` examples. When installed as a plugin, look under `~/.codex/plugins/marketplaces/*/skills/formal-modeling/` (`scripts/` for runners, `references/` for example models). If not found there, check `~/.codex/skills/formal-modeling/` or ask the user for the install path before proceeding. **Default: create a formal model file AND run the solver in the same step.** Use `.dfy` for fast iteration, `.als` for counterexamples. Building the model and running the solver are one atomic step — a `.dfy`/`.als` file without a `Solver result:` field in an `M` record does NOT satisfy TC28. "Model exists but solver deferred pending evidence" is NOT an allowed state. Consequences: - If constraints are too sparse to run usefully (e.g., waiting for S0-V.1 liveness evidence), do one of: (a) defer MODEL CREATION until Step 4 evidence arrives, (b) run the solver anyway on the sparse model — unsat or a minimal counterexample is still signal that narrows the hypothesis space, or (c) propose a skip per the protocol below. - A solver run that times out counts as a run; record the timeout and which assertions were tried. Partial results still satisfy TC28 when accompanied by a documented next step. - The M entry MUST include the `Solver result:` field per the hypothesis-entry format. An M1 entry without a solver result is a protocol violation caught by the termination gate. **Model skip — requires explicit user acknowledgement before writing the skip entry.** Protocol (MUST follow in order): 1. Codex asks the user a single direct question: "Do you acknowledge skipping the formal model? Here is what it would verify: ``. Here are the edge cases narrative reasoning misses: ``." 2. Codex WAITS for a user message. Silence, "ok", "continue", or any non-response is NOT acknowledgement. The reply must be an explicit affirmative ("yes, skip", "ack", "go ahead without the model", etc.). 3. ONLY after (2), Codex writes `M1: Skipped (user-acknowledged)` as an `M1` record under `model-changes/`. The entry MUST quote the user's verbatim acknowledgement string under an `Acknowledgement:` field. 4. If the user's reply is ambiguous, Codex re-asks. Codex does NOT infer acknowledgement from context, priors, or prior sessions. Forbidden pattern: writing `M1: Skipped (user-acknowledged)` in the same turn that proposes the skip. The skip entry and the proposal MUST be in different turns separated by a user reply. Model only the **nearest causal layer**. Build four layers: 1. **Normative** — business rule invariants, forbidden states, pre/postconditions 2. **Data** — field constraints, valid/invalid combinations, stale derived data 3. **Causal** — execution path to symptom, async/transaction boundaries, branch points 4. **Observability** — expected traces per hypothesis, source reliability Write an `M1` record under `model-changes/` with trigger, what was created, and solver results. #### Step 2. Generate hypotheses Extract hypotheses from the model. Each **must** follow H1: `[condition] -> [mechanism] -> [state change] -> [symptom]`. For each, state the counterfactual (FZ1). Write `created`, `mechanism-stated`, and `counterfactual-stated` records under `hypothesis/`. #### Step 3. Design distinguishing checks For each hypothesis pair: what check distinguishes them? **Strong** = confirms one, excludes another. **Weak** = compatible with multiple. Order by max information gain. #### Step 4. Collect facts Each fact gets a **reliability tag**: | Source | Reliability | |--------|-------------| | Production DB query | `direct` | | Production logs (<7d) | `direct` | | Production logs (>7d) | `inferred` | | Live API response | `direct` | | Deployed config / env vars | `direct` | | Repo code | `interpreted` | | Git history (local) | `interpreted` | | Prior reports / specs / docs | `interpreted` | | Alloy model results | `inferred` | | User verbal description | `interpreted` | | Mobile app code | `unreliable-source` | | Third-party docs | `interpreted` | | User reports | `inferred` | **Repo code is not production truth.** Always tag code reading as `interpreted`. **F4** — Fix tasks: first fact must be `direct` production observation of current behavior. **F3** — Dynamic data: collect (1) current value, (2) change history, (3) timeline coverage. **F6** — Zero-result queries: list ALL sources, query each. Record `Absence sources: N/M`. **F7** — Wrong values: trace WRITE paths, not read. Record `Analysis type: write-path`. **F8** — Numeric discrepancy: compute exact locally before estimating. Record `Computation method`. **F9** — Snapshot fields: check temporality before trusting. Record `Field temporality`. **F10** — Baseline comparability: differential vs "last known good" requires same repo, trigger, and config. Record `Baseline: | repo=X trigger=Y config-diff=Z`. Mismatched baseline = `interpreted`. **F11** — Workspace contamination: local/CI investigations must check for untracked/gitignored files that mask CI failure. Run `/scripts/check_workspace_clean.sh [paths]` (which wraps `git ls-files --others --exclude-standard` + gitignored enumeration). Use `--source-only` to filter common source extensions when noise is high. Record `Workspace clean: yes/no` on evidence derived from local state. Write `E` records under `evidence/` immediately as facts are gathered. #### Step 5. Update model with facts Add confirmed facts as model constraints. Re-run solver. Write an `M` record under `model-changes/`. **Valid status transitions:** | From | Allowed transitions | |------|-------------------| | `active` | `compatible`, `weakened`, `rejected`, `undistinguished` | | `compatible` | `accepted`, `weakened`, `rejected`, `undistinguished` | | `weakened` | `rejected`, `compatible` | | `undistinguished` | `compatible`, `rejected` | | `rejected` | terminal — no transitions | | `accepted` | terminal — no transitions | Write `status-changed` records under `hypothesis/` with evidence references. #### Step 6. Check diagnostic equivalence If hypotheses explain the same facts and predict the same for all checks — do NOT accept any, do NOT pick by "likelihood." Proceed to Step 7. Write `equivalence-checked` and `observability-assessed` (FZ2) records under `hypothesis/`. #### Step 7. Deepen the model Expand only where undistinguished hypotheses live. Directions: depth (code), depth (data), depth (type contracts — check types at call boundary when function returns default value), breadth (observability), breadth (concurrency). Write an `M` record under `model-changes/`. Go back to Step 2. #### Step 8. Terminate or iterate **Termination conditions** (ALL must be true): 1. Exactly one hypothesis `compatible` (U1) 2. Has mechanism — causal chain (H1) 3. Has counterfactual (H2/FZ1) 4. Counterfactual observable with current telemetry (FZ2) 5. Counterfactual verified absent against production 6. No diagnostically equivalent alternatives (U1) 7. Alternative mechanism considered (M2) 8. All cause classes reviewed — Model Coverage filled (M1) 9. `direct` evidence supports conclusion (PV1) 10. No stale `direct` evidence (F5) 11. `evidence/` has ≥1 `direct` record (PW1) 12. Model re-run after last fact integration if built (PW2) 13. `mechanism-stated` logged (PW3/H1) 14. `counterfactual-stated` logged (PW3/H2) 15. `observability-assessed` logged with "observable" (PW3/FZ2) 16. `alternative-considered` logged (PW3/M2) 17. `equivalence-checked` logged (PW3/U1) 18. Status entries: one `compatible`/`accepted`, rest `rejected` (PW3/U1) 19. First evidence in each production-first step is `direct`/`inferred` (TC19) 20. Reliability tags match source classification table (F1) 21. Status transitions follow valid transition table (no `rejected`→anything) 22. Fix tasks: first S4 evidence is `direct` (F4) 23. Dynamic data: evidence verifies current value + change history + timeline (F3) 24. Absence claims: ALL sources queried, single-source = `inferred` (F6) 25. Wrong values: write path identified, not just read path (F7) 26. Numeric: exact computation if replicable; residual >5% blocks termination (F8) 27. Snapshot fields: confirmed live for current-state use (F9) 28. Formal model exists with solver results, OR `M1: Skipped (user-acknowledged)` with an `Acknowledgement:` field quoting the user's verbatim affirmative reply from a turn AFTER the skip was proposed (PV2) 29. Investigation layout was created at Step 0 before any Step 0b/1/4 activity (PW0-init). `investigation-report-1_.md` + three subdirectories (`evidence/`, `hypothesis/`, `model-changes/`) exist on disk. Filesystem ctime of each subdirectory precedes the earliest `Timestamp:` field value of any record inside it. Retroactive rebuild fails this check. 30. Valid structured hash integrity and filesystem provenance (PW0-live). (a) Every record file has a `Timestamp:` field in ISO 8601 UTC with millisecond precision; (b) `investigation-report-_*.md` files chain via `PrevReportHash:` (first report has none); (c) hypothesis records form a valid SHA-256 chain via `PrevHypHash:` anchored on `sha256(investigation-report-1_*.md)`; (d) evidence records have a valid `ParentHypEvent:` + `ParentHypHash:` pointing to an existing hypothesis event; (e) model-change records chain via `PrevModelHash:` and have valid `ParentHypEvent:` + `ParentHypHash:`; (f) every `status-changed`/`accepted` hypothesis record has a matching `EvidenceHash:` over the cited `Evidence:` list; (g) each record's in-field `Timestamp:` matches filesystem ctime within 60 seconds. 31. Transport-shaped symptom: upstream process liveness proven via `direct` evidence before transport investigation (S0-V.1) 32. Differential evidence: baseline repo/trigger/config match the failing run (F10) 33. Local/CI investigations: workspace contamination checked via `git status --ignored` (F11) 34. No system change preceded `direct` evidence of the changed state (OB1) 35. Every `rejected` hypothesis has a valid `Reason:` (evidence-based with `Evidence: E`, or preference-based with an allowed `Priority:` + `Rationale:`) in its `status-changed` log entry (U2-doc) 36. Single-record write discipline observed throughout the investigation (PW0-strict): each E/H/M record was written by exactly one `Write` call, preceded by `Bash` calls to `now_iso.py` and `sha256_file.py` for fresh values; no multi-file write/repair helper was used; pre-write narration was present for each chain record If any fails, iterate. Before acceptance, write an `alternative-considered` and a `status-changed` event file under `hypothesis/`. Assemble report: Symptom, Conclusion, Hypothesis History, Evidence Log, Hypothesis Log, Model Change Log, Model Coverage, Remaining Uncertainties, Next Steps. The report may reference the individual record files by name (e.g., "E1, E4, and H2-3 together rule out ..."). --- ## Proof of work records Three per-record subdirectories, one file per event. PW1: `evidence/` needs ≥1 `direct` entry. PW2: `model-changes/` needs ≥1 file if a model is built, re-run after fact integration. PW3: `hypothesis/` needs TC13-18 events across the hypothesis lifecycle. **PW0-init — stub layout is a blocking precondition.** `investigation-report-1_.md` plus the three subdirectories (`evidence/`, `hypothesis/`, `model-changes/`) MUST exist on disk before Step 0a begins. No evidence collection, code reading, or queries may precede their creation. Verify via directory listing shown to the user. **PW0-live — per-record files with structured hash integrity.** Each E, H, M event is its OWN file with a timestamp suffix in the filename, a `Timestamp:` field inside, and reference-hash fields tying it to its dependencies. Enforcement (TC30) is four-part: 1. **No missing Timestamp:** every record file must have a `Timestamp:` field in ISO 8601 UTC form with millisecond precision (e.g., `Timestamp: 2026-04-25T10:30:45.123Z`). 2. **Hypothesis chain valid:** hypothesis records sorted by `Timestamp:` form a valid SHA-256 chain. Each H record's `PrevHypHash:` equals `sha256(previous-H-file-bytes)`. First H record's `PrevHypHash:` equals `sha256(investigation-report-1_*.md)`. 3. **Evidence parent link valid:** every E record has `ParentHypEvent: H-` pointing to an existing H event, and `ParentHypHash:` equals `sha256(parent-H-file-bytes)`. Evidence is not cross-chained. Model-change records have `ParentHypEvent:` + `ParentHypHash:` the same way, and additionally chain via `PrevModelHash:` to the previous M (or `sha256(investigation-report-1_*.md)` for the first M). Reports with N≥2 chain via `PrevReportHash:` = `sha256(investigation-report-_*.md)`. 4. **State-change EvidenceHash valid:** hypothesis records with `Event: status-changed` (or `accepted`) include `Evidence: [E, ...]` and `EvidenceHash:` = SHA-256 over the sorted concatenation of the cited evidence files' own SHA-256 hashes. Any later edit to any cited evidence invalidates this hash. Evidence records become immutable once cited in a state transition. If a state-change record has been superseded by a later hypothesis record carrying `Supersedes: H-`, this per-record EvidenceHash check is excused for the superseded record; its broken state is preserved as audit trail while the superseding record carries the fresh valid hash. 5. **Filesystem provenance:** the in-field `Timestamp:` must match the file's creation time within 60 seconds. Large disagreement = backdated record. Superseded records are excused from this per-record check for the same reason as Check 4: the historical mismatch remains visible on disk, but no longer blocks acceptance once a superseding record exists. These checks together make the following attacks detectable: - Retroactive insert/reorder/edit of a hypothesis event → hypothesis chain mismatch - Fake evidence attached to a closed state-change → EvidenceHash mismatch - Evidence tampered with after being cited → EvidenceHash mismatch - Orphan evidence without a parent → missing `ParentHypEvent:` or mismatched `ParentHypHash:` - Batch-flush at session end → filesystem-provenance mismatch (if timestamps backdated) or matched wall-clock mismatch (if timestamps honest but clustered) Records can be written at whatever pace the investigation runs — the structure enforces sequential dependencies without requiring artificial sleeps. Before acceptance, run `/scripts/check_pw0_live.py ` — exit 0 is required. **PW0-strict — single-record write discipline.** This is the binding rule that prevents batch-fix shortcuts. The structural integrity of the chain only holds if each record was actually constructed sequentially against the live state of its predecessor. 1. **One Write per record.** Each E/H/M record is written by exactly one `Write` tool call, immediately preceded by `Bash` calls that read the current wall-clock time and the predecessor's SHA-256. Use `scripts/now_iso.py` and `scripts/sha256_file.py`. The `Timestamp:` and `PrevHypHash:` / `ParentHypHash:` / `PrevModelHash:` / `PrevReportHash:` / `EvidenceHash:` values MUST be the values returned by those calls. Never synthesize them, and never derive them from a multi-file write helper. 2. **No multi-file write helpers.** Read-only helpers that compute hashes or timestamps for a single record (`sha256_file.py`, `evidence_hash.py`, `now_iso.py`) are allowed and encouraged. Any Bash/Python invocation that writes, edits, or rechains two or more record files in a single pass is forbidden, including for setup, convenience, or fixups after a checker fails. 3. **Append-only forever. Never delete or rewrite a record.** Once an E/H/M/report file is written, its bytes are immutable and its existence on disk is permanent. Deletion, in-place rewriting, renaming, or moving as a repair is forbidden. If a record is wrong, the only remedy is to write a new record that supersedes it. The broken record stays on disk as visible audit trail. 4. **If a checker fails, repair file-by-file.** When `check_pw0_live.py` or `check_rejection_reasons.py` reports violations across multiple files, repair each affected record individually with a fresh `Bash` call to `now_iso.py` and a fresh `Write`. Do not write a script to fix multiple files at once, and do not propose one. 5. **Cost is not a justification.** Permission prompts, tool round-trips, and context size are costs accepted in exchange for the protocol's integrity. "Batching saves prompts/tokens/time" is not a valid reason to violate the rules above. 6. **Supersedes mechanism for repairing broken records.** When a record needs correction (for example, a state-change with stale `EvidenceHash:` after cited evidence changed), write a new state-change record carrying `Supersedes: H-` naming the record it replaces. The new record has its own fresh `Timestamp:`, `PrevHypHash:`, `Evidence:`, and `EvidenceHash:` values. The original broken record stays on disk untouched. `check_pw0_live.py` excuses a superseded record from the two per-record validity checks where "the broken state IS the audit trail": - Check 4 (`EvidenceHash:` validity) - Check 5 (filesystem provenance: `Timestamp:` vs ctime within 60 seconds) Chain and parent-link checks still apply transitively because they are about the superseded record's relationships to other records, not its own repaired validity: - Check 2 (`PrevHypHash:` chain) - Check 3 (`ParentHypEvent:` / `ParentHypHash:` links) 7. **Pre-Write narration.** Before each `Write` of a chain record, state in one sentence the file being written, the `Timestamp:` value just read from `now_iso.py`, and the PrevHash/ParentHash/EvidenceHash value just computed. Skipping this is itself a PW0-strict violation. Forbidden patterns: - Drafting many records first, then writing them in rapid succession with timestamps computed in a loop - Deleting a broken record to make a checker pass - Treating deletion as distinct from edit; both are forbidden mutations of disk state **Report record format:** A file at `investigation-report-_.md` where `` starts at 1 and increments with each new version. Required fields in the body: `Timestamp:` (ISO 8601 UTC ms), and `PrevReportHash:` (sha256 of the previous report file) for N≥2. The first report has no `PrevReportHash:`. Narrative content (Symptom, Severity, Tooling, and later Conclusion / Hypothesis History / etc.) follows. **Evidence record format:** A file at `evidence/E_.md` with first line `E: [description]`, followed by required fields: `Timestamp:` (ISO 8601 UTC ms), `ParentHypEvent:` (the H record it serves, e.g., `H1-2` or `H0-1` for symptom verification), `ParentHypHash:` (sha256 of the parent H file at collection time), Step, Source, Reliability, Raw observation, Interpretation, Integrated?, Hypotheses affected, Verification query. **F6-F9 optional fields:** `Absence sources: N/M` + verdict (F6), `Analysis type: write-path` + `Producer identified` (F7), `Computation method` + `Residual` (F8), `Field temporality` + `Last written` (F9). These are the audit trail TC24-27 check at termination. **F5 staleness:** `direct` evidence goes stale after deploy/migration. Re-verify before acceptance. If investigation spans sessions, re-verify all prior `direct` evidence. **Model record format:** A file at `model-changes/M_.md` with first line `M: [description]`, followed by required fields: `Timestamp:` (ISO 8601 UTC ms), `PrevModelHash:` (sha256 of previous M, or sha256 of `investigation-report-1_*.md` for the first), `ParentHypEvent:` (triggering H event), `ParentHypHash:` (sha256 of that parent H at the time of this model change), Step, Trigger, What changed, Solver result. **Hypothesis record format:** A file at `hypothesis/H-_.md` with first line `H-: [event]`, followed by required fields: `Timestamp:` (ISO 8601 UTC ms), `PrevHypHash:` (sha256 of previous H record — or sha256 of `investigation-report-1_*.md` for the first H, which is H0-1 at Step 0b), Step, Hypothesis, Event (symptom-claimed | created | mechanism-stated | counterfactual-stated | observability-assessed | alternative-considered | status-changed | equivalence-checked), Detail. For `Event: status-changed` (any target status) or `Event: accepted`, additionally include: `Evidence: [E, E, ...]` listing the specific evidence that justifies this transition, and `EvidenceHash:` = SHA-256 over the sorted concatenation of the cited evidence files' own SHA-256 hashes. For `status-changed` to `rejected`, also add `Reason:` — either `evidence` + `Evidence: E` (the evidence list also populates the EvidenceHash) OR `preference` + `Priority:` (from the allowed set) + `Rationale:` (non-empty text; a preference-based rejection still needs `Evidence: []` + `EvidenceHash:` = sha256 of empty concatenation). **Pre-acceptance log checklist** (mirrors TC1-36): 1. `evidence/` has a `direct` record (PW1) 2. `model-changes/` has an entry if a model was built, and it was re-run after facts (PW2) 3. `mechanism-stated` logged (H1) 4. `counterfactual-stated` logged (H2) 5. `observability-assessed` = observable (FZ2) 6. Counterfactual verified via `direct` evidence 7. `equivalence-checked` logged (U1) 8. `alternative-considered` logged (M2) 9. One `compatible`/`accepted`, rest `rejected` (U1) 10. No stale `direct` evidence (F5) 11. Model Coverage table filled (M1) 12. First evidence per production-first step is `direct`/`inferred` (TC19) 13. Reliability tags match source table (F1) 14. Status transitions follow valid table (no `rejected`→other) 15. Fix tasks: first S4 = `direct` (F4) 16. Dynamic data: current value + history + timeline (F3) 17. Absence: `Absence sources N/M` with N=M (F6) 18. Wrong values: `write-path` + `Producer identified` (F7) 19. Numeric: `exact-local` + `Residual ≤5%` (F8) 20. Snapshot: `Field temporality: live` for current-state (F9) 21. Model skip: `M1: Skipped (user-acknowledged)` with rationale (TC28/PV2) 22. Stub files created at Step 0 before any evidence collection (TC29/PW0-init) 23. No burst writes on the termination turn (TC30/PW0-live) 24. Transport-shaped symptom: liveness proven before transport investigation (TC31/S0-V.1) 25. Differential baseline matches on repo/trigger/config (TC32/F10) 26. Workspace contamination checked when local/CI is involved (TC33/F11) 27. No intervention before direct evidence of the state changed (TC34/OB1) 28. Every `rejected` hypothesis has a documented `Reason:` + backing field (TC35/U2-doc) 29. Single-record write discipline observed (TC36/PW0-strict): one `Write` per record, fresh `Bash` calls for time and predecessor hash, no multi-file write/repair helpers, pre-write narration present If any fails, iterate. --- ## Protocol rules **H1** — Every hypothesis: `[condition] -> [mechanism] -> [state change] -> [symptom]`. **H2** — State what observation would make it false. No counterfactual = too vague. **T1** — Every check: which hypotheses does it distinguish? Compatible with all = zero value. **U1** — Accept only if no other hypothesis is compatible. If undistinguished → deepen, don't pick. **U2** — Multiple compatible hypotheses: keep all active, do not collapse. **U2-doc** — Every `status-changed` entry to `rejected` MUST carry a `Reason:` field: `Reason: evidence` + `Evidence: E` (cite the specific entry) OR `Reason: preference` + `Priority: ` + `Rationale: `. Allowed `Priority:` values: `Occam`, `BlastRadius`, `Severity`, `RecencyOfDeploy`, `Reproducibility`, `FixCost`. Any other priority must be raised to the user first. **M2** — Before accepting, name ≥1 alternative mechanism. **M1 — blind spot checklist** (all must be reviewed before acceptance): Concurrency, Shared mutable state, Object lifecycle, Caching, Async boundaries, External systems, Partial observability, Config/feature flags, Data migration, Tenant isolation, Auth state, Deployment drift, Multi-artifact versions, Build pipeline divergence. **F1** — Tag every fact by source reliability. Never tag `interpreted` as `direct`. **F2** — Absence ≠ evidence of absence. Could it be absent from your view but present in production? **F3** — Dynamic data: check (1) current value, (2) change history, (3) timeline coverage. **F6** — Zero-result query: list ALL sources, query each. Conclude absence only when all agree. **F7** — Wrong value: trace WRITE paths (INSERT/UPDATE), not read paths. Match value to producer. **F8** — Numeric discrepancy: compute exact locally before estimating. Residual >5% = compute instead. **F9** — DB field as current state: check temporality (live/snapshot/scheduled). Snapshot = `inferred`. **F10** — Baseline comparability: differential requires matching repo/trigger/config. Record the diff. **F11** — Workspace contamination: check `git status --ignored` + `git ls-files --others` on local/CI mixes. **OB1** — Observability before intervention. Don't change topology/config/code under investigation until you have `direct` evidence of the state being changed. Blind intervention moves the target. **PW0-strict** — One `Write` per record, with fresh `Bash` calls for time and predecessor hash. No multi-file write/repair helpers. If a checker fails, fix each affected file individually with a new `Bash` + `Write` per file. Cost (tokens, prompts, round-trips) is not a justification. Pre-write narration must state the file, `Timestamp:`, and predecessor hash before each `Write`. **PV1** — ≥1 `direct` fact must support acceptance. Code reading alone is insufficient. **PV2** — Formal model required. Skip requires: (a) Codex asked, (b) user replied affirmatively in a later turn, (c) the user's verbatim reply is quoted in the skip entry. Inferring acknowledgement from silence, prior preferences, or memory is forbidden. **FZ1** — State counterfactual for each hypothesis. **FZ2** — Unobservable counterfactual blocks acceptance. Deepen observability, don't assume true. **FM1** — ≥1 `direct` fact before building model. Sequence: verify → code → hypothesize → model → verify fix. --- ## Practical guidance - **Always model.** A 20-line Dafny model beats 2000 words of prose. Start small, grow on demand. - **Facts > structure.** One reliable fact eliminating a hypothesis class beats an elaborate model. - **Name hypotheses consistently** (H1, H2, H3). Track rejections — they prove thoroughness. - **User prompts are high-value checks.** Execute them immediately — the user's domain intuition targets blind spots the protocol misses. After each major conclusion, ask: "What would the user check that I haven't?" - **Observe before reasoning.** Compute exact values (F8), query all tables (F6), trace write paths (F7), verify field liveness (F9) — don't reason where you can observe. ## Bundled files - `templates/tooling-inventory.md` — Template for tooling inventory. Copy into the project's `investigations/` directory and fill in. The skill reads it at Step 0a to avoid re-enumerating tools each investigation. - `scripts/check_pw0_live.py` — TC30/PW0-live enforcement. Run against an investigation directory before acceptance: `python3 scripts/check_pw0_live.py investigations/`. Validates report/hypothesis/model hash chains, evidence parent links, state-change `EvidenceHash:` values, and filesystem timestamp provenance, while excusing superseded records from the per-record Check 4 and Check 5 validity rules. - `scripts/check_workspace_clean.sh` — TC33/F11 enforcement. Run against the paths relevant to the investigation: `scripts/check_workspace_clean.sh src/ bot/`. Fails if any untracked or gitignored files exist under those paths. `--source-only` filters to common source extensions when the noise floor is high (e.g., `.DS_Store`, build artifacts). Exit 0 = clean, 1 = contamination. - `scripts/check_rejection_reasons.py` — TC35/U2-doc enforcement. Run against an investigation directory: `python3 scripts/check_rejection_reasons.py investigations/`. Flags `status-changed`-to-`rejected` entries missing `Reason:`, using `preference` without an allowed `Priority:`, or missing `Evidence:`/`Rationale:` backing fields. - `scripts/sha256_file.py ` — print SHA-256 hex of one file. Use for computing `PrevHypHash:`, `PrevModelHash:`, `PrevReportHash:`, and `ParentHypHash:` values. - `scripts/evidence_hash.py [ ...]` — compute `EvidenceHash:` for a state-change record. Hashes each input individually, sorts the hex digests, concatenates, then takes sha256 of the result. Order-independent (same inputs → same hash regardless of argument order). - `scripts/now_iso.py [--filename]` — current UTC timestamp with millisecond precision. Default form is the in-field `Timestamp:` value (`2026-04-25T10:30:45.123Z`); `--filename` gives the filename-safe form (`2026-04-25T10-30-45-123Z`) with `:` and `.` replaced by `-`. - `scripts/iso_to_filename.py ` / `--reverse ` — convert between the two timestamp forms. - `scripts/time_delta.py ` — signed time delta in seconds with ms precision. Accepts either canonical or filename-safe ISO form. Useful for verifying the 60s filesystem-vs-field tolerance and for computing investigation span.