Refinement Advisor

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

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, don't recommend the tool.