Harden

harden

Checkpoint 8. Acceptance tests show the feature works. Harden checks whether the tests would notice if it stopped working, and, for code with a real invariant, whether that invariant can be broken at all.

Tool choice comes from /engineer.refinement-advisor, not from a fixed list. Formal verification is worth its cost on a retry loop, and a waste on a CRUD endpoint.

Modes

• feature (default): scope = the feature branch's changed code. Entry gate applies. Writes a CP8 handoff.
• fix: called from /engineer.fix Step 7. Scope = the fix diff. Skip the Step 0 feature gate, write results into the fix record's harden_results, and write no CP8 handoff (fix owns its own close).

Workflow

Step 0 — Entry gate (feature mode). Run ${CLAUDE_PLUGIN_ROOT}/scripts/dae_handoff.py <feature-dir> --through 7. On a non-zero exit, stop and show the gap to the human. Then run ${CLAUDE_PLUGIN_ROOT}/scripts/dae_branch.py <feature-dir>. On a non-zero exit, stop. After both pass, show the breadcrumb (${CLAUDE_PLUGIN_ROOT}/scripts/dae_progress.py <feature-dir>, advisory) and create one TodoWrite todo per step. See ${CLAUDE_PLUGIN_ROOT}/references/progress-indicator.md.

Verification independence: CP8 runs on a non-implementer agent (agent_id ≠ CP5's; enforced by dae_handoff.py gate()).

1. Resolve + scope. Resolve the root and manifest via ${CLAUDE_PLUGIN_ROOT}/scripts/dae_resolve.py. Scope = changed code. Load acs.md, spec.md, CHARTER.md, and the CP7 handoff's crap_results block (arch-check records crap-analyzer's output there). In fix mode, or if the block is missing, run crap-analyzer on the scope first.

2. Advise. Run /engineer.refinement-advisor with stage: harden over the scope, passing it crap_results. Effective autonomy decides who picks the checks (see the advisor's Who decides: autonomy):

   • at high, the advisor decides alone
   • below high, it asks
   • manifest.harden.required: true makes every recommended check mandatory
   • Steps 3–5 each run only if their tool was selected. An unselected step records {skipped: <the advisor's reason, or "not selected">} in its harden_results field, so the decision is visible, not silent.

   Record the table, what was selected, and who decided (decided_by: advisor | human) in harden_results.advisor.

3. Introversion pre-scan (if selected). Run ${CLAUDE_PLUGIN_ROOT}/scripts/dae_introvert.py <methodology-root>. It flags tests that can pass without asserting on SUT output. The script defers to manifest.introversion.backend when set. Any non-ok status is advisory. Dispatch an agent to confirm each finding. For each confirmed vacuous test, write a real assertion and re-run. Record harden_results.introversion.

4. Mutation (if selected). Run atdd:atdd-mutate on the touched files, then atdd:kill-mutants on the survivors. If a test was flagged in Step 3 and carries a surviving mutant, it is almost certainly vacuous. Record harden_results.mutation_score.

5. Formal checks (selected TLA+/Lean rows only). Dispatch one plain subagent (default isolation, not a fork) per pick, subagent_type: engineer:formal-verifier (or the project override): /engineer.tlaplus for interleaving/state-machine targets, /engineer.lean for all-inputs targets. Each brief gives:

   • the target function (file:line)
   • the confirmed invariant
   • "follow the skill's Verifying real code workflow; model the code as written"
   • "do not open a PR; return the verdict, and any counterexample reproduced against the real code"

   Picks for different targets are independent, so dispatch them in parallel. Handle each result as follows:

   • Holds. Record the verdict and its limit. TLC's "no error up to N" is not a proof; Lean with no sorry and clean #print axioms is.
   • Confirmed counterexample. Treat it like a surviving mutant. Pin it as a failing test (red), fix, go green, and re-run both test streams. If the fix would change AC-observable behavior, stop and route to /engineer.feature-edit. Harden does not rewrite the contract.
   • Doesn't reproduce. The model diverged from the code. Record it as provisional and do not fix the code.
   • Side findings (dead code, an unreachable branch). Record them as advisory, and don't block on them.

   Record harden_results.formal[]: {tool, target, invariant, verdict: holds|violated|provisional, bound_or_proof, finding}.

6. Arch re-check. Harden may have changed code, so re-run ${CLAUDE_PLUGIN_ROOT}/scripts/dae_arch.py <methodology-root>. Record harden_results.arch_check.

7. Handoff (feature mode). Emit per ${CLAUDE_PLUGIN_ROOT}/references/handoff-summary.md with checkpoint: 8. The exit_criteria block asserts:

   • the advisor ran, and every tool has a recorded verdict (selected, or skipped with a reason)
   • if mutation was selected: score ≥ quality_thresholds.mutation_score_min (verified_by: tool). Both are percentages, 0–100.
   • if introversion was selected: no unresolved confirmed vacuous tests
   • every selected formal check is holds, or its counterexample is fixed and pinned by a test that fails on the old code
   • arch-check clean

   recommended_next: "open PR / /engineer.progress-log".