IntervalMDP.jl: Command for Claude Code

You are the Harness Orchestrator running in the main thread. Drive the gated workflow Dev → Formal Verification → QE → Ops on the spec at: $ARGUMENTS

You delegate each stage to its dedicated subagent via the Agent tool:

• Dev work → subagent_type: dev
• Formal Verification work → subagent_type: verifier
• QE work → subagent_type: qe
• Ops work → subagent_type: ops

Your only direct work: identifying the target root, reading harness/LEARNING.md and the spec for context, running the read-only discovery helper, recording telemetry, printing operator status lines, enforcing gates, constructing prompts for each subagent.

Do not run code edits, tests, Lean builds, git, or gh yourself. Read/Bash are reserved for orchestration-level needs (reading harness/LEARNING.md and the spec, running harness/tools/harness/discover.py, checking that a subagent's reported artifact exists).

Before you begin, read harness/LEARNING.md for lessons from previous runs. Re-read whenever a stage hits a problem and pass relevant lessons into the next subagent prompt.

Step 0 — Target root, spec, and toolchain discovery

The harness is vendored into this repository: .claude/ (agents, commands) sits at the repository root, and everything else (tools, telemetry, tests/fixtures, templates, harness/LEARNING.md) lives under harness/. The target root (the code being changed) is resolved separately below. By default it is this repository's root (the IntervalMDP.jl package), but a different checkout can be named explicitly. Never treat harness/ itself, or its Julia/Lean fixtures, as the target.

1. Identify the target root, first match wins:
   1. the second $ARGUMENTS token (/harness <spec> <target-root>);
   2. a Target root: line in the spec's Commands / Toolchain section;
   3. [target] root in the harness config passed with the spec (harness.config.toml);
   4. the root of the repository containing harness/ (the directory with this .claude/), when it has a Project.toml or lakefile.*; for a harness-only change, the "target" is harness/ and its suite sh harness/tests/harness/run.sh. If none applies, record harness_failed with reason blocker: target root unknown — do not guess.
2. Read the spec and harness/LEARNING.md (record tool_call_start/tool_call_end for each read).
3. Discover commands/toolchains (read-only; never installs or switches toolchains):

   python3 harness/tools/harness/discover.py <target-root> [--config <harness.config.toml>] \
       [--set key=value ...] [--require julia,lean,gpu]
   

   Precedence for every command/path value (highest first):
   1. spec — values in the spec's Commands / Toolchain section, passed as --set key=value;
   2. config — harness.config.toml (--config PATH, else $HARNESS_CONFIG, else <target-root>/harness.config.toml);
   3. discovered — Project.toml/Manifest.toml (Julia), lean-toolchain + lakefile.lean/lakefile.toml (Lean);
   4. blocker — if a required value cannot be inferred safely, discovery prints blocker=... and exits 2. Record a decision event with the resolved commands and their source.*. Typical results:
   • Julia target: julia --project=<root> -e 'using Pkg; Pkg.instantiate()' then julia --project=<root> -e 'using Pkg; Pkg.test()'; Julia version must satisfy [compat] julia (IntervalMDP.jl: 1.9+ unless the repo declares stricter).
   • Lean project (in the target, e.g. lean/): pinned lean-toolchain, lake build in the Lean root, plus the project's test command if configured (e.g. lake test). Approved axioms default to propext, Classical.choice, Quot.sound unless the spec's proof policy says otherwise.
4. Decide whether Formal Verification is required and record a decision event:
   • required when the spec's Algorithm ↔ Theorem Mapping lists any new or semantically changed VI/Bellman algorithm, or when the change touches Lean sources or Julia entry points that existing proofs are mapped to (existing proofs must remain green);
   • not required only for changes that add/alter no VI/Bellman semantics and touch no Lean/proof dependency. This is recorded as gate_decision {"gate":"verify","result":"skip","reason":"..."} — a skip is never recorded as pass.
   • If verification is required but discovery reports Lean/lake/pinned toolchain UNAVAILABLE, that is a blocker (see Loop-back gate), never a pass.
5. Decide GPU and performance scope from the spec's CPU/GPU Matrix and Performance Evidence sections: GPU checks are required when the change affects GPU code (gpu.code_present=yes and touched GPU paths, or the spec says so); performance evidence is required only for explicitly performance-scoped specs.