RoT MoE 10.0.2 -- Lean+Extra

RoT MoE 10.0.2 -- Lean+Extra

Router-Lean + UNSEALED.md, the policy page that permits the unsealed lane.

this tag ships	measured
archive	RoT-MoE-Router-Lean-Extra.zip (2378 KB)
files	374
Lean 4 sources	116
UNSEALED.md	yes
manifest version inside	10.0.2

Three tags are cut from one commit: v10.0.0 Router, v10.0.1 Lean,
v10.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

Major: the observer is driven by the measured gauge, not by seven fixed
integers. 10.0.0 core · 10.0.1 lean · 10.0.2 unsealed, published
separately, cut from this one commit and differing by archive content only.

The router was already writing a "kind":"gauge" record beside every route
line — K, mean, breadth, M/C/T, sum, R/s+, active, and each of the nine lenses
with lambda, mu, a, delta, sigma, H and term. The observer read none of it and
decided when a lens should speak from lens names painted on if-statements:
out-of-band and behavioural, but not RoT MoE. This release closes that gap,
which is a behavioural change to the speaking condition — hence the major.

Changed — the seven integers became bases

• hooks/animus-observe.sh decided when a lens should speak from seven
  hardcoded integers (AN_N=2 COST_N=3 DITHER_N=3 BLOAT_N=3 LOOP_N=4
TEXT_N=6 STALL_S=120). Each is now a BASE, divided by the electing lens's
  measured share of its gauge line: a starved lens earns one remark, a lens
  carrying the session earns up to six.
• STALL_S is scaled the same way but floored at 45 s, because a false
  stall is a lie told in a lens's own voice.
• On Stop, and only on Stop, the turn is read backwards: nine candidate
  findings, each scored by the weight the gauge actually gave the lens that
  would speak it, at most two spoken and the remainder written to the
  distillate.

Added — the Nushell lane ships, first in dispatch

• Five hooks in Nushell (prover-remind.nu, rot-env.nu, rot-profile.nu,
  rot-router.nu, rot-voice-gate.nu, +2431 lines) are now tracked and
  SPDX-covered. hooks/hooks.json dispatch order is now nu → pwsh → bash;
  hosts without the nu binary fall through unchanged.
• lean/Proofs/RotCostBudget.lean grew wallBoundMs and its separation
  theorems. Theorem count 1809 → 1813, measured by checker/count-theorems.sh;
  plugin.json and marketplace.json restate the measured number.

Fixed — fused lenses were credited with zero elections

• active is a comma-joined set during NSIL FUSE. Membership was tested
  against single names only, so every fused lens was credited with zero
  elections and then accused of starving. Split on commas, credit each name.
• checker/bench-router.sh phase 2 gated wall clock against msBound, the
  router's spawn budget. Wall contains the host's interpreter startup: measured
  2026-08-28, 509–528 ms wall against 117–146 ms in-script with an unmoved
  spawn count. Wall now gates against wallBoundMs; the code claim is printed,
  not enforced; the spawn check judges the code. Proved in RotCostBudget
  (the_wall_ceiling_cannot_replace_the_spawn_check and three siblings).
• checker/ci-dryrun.sh split git ls-files -s output on whitespace, so four
  executable paths containing a space were truncated and the mode assertion
  went red by exactly four. The path is now taken from the TAB-delimited field.

Measured — a 4781-record replay of a live session sink

• 2390 gauge records parsed; 170 remarks over 52 turns, never 3 in one turn.
• 189 verdicts written; 8 of 9 lenses fired unforced. Carnage's condition (one
  lens elected on ≥80% of ≥5 readings) was forced on a fixture and observed
  firing, so all 9 are reachable.
• Starved-lens claims re-derived by an independent JSON parser: 93 of 93 true.
• A gauge-blinded mutation control differs from this build by 237 remark lines,
  which is what makes the wiring load-bearing rather than asserted.

Notes

• hooks/rot-voice.dtd ENV.26-32 now describe the bases as scaled by measured
  share rather than as constants, and engine/rot.env.example was regenerated
  from the DTD through checker/env-wiring.sh --emit — no env var added or
  removed.
• The .nu files require the nu binary; PowerShell 7 cannot parse them.
  Dispatch probes for nu and falls back, so no host that could run 9.0.1 is
  worse off.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 10.0.1 -- Lean

RoT MoE 10.0.1 -- Lean

Router + the Lean 4 toolchain fetcher and the proof corpus. This is the tier /plugin install serves.

this tag ships	measured
archive	RoT-MoE-Router-Lean.zip (2375 KB)
files	373
Lean 4 sources	116
UNSEALED.md	no
manifest version inside	10.0.1

Three tags are cut from one commit: v10.0.0 Router, v10.0.1 Lean,
v10.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

Major: the observer is driven by the measured gauge, not by seven fixed
integers. 10.0.0 core · 10.0.1 lean · 10.0.2 unsealed, published
separately, cut from this one commit and differing by archive content only.

The router was already writing a "kind":"gauge" record beside every route
line — K, mean, breadth, M/C/T, sum, R/s+, active, and each of the nine lenses
with lambda, mu, a, delta, sigma, H and term. The observer read none of it and
decided when a lens should speak from lens names painted on if-statements:
out-of-band and behavioural, but not RoT MoE. This release closes that gap,
which is a behavioural change to the speaking condition — hence the major.

Changed — the seven integers became bases

• hooks/animus-observe.sh decided when a lens should speak from seven
  hardcoded integers (AN_N=2 COST_N=3 DITHER_N=3 BLOAT_N=3 LOOP_N=4
TEXT_N=6 STALL_S=120). Each is now a BASE, divided by the electing lens's
  measured share of its gauge line: a starved lens earns one remark, a lens
  carrying the session earns up to six.
• STALL_S is scaled the same way but floored at 45 s, because a false
  stall is a lie told in a lens's own voice.
• On Stop, and only on Stop, the turn is read backwards: nine candidate
  findings, each scored by the weight the gauge actually gave the lens that
  would speak it, at most two spoken and the remainder written to the
  distillate.

Added — the Nushell lane ships, first in dispatch

• Five hooks in Nushell (prover-remind.nu, rot-env.nu, rot-profile.nu,
  rot-router.nu, rot-voice-gate.nu, +2431 lines) are now tracked and
  SPDX-covered. hooks/hooks.json dispatch order is now nu → pwsh → bash;
  hosts without the nu binary fall through unchanged.
• lean/Proofs/RotCostBudget.lean grew wallBoundMs and its separation
  theorems. Theorem count 1809 → 1813, measured by checker/count-theorems.sh;
  plugin.json and marketplace.json restate the measured number.

Fixed — fused lenses were credited with zero elections

• active is a comma-joined set during NSIL FUSE. Membership was tested
  against single names only, so every fused lens was credited with zero
  elections and then accused of starving. Split on commas, credit each name.
• checker/bench-router.sh phase 2 gated wall clock against msBound, the
  router's spawn budget. Wall contains the host's interpreter startup: measured
  2026-08-28, 509–528 ms wall against 117–146 ms in-script with an unmoved
  spawn count. Wall now gates against wallBoundMs; the code claim is printed,
  not enforced; the spawn check judges the code. Proved in RotCostBudget
  (the_wall_ceiling_cannot_replace_the_spawn_check and three siblings).
• checker/ci-dryrun.sh split git ls-files -s output on whitespace, so four
  executable paths containing a space were truncated and the mode assertion
  went red by exactly four. The path is now taken from the TAB-delimited field.

Measured — a 4781-record replay of a live session sink

• 2390 gauge records parsed; 170 remarks over 52 turns, never 3 in one turn.
• 189 verdicts written; 8 of 9 lenses fired unforced. Carnage's condition (one
  lens elected on ≥80% of ≥5 readings) was forced on a fixture and observed
  firing, so all 9 are reachable.
• Starved-lens claims re-derived by an independent JSON parser: 93 of 93 true.
• A gauge-blinded mutation control differs from this build by 237 remark lines,
  which is what makes the wiring load-bearing rather than asserted.

Notes

• hooks/rot-voice.dtd ENV.26-32 now describe the bases as scaled by measured
  share rather than as constants, and engine/rot.env.example was regenerated
  from the DTD through checker/env-wiring.sh --emit — no env var added or
  removed.
• The .nu files require the nu binary; PowerShell 7 cannot parse them.
  Dispatch probes for nu and falls back, so no host that could run 9.0.1 is
  worse off.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 10.0.0 -- Router

RoT MoE 10.0.0 -- Router

The router and its organs. No Lean 4, no unsealed policy page.

this tag ships	measured
archive	RoT-MoE-Router.zip (691 KB)
files	73
Lean 4 sources	0
UNSEALED.md	no
manifest version inside	10.0.0

Three tags are cut from one commit: v10.0.0 Router, v10.0.1 Lean,
v10.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

Major: the observer is driven by the measured gauge, not by seven fixed
integers. 10.0.0 core · 10.0.1 lean · 10.0.2 unsealed, published
separately, cut from this one commit and differing by archive content only.

The router was already writing a "kind":"gauge" record beside every route
line — K, mean, breadth, M/C/T, sum, R/s+, active, and each of the nine lenses
with lambda, mu, a, delta, sigma, H and term. The observer read none of it and
decided when a lens should speak from lens names painted on if-statements:
out-of-band and behavioural, but not RoT MoE. This release closes that gap,
which is a behavioural change to the speaking condition — hence the major.

Changed — the seven integers became bases

• hooks/animus-observe.sh decided when a lens should speak from seven
  hardcoded integers (AN_N=2 COST_N=3 DITHER_N=3 BLOAT_N=3 LOOP_N=4
TEXT_N=6 STALL_S=120). Each is now a BASE, divided by the electing lens's
  measured share of its gauge line: a starved lens earns one remark, a lens
  carrying the session earns up to six.
• STALL_S is scaled the same way but floored at 45 s, because a false
  stall is a lie told in a lens's own voice.
• On Stop, and only on Stop, the turn is read backwards: nine candidate
  findings, each scored by the weight the gauge actually gave the lens that
  would speak it, at most two spoken and the remainder written to the
  distillate.

Added — the Nushell lane ships, first in dispatch

• Five hooks in Nushell (prover-remind.nu, rot-env.nu, rot-profile.nu,
  rot-router.nu, rot-voice-gate.nu, +2431 lines) are now tracked and
  SPDX-covered. hooks/hooks.json dispatch order is now nu → pwsh → bash;
  hosts without the nu binary fall through unchanged.
• lean/Proofs/RotCostBudget.lean grew wallBoundMs and its separation
  theorems. Theorem count 1809 → 1813, measured by checker/count-theorems.sh;
  plugin.json and marketplace.json restate the measured number.

Fixed — fused lenses were credited with zero elections

• active is a comma-joined set during NSIL FUSE. Membership was tested
  against single names only, so every fused lens was credited with zero
  elections and then accused of starving. Split on commas, credit each name.
• checker/bench-router.sh phase 2 gated wall clock against msBound, the
  router's spawn budget. Wall contains the host's interpreter startup: measured
  2026-08-28, 509–528 ms wall against 117–146 ms in-script with an unmoved
  spawn count. Wall now gates against wallBoundMs; the code claim is printed,
  not enforced; the spawn check judges the code. Proved in RotCostBudget
  (the_wall_ceiling_cannot_replace_the_spawn_check and three siblings).
• checker/ci-dryrun.sh split git ls-files -s output on whitespace, so four
  executable paths containing a space were truncated and the mode assertion
  went red by exactly four. The path is now taken from the TAB-delimited field.

Measured — a 4781-record replay of a live session sink

• 2390 gauge records parsed; 170 remarks over 52 turns, never 3 in one turn.
• 189 verdicts written; 8 of 9 lenses fired unforced. Carnage's condition (one
  lens elected on ≥80% of ≥5 readings) was forced on a fixture and observed
  firing, so all 9 are reachable.
• Starved-lens claims re-derived by an independent JSON parser: 93 of 93 true.
• A gauge-blinded mutation control differs from this build by 237 remark lines,
  which is what makes the wiring load-bearing rather than asserted.

Notes

• hooks/rot-voice.dtd ENV.26-32 now describe the bases as scaled by measured
  share rather than as constants, and engine/rot.env.example was regenerated
  from the DTD through checker/env-wiring.sh --emit — no env var added or
  removed.
• The .nu files require the nu binary; PowerShell 7 cannot parse them.
  Dispatch probes for nu and falls back, so no host that could run 9.0.1 is
  worse off.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 9.0.2 -- Lean+Extra

RoT MoE 9.0.2 -- Lean+Extra

Router-Lean + UNSEALED.md, the policy page that permits the unsealed lane.

this tag ships	measured
archive	RoT-MoE-Router-Lean-Extra.zip (2339 KB)
files	369
Lean 4 sources	116
UNSEALED.md	yes
manifest version inside	9.0.2

Three tags are cut from one commit: v9.0.0 Router, v9.0.1 Lean,
v9.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

The tier is the patch digit again — and the audit that earned the release.
9.0.0 core · 9.0.1 lean · 9.0.2 unsealed, published separately. 9.0.1
is what /plugin install serves: the verification surface is the point of this
project, so the default carries it.

Fixed — two RED, found by audit and each proven load-bearing by mutation

• R1 both PowerShell arms emitted OEM best-fit garbage for every non-ASCII
  byte (⚜️→??, λ→?, ·→0xFA). One pinned encoding per arm. Reverting
  the pin turns cross-diff red — mutation-proven, not asserted.
• R2 the project path was normalised BEFORE the $PWD fallback. Reordered.
  Stated honestly: the live corruption was real, its mechanism was NOT
  reproducible from any shell, and the reorder is kept as a safety property
  rather than a reproduced fix.

Fixed — instrument and latent defects

• R3 the CI audit judged whatever run came back; it now NAMES its workflow
  and refuses (exit 2) if that workflow is absent. Steps read: 5 → 221.
• O1 byte-wise locale for the DTD reader, bound to the declaration.
• O2 the sink-retirement check asked node for its own path. voice-contract
  46/1 → 47/0.
• O3 an unbound "26 checks" claim removed from three README spots — and a
  guard added, because replanting it was previously undetected.
• O5 / O5b the licence gate had never opened a .js, and bonus/ shipped
  six unlicensed files. 287 → 318 source files, 0 missing a header.
• O6 every hook command ran BOTH arms when the ps1 arm failed
  (A && B || C). All 63 rewritten to the conditional form; installers carry
  legacy strings so an old arm still disarms.
• Y1 path equality is not string equality — a pin this installer wrote
  survived arm under a different true spelling of the same directory.
• Y5 cross-diff never reached the payload path. Y6 the ps1 sink wrote
  CRLF into .jsonl. Y7 dead ROT_PROFILE removed from both arms.
  Y8 three deliberate control bytes documented. Y10 the arm fallback
  finally has a checker — shape AND behaviour.

Verified

87/87 modules kernel re-verified · 797/797 mutants killed, 0 survived ·
1632 theorems · 0 sorry · 31 hook events / 63 entries all execute ·
Animus consume-and-emit proven with five controls · 190 .sh files,
0 syntax failures, error tier cleared · two separate Claude Code 2.1.238
scratchpad sessions wrote their own sinks and fired 10 distinct hook events.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 9.0.1 -- Lean

RoT MoE 9.0.1 -- Lean

Router + the Lean 4 toolchain fetcher and the proof corpus. This is the tier /plugin install serves.

this tag ships	measured
archive	RoT-MoE-Router-Lean.zip (2336 KB)
files	368
Lean 4 sources	116
UNSEALED.md	no
manifest version inside	9.0.1

Three tags are cut from one commit: v9.0.0 Router, v9.0.1 Lean,
v9.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

The tier is the patch digit again — and the audit that earned the release.
9.0.0 core · 9.0.1 lean · 9.0.2 unsealed, published separately. 9.0.1
is what /plugin install serves: the verification surface is the point of this
project, so the default carries it.

Fixed — two RED, found by audit and each proven load-bearing by mutation

• R1 both PowerShell arms emitted OEM best-fit garbage for every non-ASCII
  byte (⚜️→??, λ→?, ·→0xFA). One pinned encoding per arm. Reverting
  the pin turns cross-diff red — mutation-proven, not asserted.
• R2 the project path was normalised BEFORE the $PWD fallback. Reordered.
  Stated honestly: the live corruption was real, its mechanism was NOT
  reproducible from any shell, and the reorder is kept as a safety property
  rather than a reproduced fix.

Fixed — instrument and latent defects

• R3 the CI audit judged whatever run came back; it now NAMES its workflow
  and refuses (exit 2) if that workflow is absent. Steps read: 5 → 221.
• O1 byte-wise locale for the DTD reader, bound to the declaration.
• O2 the sink-retirement check asked node for its own path. voice-contract
  46/1 → 47/0.
• O3 an unbound "26 checks" claim removed from three README spots — and a
  guard added, because replanting it was previously undetected.
• O5 / O5b the licence gate had never opened a .js, and bonus/ shipped
  six unlicensed files. 287 → 318 source files, 0 missing a header.
• O6 every hook command ran BOTH arms when the ps1 arm failed
  (A && B || C). All 63 rewritten to the conditional form; installers carry
  legacy strings so an old arm still disarms.
• Y1 path equality is not string equality — a pin this installer wrote
  survived arm under a different true spelling of the same directory.
• Y5 cross-diff never reached the payload path. Y6 the ps1 sink wrote
  CRLF into .jsonl. Y7 dead ROT_PROFILE removed from both arms.
  Y8 three deliberate control bytes documented. Y10 the arm fallback
  finally has a checker — shape AND behaviour.

Verified

87/87 modules kernel re-verified · 797/797 mutants killed, 0 survived ·
1632 theorems · 0 sorry · 31 hook events / 63 entries all execute ·
Animus consume-and-emit proven with five controls · 190 .sh files,
0 syntax failures, error tier cleared · two separate Claude Code 2.1.238
scratchpad sessions wrote their own sinks and fired 10 distinct hook events.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 9.0.0 -- Router

RoT MoE 9.0.0 -- Router

The router and its organs. No Lean 4, no unsealed policy page.

this tag ships	measured
archive	RoT-MoE-Router.zip (637 KB)
files	68
Lean 4 sources	0
UNSEALED.md	no
manifest version inside	9.0.0

Three tags are cut from one commit: v9.0.0 Router, v9.0.1 Lean,
v9.0.2 Lean+Extra. They differ by archive content, not by source tree --
the table above is the whole difference, read out of the zip at publish time.

---

The tier is the patch digit again — and the audit that earned the release.
9.0.0 core · 9.0.1 lean · 9.0.2 unsealed, published separately. 9.0.1
is what /plugin install serves: the verification surface is the point of this
project, so the default carries it.

Fixed — two RED, found by audit and each proven load-bearing by mutation

• R1 both PowerShell arms emitted OEM best-fit garbage for every non-ASCII
  byte (⚜️→??, λ→?, ·→0xFA). One pinned encoding per arm. Reverting
  the pin turns cross-diff red — mutation-proven, not asserted.
• R2 the project path was normalised BEFORE the $PWD fallback. Reordered.
  Stated honestly: the live corruption was real, its mechanism was NOT
  reproducible from any shell, and the reorder is kept as a safety property
  rather than a reproduced fix.

Fixed — instrument and latent defects

• R3 the CI audit judged whatever run came back; it now NAMES its workflow
  and refuses (exit 2) if that workflow is absent. Steps read: 5 → 221.
• O1 byte-wise locale for the DTD reader, bound to the declaration.
• O2 the sink-retirement check asked node for its own path. voice-contract
  46/1 → 47/0.
• O3 an unbound "26 checks" claim removed from three README spots — and a
  guard added, because replanting it was previously undetected.
• O5 / O5b the licence gate had never opened a .js, and bonus/ shipped
  six unlicensed files. 287 → 318 source files, 0 missing a header.
• O6 every hook command ran BOTH arms when the ps1 arm failed
  (A && B || C). All 63 rewritten to the conditional form; installers carry
  legacy strings so an old arm still disarms.
• Y1 path equality is not string equality — a pin this installer wrote
  survived arm under a different true spelling of the same directory.
• Y5 cross-diff never reached the payload path. Y6 the ps1 sink wrote
  CRLF into .jsonl. Y7 dead ROT_PROFILE removed from both arms.
  Y8 three deliberate control bytes documented. Y10 the arm fallback
  finally has a checker — shape AND behaviour.

Verified

87/87 modules kernel re-verified · 797/797 mutants killed, 0 survived ·
1632 theorems · 0 sorry · 31 hook events / 63 entries all execute ·
Animus consume-and-emit proven with five controls · 190 .sh files,
0 syntax failures, error tier cleared · two separate Claude Code 2.1.238
scratchpad sessions wrote their own sinks and fired 10 distinct hook events.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt, or on macOS, where that tool does not exist: shasum -a 256 -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

🎁 BONUS — CmdPulse: real progress bars for every Claude Code tool call

"for everyone tired about waiting for the next update — I made something everyone was
searching for, because it is far easier than what I'm working on.

It took me about 1 hour to produce that, a function everyone was searching for, easy…
imagine what the router is capable of after 2 weeks…"

A live progress bar for every Claude Code tool call, rendered inside Claude Code's own
status line. It answers the one question the UI never answers:

Is it still working, or is it stuck?

⠸ Bash         ██████░░░░  61%   2m14s  cargo test --release
    └ [  5/20] seed 0004: 145832  (mean: 152340.2, 3.1s/seed)
◈ phase        ···                  8s  awaiting permission: Bash
██████░░░░ 47% | [Opus 5 (1M context)] xhigh ✻ | my-project  main* | ⧉ Inspect

Everything is local. Nothing is uploaded. No dependencies beyond bash and jq.

---

What it shows

element	meaning
██████░░░░ 61%	how far through the learned median time for this exact command shape
over (red)	already past its usual time — the honest "this might be stuck" signal
··· sweeping	fewer than 2 past runs, so no honest estimate exists yet
2m14s	live elapsed, readable to hours
└ [ 5/20] seed 0004…	the command's own stdout, streamed live (opt-in)
◈ phase	compaction, a pending permission prompt, or a subagent running
✓ / ✗	finished call, with true duration and start clock
⧉ Inspect	opens the full HTML dashboard

The percentage is an ETA against history this machine actually recorded — never a fake
byte count. A command CmdPulse has not seen twice gets a sweeping bar and the label ···,
because inventing a number would be worse than admitting there isn't one.

---

Why the phase rows matter most

Tool bars only cover PreToolUse → PostToolUse. Three things happen outside that window
and look identical to a freeze:

• context compaction — long, silent
• a permission prompt — the machine is waiting on you
• a subagent thinking between its own tool calls

CmdPulse wires all 31 Claude Code hook events and renders these as ◈ phase rows. Nine
carry meaning; the other 22 return immediately so they cost nothing.

---

Install

bash install.sh

Copies four scripts to ~/.claude/, backs up settings.json, and merges the config —
appending to any hooks you already have rather than overwriting them. No restart needed;
Claude Code re-reads settings.json live.

Requires bash and jq. On Windows use Git's bash (C:\Program Files\Git\bin\bash.exe);
the installer detects the platform and writes the correct command form.

Manual install and the Windows/POSIX settings forms are in REPRODUCE.md.
Every feature, flag and troubleshooting step is in USAGE.md.

---

The one number that matters: refreshInterval

"statusLine": { "type": "command", "command": "...", "refreshInterval": 3 }

Do not lower this to 1 without reading USAGE.md §Performance.

Claude Code re-runs the status line on a timer, and each new run aborts the previous one
still executing (#_(){ this.#s?.abort() }). On Windows a full render costs ~1.3s, because
a shell script pays ~14ms per subprocess spawn and this one makes ~75. At refreshInterval: 1
every render is aborted before it finishes and the status line goes completely blank —
which looks exactly like the tool being broken. At 3 each render completes.

On Linux/macOS spawns are far cheaper and 1 is usually fine. Measure before changing it:

time (echo '{"model":{"display_name":"T"},"workspace":{"current_dir":"/tmp"},
"context_window":{"total_input_tokens":5000,"context_window_size":200000,
"used_percentage":2.5},"cost":{"total_cost_usd":0}}' | bash ~/.claude/statusline.sh)

Keep refreshInterval comfortably above that number.

---

Live output streaming (opt-in)

export CMDPULSE_STREAM=1

Rewrites Bash commands via the updatedInput field of PreToolUse so they tee their output
to a log the bar tails. Your script's own progress lines then appear under the bar, live.

Exit codes are preserved — the wrapper ends with exit ${PIPESTATUS[0]}. This is not
cosmetic: a naive cmd | tee yields tee's exit status, silently turning a failed build
green. Verified against a command exiting 101 (naive form returned 0; shipped form returns
101; a succeeding command still returns 0). If you modify the wrapper, re-run that test.

Off by default, and only ever applied to Bash.

---

The other two surfaces

bash ~/.claude/cmdpulse/cmdpulse.sh        # live dashboard, 200ms, own clock
bash ~/.claude/cmdpulse/cmdpulse.sh top    # where your time actually goes
bash ~/.claude/cmdpulse/cmdpulse-web.sh    # HTML inspector: full input/output, copyable

cmdpulse.sh in a split pane is the only surface that can animate a bar while a fast
command runs — it owns its own clock instead of waiting for Claude Code to be idle.

wezterm-cmdpulse.lua is included for WezTerm users: same bar in WezTerm's status bar at
200ms. Inert on other terminals.

---

Honest limits

• Fast tools can't be caught live. Read averages 66ms, Write 24ms, Edit 111ms. The
  status line needs a 300ms quiet gap plus the render time, so only Bash-class calls are
  caught in flight. Everything else is shown by the completed-call row instead — and
  everything is recorded either way.
• The completed bar's fill is a replay, not live progress. Duration, start time and
  outcome are true measurements; the animation is reconstructed across the afterglow window.
  CMDPULSE_REPLAY=0 disables it.
• Hook cost is ~285ms per hook on Windows (bash + jq startup), so ~570ms per tool call.
  Meaningfully cheaper on Linux/macOS.
• runs/ grows two files per tool call and is not auto-pruned:
  find ~/.claude/cmdpulse/runs -type f -mtime +7 -delete

---

Privacy

~/.claude/cmdpulse/ records every command you run and its output in events.ndjson,
runs/ and (if streaming is on) stream/. This package ships none of that. Delete those
directories before sharing your own copy.

---

Uninstall

cp ~/.claude/settings.json ~/.claude/settings.json.bak
jq 'del(.statusLine)
  | .hooks |= with_entries(.value |= map(.hooks |= map(select((.command // "")
      | test("cmdpulse") | not))))' ~/.claude/settings.json.bak > ~/.claude/settings.json
rm -rf ~/.claude/cmdpulse ~/.claude/statusline.sh

---

Licensed under the same terms as the rest of this repository.

---

ETA

⠸ Bash  ██░░░░░░░░  20%   4s  ETA 16s  cargo build --release
⠋ Bash  ██████░░░░  60%  12s  ETA 8s   cargo build --release
⠇ Bash  ██████████ over  25s           cargo build --release

ETA is the learned median minus elapsed, shown only when that command signature has at
least 2 recorded runs. Fewer than that and you get ETA ? with a sweeping bar — the estimate
does not exist yet, and inventing one would be worse than saying so.

Rolling history

CMDPULSE_ROWS (default 3, max 12) shows the last N completed calls stacked above the status
line, each with mark, duration and start clock — so a burst of fast tools stays visible
instead of each overwriting the last.

Refresh rate — what is actually achievable

surface	interval	why
Claude Code status line	1s floor, ships at 3	Math.max(1,t)*1000 in the binary; sub-second is not configurable, and a render slower than the interval is aborted, blanking the line
cmdpulse.sh split pane	100ms	owns its own clock, independent of the host
WezTerm status bar	100ms	same

A status-line render currently costs ~1.0–1.7s on Windows (~75 subprocess spawns at ~14ms
each). Reaching 100ms there would need roughly an 11× speedup — a single-jq rewrite of the
render path, not a config change. Until then, the split pane is the fast surface.

---

Real progress, when the command reports it

A generic tool cannot know how much work an arbitrary command has left — nothing exposes
that. But the command itself often says so, and with CMDPULSE_STREAM=1 that output is
already on disk, so CmdPulse parses it:

⠴ Bash  ██░░░░░░░░ 25%  45s ETA 2m15s 5/20   cargo test --release
    └ [  5/20] seed 0004: 145832  (mean: 152340.2, 3.1s/seed)

[5/20], 12 of 34, 73% — all recognised. The ETA is then computed from the counter
itself (elapsed ÷ done × remaining) and needs no history at all.

bar colour	meaning
cyan	the number came from the command's own output — measured
violet/gold	estimated from the learned median for that signature
sweep + ETA ?	fewer than 2 recorded runs; no honest estimate exists

If a command reports nothing, the bar falls back to the median rather than inventing a
number. That fallback is verified by a control test, not assumed.

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 8.0.1 -- The Whole Packet, three ways

Patch: the gate learns to show its seals and to ask without demanding
theatre — and the armed sink comes back from the dead. The Socio ran
the voice gate in a live session on the newest CLI (2.1.237) and reported
two defects: the seals never showed in the summoned stanzas, and after
the second Stop the gate "stopped working". Both were reproduced in real
three-turn sessions before a line changed, and both trace to the refusal
the gate speaks when it blocks a Stop. The ten-turn blind acceptance run
the Socio then ordered surfaced a third, older defect nobody had measured
— and it is the biggest of the three.

Fixed — the seals ride the summons now

The router recorded a summons as Name|element|charter|bound; the DTD's
sigil never left the router, so the gate's refusal could not show it, and
a blind convening model — never once shown a seal — spoke correct but
sigil-less stanzas on every CLI version tested. Structural, not a
regression. Both router arms now write a fifth field,
Name|element|charter|bound|sigil, and the gate prints each missing
lens's seal beside its element (<rot:nova> ⚜️ (Nova): …). A four-field
row from a pre-8.0.1 router still parses; the seal simply goes unshown —
the gate never breaks on the old shape.

Fixed — the refusal no longer reads as an order to fabricate

B4's pattern returned, one CLI generation later. Blocked over a trivial
turn, the 2.1.237-era convening model refused the old demand — "I won't
manufacture three persona stanzas over nothing just executed or read" —
on every turn of the live repro, and since the gate consumes its summons
on the block either way, the observable symptom was a gate that held the
door once and then went quiet: "stopped working after the second Stop."
The model was right, which is the point. W4 (in the gate's own header)
already ruled that the TAG is the measurable commitment and the words
inside it are the model's honour; the refusal now says so out loud — a
lens with nothing real to report satisfies the contract with one plain
line inside its element saying exactly that, and the closing format adds
to the user's request, never overrides it. Re-run live on 2.1.237 after
the patch: stanzas with seals on every turn, honest-empty where nothing
ran, and a fourth turn with a real tool call attributed truthfully — the
gate satisfied without a single fabricated claim.

Fixed — every armed session ran sinkless; the fossil pin is retired

Found by the blind run: its Animus observer saw nothing for ten turns.
Six hypotheses died by controlled reproduction before the instrumented
rerun caught the router writing the summons and skipping the sink in the
same invocation — and the armed hook environment held the answer.
hooks/settings-merge.js had injected ROTMOE_DEBUG_LOG=<config>/ rot-moe/rot-route-debug.jsonl into the armed settings since 2026-08-09,
written when the sink was opt-in-only. 7.0.0 later gave the router its
per-session state-dir sink — the very file the Animus observer (organ 8)
pairs on — but SET wins over the default by design, the pinned directory
was never created, and the writability probe degraded the sink to OFF.
Every armed session since the pin existed ran with no sink at all; every
checker and the 8.0.0 paired probe invoked hooks directly, so none could
see it. Arm now retires exactly the pin it used to write (a user-chosen
value is kept byte-for-byte; the merge validator learned the one
sanctioned mutation, deletion-safe on both images), and the per-session
sink takes over. Re-run live: the sink grew every turn (188 lines, 94
route records), the observer queued remarks from measured triggers, the
queue file was consumed FIFO on camera, and the worker-side ear spoke
(animus) remarks into the envelope on three of five turns — the whole
of organ 8 alive in a blind session for the first time under ARM.

Held — the contract grew six rows, each falsified first

checker/voice-contract.sh D10 now also holds: every summons row carries
five fields with a non-empty seal; the blocking refusal shows the seals
beside their elements; and the refusal carries the honest-empty sanction.
A new D15 holds the pin's retirement in both directions: a fresh arm
writes no sink pin, a re-arm retires the pre-8.0.1 pin, and a user-chosen
ROTMOE_DEBUG_LOG survives untouched. All six were made to fail before
being trusted — a four-field summons file fails the row check, the
pre-patch gate fails both wording checks, and the pre-patch merger,
run against D15's own probe, injects the pin and goes red.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 8.0.0 -- The Whole Packet, three ways

Major: Animus — the paired observer. 7.0.0 let a lens speak on the
result; 8.0.0 gives the whole roster a second pair of eyes. Two agents on
one task: a worker session solves it, and an observer process
watches what the worker actually does — its measured event stream, never
its prose — and injects the perspective the worker forgot, mid-run, through
the same channel the voices already use. The eighth organ, and the origin
of its name: self-distillation through hard study.

Added — the observer: the router applied to its own records

hooks/animus-observe.sh, an operator tool (nothing registers it, it
blocks no turn, POSIX-only by design and the DTD says so). It tails the
worker's per-session debug sink at one-second cadence and fires on eight
measured triggers, every threshold a declared ENV row (ENV.26–32),
never a judgment a checker could not replay: AntiVenom on a recurring
result anomaly; Chroma on consecutive actions each costlier than the last,
and once per run when the task text routes PREDICTIVE and the stream never
goes there; Venom on prompt turns with no act between; Soleil on actions
growing longer every time; Eidolon on one lane+stem pair looping; Violet
once per run when the task routes EMPATHIC and the stream never visits the
register; and the Claude lens on a PreToolUse whose Post never lands —
the stall named while it is still happening, no timeout waited out.
Budgets are law: one remark per event, three per lens per run — a critic
that repeats is wallpaper, the blind campaign's own verdict. Every remark
appends to two distillates (project .rot-moe/, plus a global one in the
state dir; ENV.33/34 override the paths) together with the measured
next-action delta — the three events before the injection against the
three after, quoted from the sink. The next run loads global first, then
project. commands/animus.md is the launch order.

Added — the worker-side ear, in both router arms

Under ROTMOE_ANIMUS=1 (ENV.25), each PostToolUse consumes at most
ONE queued remark FIFO from animus-queue.<session> and speaks it inside
the owning lens's declared element, tagged (animus) so remark and
gauge stanza can never be confused. The queue is cross-process, so both
sides are rename-atomic — the observer never touches an existing queue
file, the consumer takes the whole file before reading a byte — and a
consumed remark can never resurrect. A lens name outside the nine-element
roster is refused AND dropped, so a compromised queue writer can neither
mint a tenth voice nor jam the queue head. Empty queue = not a byte;
ROTMOE_VOICE=0 silences remarks with the rest of the voice.

Added — the sentinel's firing is now a record

Until this release a sentinel clause went to the envelope and nowhere
else: whether it ever fired was unfalsifiable from the log, the same
defect class the event field closed in 6.0.x — and the observer's
recurrence trigger would have had nothing to count. Both arms now write
one kind:"anomaly" line (shape and tool, central sink only) when a
clause fires, with the shape derived from the clause text itself so record
and clause cannot name different verdicts.

Added — the contract around all of it

checker/voice-contract.sh D14: fifteen rows with negative controls —
consumption, FIFO order, empty-queue silence, the roster refusal and its
drop, the unarmed worker leaving the queue untouched, the off-switch
keeping the queue standing, a writer's half-landed tmp file staying
invisible, the anomaly record and its healthy-result control, the observer
firing on a planted recurrence and staying silent over an empty sink, and
the command file bound to the observer and the arm switch.
checker/cross-diff.sh gained an Animus phase: identical planted queues,
per-arm state dirs, envelopes compared byte for byte — refusal and
off-switch included, with a live control proving a genuine difference is
visible. The live paired probe ran the whole loop as two real processes:
two planted blanks, the remark queued within one poll, spoken on the
worker's third event.

Held open — the Lean debt, named

The queue's take-and-remainder semantics and the trigger predicates are
held by the executable contract and the cross-arm comparison, not yet by
theorems — bench/ungap-7.1.md N10 carries that debt by name rather
than letting an organ ship pretending it was proved.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed

RoT MoE 7.0.0 -- The Whole Packet, three ways

Major: the working share. 6.0.2 gave the lenses a dynamic share of the
prompt turn; 7.0.0 extends the share to the work itself. The lenses now
speak on the result — the moment a command comes back wrong-shaped, not
a timeout later — and the whole tree was re-studied, re-measured and
compressed around that idea until the un-gap ledger emptied.

Added — the result sentinel: a lens speaks on the result itself

The Socio's scenario, delivered: a command stalls, returns a blank, or
returns something in between — and a lens notifies the convening model at
the moment the evidence exists, because hooks fire on harness events,
behind the reasoning layer. No timeout is waited out. On PostToolUse,
three clauses in precedence order, every guard a measured payload
field: a command the harness reports interrupted (the Claude lens — what
follows the cut was never run); a blank result without the harness's own
no-output sanction (Anti-Venom); a Write that stored zero bytes where
content was given (Anti-Venom, guarded on the input side so intentional
empty files stay silent). One clause at most, promoted onto the JSON
envelope with the marker; silence is the healthy state; ROTMOE_VOICE=0
silences it with the rest of the voice. The Edit tool's response shape was
not measured, so it is not read — both arms say so in place. The old
"Post is a deduplicated echo" comment gained its measured exception: a
result-aware line is new information, and the design note explains why.

Added — the payload survey: measure the harness before reading it

The sentinel's fields were not taken from documentation — the docs were
wrong. ROTMOE_DEBUG_PAYLOAD=1 (ENV.24) surveys each hook payload's
key names — never a value — into its own per-session sink. Run live,
it overruled the documented schema on the decisive fields: no exit code
reaches the hook; interruption and sanctioned silence do. The sentinel
ships on what was measured, and the instrument ships with it.

Added — the goldens: one arm is enough to catch its own drift

Arm-vs-arm agreement cannot kill a single-arm mutation on a machine with
one arm. Two generated goldens close that: per-row hashes of the reminder
corpus, and per-profile gauge records carrying the full-precision lens
arrays — added after a planted λ retune provably survived the 2-decimal
human line and died against the record's digits. Both are rewritten only
by a deliberate --make-golden act with a banner; a stale golden is a
failure, not a shrug. Two checker mutants flipped from INEXPRESSIBLE to
KILLED on a PowerShell-less box, and the ones that remain machine-bound
are named as such instead of counted green.

Added — the outcome study, preregistered before any run

bench/ROT-STUDY-PREREGISTRATION.md: three arms on matched real tasks,
outcome-blind grading against keys written with the tasks, and the blind
campaign's verdict — "wallpaper with a tax" — standing as the null
hypothesis. The design commits to printing a null as a null.

Fixed — opting out of the gate no longer opts out of the cleanup

A summons written while the gate was armed survived every ROTMOE_GATE=0
turn, so the first Stop after re-arming was blocked for a turn long dead.
Both router arms now clear the summons even when the gate is off, and the
voice contract replays the exact scenario as a sequence probe.

Fixed — a skip is a skip everywhere

The portability suite's sections this machine cannot run used to vanish
from the verdict. They are counted now, the summary names them, and the
suite exits 3 — the repository's did-not-run code — instead of wearing a
pass. A real failure still outranks a skip.

Fixed — a reading that misleads is worse than none

rot env get read only two of the loader's three files and interpolated
its key into a regex. It now reads the loader's exact file order —
ROTMOE_ENV first — and refuses regex-shaped keys with the loader's own
charset, so what get prints is what load would use.

Changed — the front page says what the tree measures, in half the lines

A truth pass fixed every stale claim the re-study surfaced: the seventh
organ joined its own table; the contract check count and module counts were
re-measured; the voices section was re-captured live from the shipped
tree, dynamic stanzas and sentinel envelope both quoted with their prompts;
comparison totals this machine cannot measure were replaced by what the
goldens actually hold. Then the compression: the front page dropped from
2,334 lines to 1,216 by moving its depth — the module arguments, the Lean
essay and corpus, the lens benchmark, the tips, the Easter Egg — verbatim
into five docs/ files, each carrying its licence header and a backlink.
A new Measured in the field section puts the two campaigns on the
page: four graphs drawn from the bench records themselves, the
verdict-shaped gauge stated plainly, the 1-vs-52 gate-pressure contrast,
and the outcome question left honestly open. The citation gate's surface
follows the content: README plus exactly the five depth files, history
logs excluded by the same scope law the count binder already states.

Changed — the charters cite what exists and their examples add up

The stuck-head exception cited a line that holds different text and quoted
a sentence that exists nowhere; three citers now point at the prover's
real Reporting contract. Nova's transcribed gauge bounds name their true
source and state that the router reads per-lane bands. Violet's worked
example adds up — four roles, four deltas, entropy inside her own band —
with the correction disclosed in place. Chroma's template no longer puts
all its probability on the branches it shows. The Claude lens cites the
README by section, because this very release moved the line numbers.
Deliberately untouched: Eidolon's hybrid-table defect disclosure, which is
the charter working, not drifting. The Lean sweep found the same disease
in two proof modules — front-page citations by line number, both now
pointing at the wrong text — fixed the same way, by section; everything
else that sweep surfaced is real, out of scope, and opens
bench/ungap-7.1.md so the next release starts where this one measured.

---

Verify any download against its published checksum: sha256sum -c SHA256SUMS.txt

---

Topics — 42 tags, generated from .github/tags.txt

#Specification #ExpertRouting #KernelVerified #Bash #AgenticWorkflow #MachineChecked #Router #OpenSource #Copyleft #CliTool #Leanchecker #Eupl #PromptEngineering #ClaudeCode #FormalVerification #Anthropic #Spdx #StaticAnalysis #EnsembleMethods #ProofAssistant #Powershell #AiAgents #Mathlib #Moe #FreeSoftware #VerifiedSoftware #Plugin #MutationTesting #Agpl #LlmTooling #ProofEngineering #Lean4 #NonProfit #ReuseCompliance #DeveloperTools #Sigmoid #DependentTypes #Hooks #ClaudeCodePlugin #TheoremProving #MixtureOfExperts #DualLicensed