/refinement-advisor

name: refinement-advisor
description: Use to decide which refinement and hardening tools are worth running on a set of changes — refine, crap-analyzer, arch-check, introversion scan, mutation testing, TLA+ model checking, Lean proofs — and on which files, with the invariant to check. Triggers — "/engineer.refinement-advisor", "what should we harden", "which checks fit this diff", "is this worth TLA+ / Lean", "should we model-check this", "how do I harden this change". Called by /engineer.harden at CP8; also usable ad hoc on any diff, in or out of the pipeline.

refinement-advisor

Reads a diff and recommends which of the DAE refinement/hardening tools to run, where, and why. It **advises; it does not run the tools.** The expensive ones (TLA+, Lean) cost real minutes each, and running every tool on every diff buries the one finding that matters under noise from checks that never fit the code.

The advice is only as good as its reading of the code: read the changed functions, not just filenames or the diff stat.

When to use

• Called by `/engineer.harden` (CP8) to pick that checkpoint's tools.
• Ad hoc: "which checks fit this change?", before a risky merge, or when

deciding whether a piece of code deserves formal verification.

**Not for:** running the tools (`harden`, or the tools' own skills), or reviewing code quality itself (`refine`).

Inputs

• **Scope** — a feature dir (diff = feature branch vs its branch point), a fix

record, a PR, or an explicit ref range. Default: current branch vs its merge-base with the default branch.

• **Stage** (optional) — `refine`, `verify`, `harden`, or `any` (default). Limits

the recommendations to that stage's tools.

• **Prior results** (optional) — if a CP7 handoff exists, read its

`crap_results` block (arch-check records crap-analyzer's output there). CRAP scores tell you where complex, poorly tested code is. Use them; don't redo that analysis.

The toolbox

| Tool | Stage | Answers | Cost | |---|---|---|---| | `/engineer.refine` | CP6 | Is the changed code clean: reuse, clarity, efficiency? | medium | | `crap-analyzer` | CP7 | Where does high complexity meet low test coverage? | low | | `/engineer.arch-check` | CP7 | Does it respect the charter's layering and naming? | low | | introversion scan (`dae_introvert.py`) | CP8 | Can a test pass without asserting anything? | low | | `atdd:atdd-mutate` | CP8 | Do the tests fail when the code is wrong? | medium | | `/engineer.tlaplus` | CP8 | Can **some interleaving or sequence of events** break an invariant? | high | | `/engineer.lean` | CP8 | Does an invariant hold **for every input**, including unbounded ones? | high |

**Every tool in scope gets a verdict, `recommend` or `skip`, with a reason.** Nothing runs by default. A cheap tool that can't find anything in this diff is still noise, and an expensive one that fits is worth its cost. Judge each one against the signals below.

Signals, per tool

**`/engineer.refine`**: recommend when CP6 hasn't run on the current diff, or code changed since it did. Skip when refine's handoff already covers these commits.

**`crap-analyzer` / `arch-check`**: recommend when CP7 hasn't run on the current diff. Skip when a CP7 handoff covers these commits, and reuse its numbers instead.

**Introversion scan**: recommend when test files were added or changed. Skip when no tests changed (there is nothing new to scan).

**Mutation (`atdd:atdd-mutate`)**: recommend when the change adds or alters branching logic (conditions, loops, error paths, boundaries) **and** tests exercise it. That's where a weak assertion hides. Skip when:

• the change is config, docs, markup, styling, generated code, or trivial

accessors

• no tests cover the changed code (mutation just reports "all survived", which

crap-analyzer already told you; recommend writing tests instead)

• mutation already ran on the same files and they haven't changed since
• the risk is temporal (races, ordering). Mutants don't model interleavings, so

that is a TLA+ job, not a mutation job.

**`tlaplus`**: recommend when the changed code has temporal or concurrent shape:

• retry and backoff loops, timeouts, circuit breakers, rate limiters
• locks, queues, workers, schedulers, cron-style jobs that can overlap
• async/await, promises, callbacks, events, or streams where order matters
• an explicit state machine or status enum with transitions, such as session

phase, order status, or a connection lifecycle

• multi-step protocols (handshake, cancel/redeliver, two-phase anything)

Races don't raise complexity metrics, so a low CRAP score says nothing here. Recommend TLA+ based on the shape of the code, not on the risk score.

**`lean`**: recommend when there is a claim of the form "for all inputs X, P holds", about pure logic:

• parsers, sanitizers, maskers, encoders (e.g. "the output never contains the

password")

• money, units, rounding, or date arithmetic
• permission and authorization predicates
• ordering, dedup, and merge functions
• a state machine whose invariant must hold over unbounded counts or data. TLC

only checks a finite model; Lean proves the general case.

Choose between TLA+ and Lean by the question: if you are asking "what if these happen in a different order", use TLA+. If you are asking "what if the input is weird", use Lean. If both apply, recommend both, each scoped to its own function. Skip both for CRUD, glue, configuration, rendering, or straight-line code with no invariant worth stating, or when a small table-driven test already covers the whole input space.

The invariant is the deliverable

For every TLA+/Lean recommendation, draft the invariant in one plain sentence ("attempt count never exceeds MAX_RETRIES and every path exits"). Both formal skills say the invariant is the one thing that can't be inferred from the code: it states what must never happen. The advisor's draft is a starting point for the human to correct. If you can't state an invariant, do