musubix5

0.2.0 · GitHub Copilot CLI only · Node.js ≥20 · TypeScript · MIT

日本語

What changed from musubix2 to musubix5 (Japanese)

GitHub Copilot can plan, generate, edit, test, and review software. musubix5 adds repository-local specifications plus deterministic, fail-closed checks over the evidence required by the repository's configured quality profile: requirements → constitution → design/ADRs → implementation → traceability → quality evidence.

Learned from musubix2's concepts, rebuilt cleanly in three workspaces. No artifact compatibility or migration is promised. This repository does not guarantee correctness simply because IDs are linked or requirements are satisfiable.

Why GitHub Copilot alone is not enough

Copilot is the implementation engine. It understands a request, explores the repository, proposes a plan, edits files, runs tools, and explains the result. That is necessary, but a successful conversation is not durable proof that:

• the implemented behavior matches an explicit, measurable requirement;
• every requirement is connected to design, code, and an authoritative test;
• Red really failed before Green passed without the test being rewritten;
• test, graph, formal, and quality results still match the current source;
• a requirement change propagated through all affected artifacts in order;
• a policy was not weakened merely to make the final gate pass.

Conversation text such as “tests passed” or “implementation complete” is not enough because it can become stale, omit scope, or disappear outside the repository. Copilot should remain responsible for reasoning and development; musubix5 makes the completion criteria persistent and machine-checkable.

| GitHub Copilot provides | musubix5 complements it with | |---|---| | Planning, coding, refactoring, and tool execution | Repository-local SDD Skills that require explicit requirements, design decisions, implementation links, and completion conditions | | Test generation and runner execution | Structured TEST identities, native-report normalization, and verified Red/Green/Refactor evidence | | Explanations of what changed | Typed requirement → design → code → test traceability and bidirectional impact analysis | | Repository exploration | Deterministic Code Graph indexing, unresolved-local dependency diagnostics, and architecture gates | | Suggestions for constraints and invariants | Optional Z3/Lean consistency checks and model-to-passing-test correspondence | | A session-level completion report | Freshness, fingerprints, input-stability checks, protected policy baselines, attestations, and a fail-closed readiness gate |

musubix5 does not replace Copilot, add another coding agent, or claim that formal satisfiability proves implementation correctness. Copilot performs the development; musubix5 records the specification, checks the evidence, rejects stale or incomplete required evidence, and leaves a reviewable answer to “why does this repository's configured policy consider the change ready?”

Quick start

There are two ways to load musubix5's skills into a project — pick exactly one per project, never both:

• npm install (this section, recommended): add musubix5 as a project dev dependency, then run npx musubix5 init to copy the skills into .github/skills/ and scaffold starter .musubix/ artifacts. Version and upgrades are tracked in your project's package.json/lockfile (npm install ...@latest + npx musubix5 upgrade); see Upgrade. Recommended because the skills and starter SDD artifacts are committed to the repository itself, so every contributor and CI job gets the same reproducible setup without each of them running a separate plugin install.
• copilot plugin install (native plugin/marketplace route): register musubix5 directly with Copilot CLI's own plugin manager — no npm dependency is added to the project, and no files are copied into .github/skills/. Upgraded with copilot plugin update musubix5 (or the marketplace equivalent). See Distribution options for the exact commands.

The rest of this section documents the npm install route.

For a reproducible project-local installation:

npm install --save-dev --save-exact musubix5@latest
npx --no-install musubix5 --version
npx --no-install musubix5 init --dry-run
npx --no-install musubix5 init
copilot

For a one-time evaluation without pinning subsequent Skill-driven CLI runs:

npx musubix5@latest --version
npx musubix5@latest init --dry-run

Install the exact local dependency before relying on generated Skills in continued development; their commands intentionally use the repository-local npx --no-install musubix5 executable.

To build the repository itself:

git clone https://github.com/nahisaho/musubix5.git
cd musubix5
npm install
npm run build
node dist/packages/cli/src/main.js --help

Ask Copilot: “Use sdd-change to add this feature and propagate it through the specification, implementation, traceability, and quality gate.” All eight skills instruct Copilot to follow your input language (English/Japanese).

init (install alias) copies repository-local skills and creates starter SDD artifacts. It preserves existing files, merges a cache ignore rule, and is idempotent. --force replaces only named bundled/managed paths; it does not delete unrelated files. Review its dry-run first. No Copilot global settings, MCP, LSP, hooks, or project instructions are overwritten. Symbolic-link write targets and paths escaping the project are refused.

The starter is deliberately not release-ready: replace its example, implement and test it, and configure real check commands before expecting the gate to pass.

Upgrade

The upgrade command is included in musubix5 0.2.0. Its compatibility contract is based on the command introduced in musubix3 0.1.14. Check published musubix5 versions with npm view musubix5 versions.

For the npm-installed route (init/repository-local skills):

npm install --save-dev --save-exact musubix5@latest
npx --no-install musubix5 upgrade --dry-run
npx --no-install musubix5 upgrade

upgrade refreshes only the bundled .github/skills/sdd-* files that differ from the installed package version. It never creates, replaces, or deletes .musubix/config.json, .musubix/policy-baseline.json, .musubix/constitution.md, ADRs, feature artifacts, evidence, or .gitignore — those are yours to keep customizing. It is idempotent: it compares against the currently installed package's skill files, so running it again without first installing a newer musubix5 version reports every skill file as unchanged. Review --dry-run first, same as init.

init --force remains available for replacing bundled/managed paths more broadly (including .musubix/config.json, constitution.md, and the starter feature's requirements.md/design.md), but it overwrites customized content in those files, so prefer upgrade for routine version bumps.

For the native plugin route:

copilot plugin update musubix5

For the native marketplace route:

copilot plugin marketplace update musubix5-marketplace
copilot plugin update musubix5

These delegate to Copilot's own plugin manager, which re-fetches plugin.json/the marketplace catalog; they do not touch .musubix/ at all (only the npm-installed route manages .musubix/ artifacts).

Distribution options

Choose one skill-loading route to avoid duplicate skill names.

Native plugin (direct)

Pick exactly one of the following (not both):

copilot plugin install ./musubix5            # local clone, from its parent directory

copilot plugin install nahisaho/musubix5     # published GitHub repository, no local clone needed

plugin.json at the repository root is the source of truth and references .github/skills/. The plugin contains skills, not an agent runtime or background services. Git installs do not compile/install the npm engine: build the clone or install the npm package separately when running npx musubix5 commands.

There is a third way to run the same copilot plugin install, useful only if you want a durable local path instead of an ephemeral npx cache — do this instead of, not in addition to, the two commands above:

npm install --save-dev --save-exact musubix5@latest
npx --no-install musubix5 plugin-install

plugin-install only calls copilot plugin install <absolute-package-root> for you; it does not edit Copilot internals, and it is unrelated to the npm-installed skill-copy route in Quick start — it never runs init and never copies files into .github/skills/. Do not run both this and npx musubix5 init in the same project.

Native marketplace

copilot plugin marketplace add nahisaho/musubix5
copilot plugin install musubix5@musubix5-marketplace
# Local development:
copilot plugin marketplace add ./musubix5

The catalog is .github/plugin/marketplace.json; its plugin source is .. These flows use the native plugin interface.

Repository-local skills / npm installer

Run npx --no-install musubix5 init after installing the exact local dependency, or copy .github/skills/sdd-* there yourself. Start Copilot in that trusted project. init --root <dir> targets another project; --feature <slug> changes the starter directory and ID prefix. Installing another feature does not reset existing configuration.

Skills and native boundaries

| Skill | Purpose | |---|---| | sdd-change | End-to-end feature/change/fix propagation and completion gate | | sdd-requirements | Six controlled EARS forms and measurable constitution | | sdd-design | Explicit responsibilities/interfaces/constraints, ADRs, diagrams | | sdd-implementation | Native editing with requirement-linked code and tests | | sdd-traceability | Generated coverage, dangling links, bidirectional impact | | sdd-quality | Actual verification commands, policy, readiness evidence | | sdd-knowledge | Local artifact/Git retrieval, not conversational memory | | sdd-formal-codegraph | Optional consistency checks, compiler graph, architecture | | sdd-parallel-dispatch | Dispatch approved assignments without exceeding plan concurrency | | sdd-agent-assignment | Execute one owned-path assignment in its managed worktree | | sdd-integration-verification | Integrate verified ranges, verify, hand off, and clean up |

Use native Copilot for planning, editing, research, review, security review, memory, code navigation/LSP, MCP management, and subagent/fleet/task coordination. musubix5 does not implement those services, generic code/test generation, orchestration, a scheduler, MCP server, Claude support, an interactive REPL, or a resident watcher. status, query, impact and --changed provide one-shot value. Skills may combine neural proposals from Copilot with symbolic checks; there is no separate “neurosymbolic AI” model or claims of learned verification.

Workflow

Natural-language requests such as “develop/build/create/implement X” activate sdd-change as the mandatory first Skill. It elicits and validates requirements and design before implementation; only an explicit request to implement existing approved artifacts may enter sdd-implementation directly. The implementation Skill fails closed when those validated artifacts are absent or invalid. When material context is missing, requirements elicitation asks one highest-priority question at a time and waits for the answer; it does not batch questions or finalize requirements while blockers remain.

1. Use native planning/research to establish intent and measurable acceptance.
2. Record change-record CHANGE-ID impact, edit/validate requirements, run a rubber-duck review of the requirements document and fix every finding (repeat review/fix until zero issues remain), record the requirements checkpoint, then obtain explicit artifact-bound human requirements approval before design.
3. Design explicit components, record trade-offs in ADRs, run a rubber-duck review of the design document/ADRs and fix every finding (repeat until zero issues remain), record design, then obtain explicit artifact-bound human design approval before implementation.
4. Write an annotated behavior test, record a structured failing tdd red, then record the change red checkpoint.
5. Implement the minimum change, record implementation, run passing tdd green, then record green and refactor. For a change with multiple requirements, red/implementation/green may instead be recorded once per requirement subset (an independent batch per subset), completing each requirement's Red-Implementation-Green loop before moving to the next, instead of completing every requirement's Red before any Implementation.
6. Add trace annotations, build graphs, inspect impact and fix missing coverage.
7. Configure real checks and run the candidate gate --changed. Run a rubber-duck review of the release/quality evidence summary and fix every finding (repeat until zero issues remain). After every required non-approval check passes, obtain explicit human release approval, rerun the gate/status, and only then commit, push, publish, or deploy.

Any AI-generated documentation deliverable (requirements, design, ADRs, the CHANGE document, or release/quality evidence summaries) goes through this rubber-duck review/fix loop until zero issues remain before the corresponding human approval step is requested.

Parallel implementation workflow

After requirements and design approval, put the active feature's Parallel-Policy: JSON declaration in the first policy-bearing artifact listed by the active CHANGE's design approval manifest. This makes policy ownership deterministic when the manifest also contains unrelated feature designs. Validate and create the bound plan with parallel plan, then prepare its managed Git worktrees. sdd-parallel-dispatch requests assignment instructions without exceeding persisted concurrency; each sdd-agent-assignment changes only its declared worktree and owned paths, and the CLI verifies every commit in the result range before accepting it.

provisionCommands declares trusted argument-array commands that prepare each managed worktree before focused or integration verification. The starter design uses npm ci --ignore-scripts; replace it with the repository's lockfile-based installer when the project does not use npm.

Use parallel status for persisted plan, assignment, and integration state. After all assignments complete, sdd-integration-verification performs deterministic integration, required verification, fast-forward-only candidate handoff, and branch-retaining cleanup. Stale plans permit only explicitly targeted status and stale cleanup; dirty or unconsumed worktrees are retained.

npx musubix5 requirements validate .musubix/features/example/requirements.md --json
npx musubix5 constitution validate --json
npx musubix5 approval prepare requirements --json
npx musubix5 approval record requirements --approver "Requirements Owner" --artifact-sha256 "$REVIEWED_HASH" --confirm
npx musubix5 design validate .musubix/features/example/design.md --json
npx musubix5 design c4 .musubix/features/example/design.md
npx musubix5 approval prepare design --json
npx musubix5 approval record design --approver "Design Owner" --artifact-sha256 "$REVIEWED_HASH" --confirm
npx musubix5 change-record CHANGE-0001 design --requirement REQ-EXAMPLE-001
npx musubix5 tdd red TEST-EXAMPLE-001 --requirement REQ-EXAMPLE-001 --command test
# Implement the minimum behavior without changing the test.
npx musubix5 tdd green TEST-EXAMPLE-001 --requirement REQ-EXAMPLE-001 --command test
npx musubix5 tdd refactor TEST-EXAMPLE-001 --requirement REQ-EXAMPLE-001 --command test
# A change declaring REQ-EXAMPLE-001 and REQ-EXAMPLE-002 may record red/implementation/green
# once per requirement subset instead of once for the whole change:
npx musubix5 change-record CHANGE-0001 red --requirement REQ-EXAMPLE-001
npx musubix5 change-record CHANGE-0001 implementation --requirement REQ-EXAMPLE-001
npx musubix5 change-record CHANGE-0001 green --requirement REQ-EXAMPLE-001
npx musubix5 trace build
npx musubix5 trace check --strict --json
npx musubix5 graph index
npx musubix5 graph impact src/service.ts
npx musubix5 gate --changed --json
npx musubix5 approval prepare release --json
npx musubix5 approval record release --approver "Release Owner" --artifact-sha256 "$REVIEWED_HASH" --confirm
npx musubix5 gate --changed --json
npx musubix5 approval validate --json
npx musubix5 status --json

A requirement already satisfied as a side effect

tdd red rejects recording a Red phase for a test that is already passing (TDD_TARGET_RESULT). This is correct: it is not a bug when a correct, general implementation written for one requirement also happens to satisfy a separate, not-yet-implemented requirement (for example, a general capacity-aware assignment algorithm that also correctly handles a "no resource available" edge case required by a different requirement). There is deliberately no --already-satisfied-by-style declaration to bypass Red for this case: a human declaration that a requirement is "already satisfied elsewhere" is not measured evidence, and accepting one would let an unimplemented or incorrectly implemented requirement pass gate on an unverified claim.

The recommended practice is to prove the Red genuinely, the same way as any other requirement, by briefly and deliberately narrowing the scope of the already-correct shared implementation so the new requirement's test fails, recording tdd red, then restoring the correct implementation for tdd green:

# The shared implementation is already correct; temporarily narrow it
# (e.g. re-add the special case the general algorithm already subsumes)
# so TEST-EXAMPLE-002 genuinely fails.
npx musubix5 tdd red TEST-EXAMPLE-002 --requirement REQ-EXAMPLE-002 --command test
# Restore the correct (already-written) implementation; no other code changes.
npx musubix5 tdd green TEST-EXAMPLE-002 --requirement REQ-EXAMPLE-002 --command test

Keep the narrowing edit local and revert it in the same step as recording Green; do not leave the weakened code committed at any point.

A brand-new module for a from-scratch requirement

tdd red requires a collected and executed failing test, not merely a test file that exists: if the test imports a source module that does not exist yet, the runner fails at collection time (0 tests run) instead of failing an assertion, and tdd red correctly reports this as an invalid Red (TDD_REPORT_INVALID). For a vitest/jest adapter, the thrown error now appends the underlying suite collection-failure message (for example Cannot find module '../src/service.js') after No annotated TEST-* identities were found, to make this cause visible immediately instead of requiring a separate investigation.

The recommended practice for a genuinely new module is the same stub-then-correct technique as above: create a compiling implementation file with a deliberately wrong body first, so the runner can collect and execute the test (and it fails on the wrong behavior, not on a missing import), then implement the correct behavior for Green:

# src/service.ts does not exist yet; create it with an intentionally wrong body
# so the test can be collected and genuinely fails on assertion, not on import.
npx musubix5 tdd red TEST-EXAMPLE-003 --requirement REQ-EXAMPLE-003 --command test
# Replace the stub body with the correct implementation.
npx musubix5 tdd green TEST-EXAMPLE-003 --requirement REQ-EXAMPLE-003 --command test

Command reference

All analysis commands accept --root <directory> and --json. Files resolve relative to that root; access outside it is refused. plugin-install uses the installed package root. Exit codes: 0 successful operation, 1 rejected validation/gate or requested solver failure, 2 usage, I/O or malformed config. status is informational (exit 0 even if not ready); inspect gate.ready.

| Command | Behavior | |---|---| | init [--dry-run] [--force] [--feature slug] | Preserve-first skills/artifacts installation; install alias | | upgrade [--dry-run] | Refresh bundled skill files only; never touches config, constitution, or feature artifacts | | plugin-install | Invoke native Copilot installer (no internal config edits) | | requirements validate <file> | IDs, priorities, declared/detected EARS pattern | | requirements scaffold <slug> [--title <text>] | Create .musubix/features/<slug>/requirements.md from a fixed placeholder template; never overwrites an existing file | | constitution validate [file] | Versioned principles and measurable rule definitions | | design validate <file> | Fields, global requirement IDs, existing ADR references | | design scaffold <slug> | Create .musubix/features/<slug>/design.md from a fixed placeholder template; never overwrites an existing file, and does not require a pre-existing requirements.md | | design c4 <file> | Mermaid component/dependency diagram from explicit fields | | approval prepare <requirements\|design\|release> | Display the exact deterministic manifest and hash for human review | | approval record <stage> --approver <name> --artifact-sha256 <hash> --confirm | Record approval only if the reviewed hash is still current | | approval validate | Report each approval as approved, missing, or stale; never infer approval from validation | | trace build | Generate global trace snapshot and feature copies | | trace check [--strict] | Dangling IDs, stale inputs/paths, mandatory coverage | | trace impact <id-or-path> | Bidirectional breadth-first traversal with explanation paths | | graph index [--changed] | Compiler imports, declarations and best-effort call targets | | graph impact <symbol-or-path> | Conservative reverse-import closure; path#name disambiguates | | graph cycles | Strongly connected components; exit 1 when cycles exist | | graph gate | Fresh index + architecture rule/cycle checks | | knowledge build | Markdown and bounded Git evidence index | | knowledge query <text> [--limit 10] | Deterministic TF-IDF/cosine results and staleness flag | | formal generate <file> [--format both\|smt2\|lean] | Reproducible solver inputs with SHA-256 evidence | | formal doctor | Probe Z3, Lean, and lake env lean availability and versions | | mutation doctor | Probe language-aware local mutation engines and show setup recommendations | | formal check <file> [--solver auto\|none\|z3\|lean] | Check the explicit Boolean/conditional/numeric/temporal/transition model | | model-correspondence validate | Revalidate Formal JSON → generated trace → authoritative passing test evidence (run evidence refresh first to generate its evidence file) | | evidence refresh [--changed] | Regenerate derived evidence through the same fail-closed gate pipeline | | mutation validate | Revalidate requirement-scoped schema-v1 killed-mutant evidence | | mutation identity <REQ-ID> <TEST-ID> <sourcePath> <operator> <line> <column> | Print the deterministic MUT-* identity a mutation report must declare | | parallel plan validate\|create <file> | Validate or persist an approval-, generation-, candidate-, policy-, and command-bound plan | | parallel prepare\|assignment ... | Create managed worktrees and process assignment instruction, heartbeat, result, failure, and retry | | parallel integration start\|verify\|reopen ... | Integrate verified ranges and verify or reopen a dependency-closed assignment set | | parallel handoff\|status\|cleanup ... | Fast-forward the candidate, inspect persisted state, or perform branch-retaining cleanup | | tdd validate | Validate persisted Red/Green/Refactor order, fingerprints, durations, and hash-chain evidence | | tdd red\|green\|refactor <TEST-ID> --requirement <REQ-ID> --command <name> | Execute and record a verified TDD phase. Recording the project's first tdd cycle (any red call while .musubix/evidence/tdd.json has zero cycles) makes gate's tdd check required project-wide, for every mandatory requirement, not just the ones touched by the current change; each uncovered requirement then surfaces as TDD_REQUIREMENT_UNCOVERED. approval record release always runs the full (non---changed) gate, so it is blocked by any resulting TDD_REQUIREMENT_UNCOVERED diagnostics. tdd migrate cannot be used to bulk-onboard previously-uncovered requirements: it only re-fingerprints a requirement that already has a valid Green cycle. tdd red prints/returns a TDD_ADOPTION_PROJECT_WIDE warning (in a warnings array, separate from diagnostics) the moment this first cycle is persisted, listing every other still-uncovered mandatory requirement. | | workflow-record <skill> <phase> --status <status> | Record a compact self-reported workflow declaration | | workflow waiver record <code> --skill <skill> --phase <phase> --recorded-at <timestamp> [--index <n>] --approver <name> --reason <text> --confirm | Record an audited, bounded downgrade of one declaration-scoped workflow reconciliation diagnostic (WORKFLOW_SKILL_NOT_INVOKED, WORKFLOW_INVOCATION_ORDER, WORKFLOW_INVOCATION_INCOMPLETE, WORKFLOW_INVOCATION_FAILED, or WORKFLOW_INVOCATION_REUSED) to a non-blocking waived status; a paired WORKFLOW_BINDING_MISSING diagnostic sharing the same declaration scope is downgraded together with it. It cannot waive WORKFLOW_INVOCATION_UNVERIFIED, which only workflow-verify having actually run this session can resolve | | workflow waiver record-all --approver <name> --reason <text> --confirm | Bulk variant of workflow waiver record: waives every currently-outstanding waivable declaration-scoped diagnostic across the whole reconciliation report in one all-or-nothing call, instead of one record invocation per diagnostic. Rejects (recording nothing) if any bulk waiver precondition fails first — malformed waiver evidence, an invalid waiver chain, a blank --approver/--reason, or a WORKFLOW_INVOCATION_UNVERIFIED diagnostic (which workflow-verify must resolve first; no per-declaration or bulk waiver can substitute for workflow-verify never having run). Each waived declaration-scoped diagnostic's paired WORKFLOW_BINDING_MISSING is downgraded together with it, identically to the existing single-record command. With zero remaining candidates (already waived, or none present) it succeeds idempotently and records nothing | | workflow-sanitize <copilot.jsonl> <output-file> [--session-id <uuid>] | Remove messages and non-Skill tool data before review or strict verification | | workflow-verify <copilot.jsonl...> [--strict] [--session-id <uuid>] | Reconcile Skill events; compatible mode accepts multiple transcript files (concatenated in chronological session order) so declarations whose invocation occurred in an earlier Copilot CLI session can be reconciled; --strict/--session-id still require exactly one file | | attestation oidc-audience --key-id <id> [--public-key-file <pem>] | Derive the GitHub custom audience that authorizes a signing key | | attestation payload --provider <name> --run-id <id> --key-id <id> [--public-key-file <pem>] [--github-oidc-token-file <jwt>] | Emit canonical unsigned CI payload for external signing | | attestation verify | Verify static-key or GitHub OIDC-authorized Ed25519 provenance | | change-record <CHANGE-ID> <phase> --requirement <REQ-ID...> [--allow-unchanged] [--dry-run] | Record ordered artifact/TDD fingerprints for a staged change. impact/requirements/design/quality require the change's full requirement ID set; red/implementation/green also accept a proper non-empty subset, recorded as an independent per-requirement batch, so a multi-requirement change can be completed with an interleaved per-requirement Red-Implementation-Green loop instead of one global batch. Rejects with a non-zero exit and a stable *_UNCHANGED_AT_RECORD diagnostic (leaving changes.json/order.json untouched) when a phase's fingerprint is byte-identical to the immediately preceding phase's, since that mistake is otherwise only caught much later by trace check --strict/gate, at which point the append-only evidence store makes it unfixable. --allow-unchanged bypasses this check for the requirements phase only (the one case sdd-change documents as legitimate: a defect fix that intentionally leaves its requirement unchanged) and persists a durable marker so later validation does not re-flag it. --dry-run previews the exact success/rejection outcome, including every existing check, without persisting anything. Each recorded phase/batch stores both order (the verified, gate-checked logical append sequence from order.json — the only field guaranteed correct and monotonic per change) and recordedAt (an independently captured wall-clock timestamp with no ordering guarantee relative to order); gate reports a non-blocking CHANGE_RECORDEDAT_OUT_OF_ORDER warning when a change's recordedAt values disagree with its order sequence | | config lint | Report configured commands whose args reference repository-relative paths that do not exist | | config scaffold | Propose native test-command entries for detected Go/Rust/Maven/Python/Node toolchains without writing .musubix/config.json | | gate [--changed] [--feature <name>] | Fresh full checks plus actual configured commands; persist evidence. --feature scopes requirements/design/trace/tdd/change-history/change-completeness checks to one feature as a diagnostic view; never a substitute for the repository-wide gate | | status | Artifact counts and readiness/staleness summary |

--changed reads staged, unstaged, untracked and renamed/deleted paths from Git. It reports affected files but conservatively recomputes all deterministic checks and executes all configured commands. This avoids unsafe incremental skips. There is no daemon, polling loop or background service. Workflow evidence automatically requires workflow. TDD evidence automatically requires tdd; a .musubix/changes/CHANGE-*.md document additionally requires tdd, change-history, and change-completeness, even when omitted from requiredChecks.

Artifact schema (v1)

.github/skills/sdd-*/SKILL.md
.musubix/
  config.json
  constitution.md
  features/<slug>/
    requirements.md
    design.md
    trace.json                 # generated; never hand-edit
  decisions/ADR-0001.md
  evidence/
    quality.json                # actual gate report, initially skipped
    workflow.json               # declarations plus optional strict transcript/session evidence
    tdd.json                    # append-only phase hash chain and TDD cycles
    changes.json                # staged change checkpoints
    order.json                  # shared monotonic TDD/change chronology ledger
    performance.json            # deterministic operation-budget observations
    model-correspondence.json   # Formal model → trace → fresh passing-test correspondence evidence
    mutation.json               # fresh requirement-scoped mutation executions
    attestation.json            # optional externally signed CI provenance
  cache/                       # ignored; generated indexes and solver inputs

Requirements and design

---
schemaVersion: 1
feature: auth
---
## REQ-AUTH-001: Reject expired sessions
Priority: must
Type: functional
Pattern: event-driven
Statement: When a session expires, the system shall reject the request.
Acceptance: An expired-session request produces HTTP 401.
Formal: {"kind":"conditional","condition":"session.expired","consequence":"request.rejected"}

## DES-AUTH-001: Session guard
Responsibilities: Reject requests whose session has expired.
Interfaces: guard(request) returns a principal or HTTP 401.
Constraints: Do not log session tokens.
Requirements: REQ-AUTH-001
ADRs: ADR-0001
Depends-On: DES-AUTH-002

Put these entries in their respective requirements.md / design.md; declare every dependency as another component. A component that genuinely has no architecturally significant decision may write ADRs: none — <reason> (a concrete, non-placeholder reason) instead of a real ADR reference; a bare none, an empty field, or a placeholder reason (TODO/TBD/N/A/未定) still fails validation, now with DES_ADR_EXEMPTION_REASON when a "none" marker is present without a usable reason. Each requirement has one controlled statement. Accepted priorities are must (default), should, may. Requirement types are functional (default) and non-functional. Formal: is optional strict single-line JSON. Supported kinds are conditional, numeric (integer comparison), temporal (withinMs plus optional nonnegative afterMs), and transition (from/event/to). Numeric units ms/s/min share an exact duration dimension, while bytes/kib/mib share an exact size dimension. Other units and incompatible dimensions remain separate. It models only the declared fields. A non-functional requirement may also declare Performance: {"counter":"visitedNodes","max":100,"testId":"TEST-AUTH-002"}; the named passing test must report that integer operation counter. IDs use uppercase REQ-, DES-, CODE-, TEST-, a feature prefix, and ≥3 digits. ADRs use ADR- plus ≥4 digits. IDs must be globally unique.

Six EARS patterns: “The system shall …”; “When …, the system shall …”; “While …, …”; “If …, then …”; “Where …, …”; combined distinct Where/While/When clauses. Japanese controlled forms are documented in README-ja.md. These are syntax checks, not natural-language understanding; arbitrary prose is deliberately rejected.

Source/test trace annotations are read from language comments. JS/TS uses parser-aware comment locations; Haskell supports -- and {- ... -}, Lua supports -- and --[[ ... ]], and Visual Basic supports apostrophe comments including ''' XML documentation. These scanners exclude string literals; other languages require their supported line or block comments. Python annotations must use consecutive # comments; annotation-like text in docstrings is ignored with TRACE_ANNOTATION_IN_PYTHON_DOCSTRING guidance:

/** @id CODE-AUTH-001
 * @implements REQ-AUTH-001
 * @design DES-AUTH-001
 */
export function guard() { /* actual implementation */ }

/** @id TEST-AUTH-001
 * @verifies REQ-AUTH-001
 */
// Real behavior test follows.

One block comment per entity; comma/space-separated targets. @design is optional. This doc comment and native test-report ID matching are two independent requirements that must both be satisfied for tdd red/tdd green to succeed. The @id TEST-*/@verifies REQ-* comment only makes the test discoverable as a kind: 'test' trace-graph node, so the CLI can resolve its requirement link. Separately, the configured adapter (or tddReport) must match that same ID inside the executed native test report, using its own adapter-specific mechanism — see the adapter reference table below. A test with only the doc comment but a report the adapter cannot match to that ID fails Red/Green (the report never contains a recognized TEST-* entry); a test whose report matches but lacks the doc comment fails earlier with Annotated test ID not found: <id> (not present in the trace graph). Both failure modes look similar but have different causes — check the doc comment first, then the adapter's matching rule below. In PHP, use plain /* ... */ blocks rather than /** ... */ PHPDoc: PHPDoc reserves @implements for generic type declarations, so PHPStan/Psalm report phpDoc.parseError on requirement-ID lists inside doc comments. musubix5 reads either form. Mandatory implementation coverage may be direct or through a linked design; tests must directly verify a requirement. Links alone are not semantic proof. Each feature's trace.json holds the complete repository snapshot, including cross-feature edges and input SHA-256 fingerprints; copies intentionally agree. The cache is preferred when present; feature snapshots support cache-free checks. Rebuild when inputs change; stale impact queries are rejected.

Constitution and configuration

---
version: 1.0.0
---
## PRINC-001: Evidence first
### RULE-001: No missing trace coverage
Metric: trace.errors
Limit: 0

Supported metrics are requirements.errors, design.errors, trace.errors, graph.violations, formal.errors, formal.modeledFraction, tests.annotatedIds, tests.executedIds, commands.failures and commands.skipped. Every rule declares a nonnegative numeric upper bound. constitution validate checks the definition; only gate measures it. Unavailable evidence is skipped, never a measured zero.

Example .musubix/config.json (adapt command arguments to your own project):

{
  "schemaVersion": 1,
  "language": "auto",
  "qualityProfile": "custom",
  "commands": [
    { "name": "typecheck", "command": "npm", "args": ["run", "typecheck"], "required": true, "timeoutMs": 120000 },
    {
      "name": "test",
      "command": "npm",
      "args": ["test", "--"],
      "adapter": "vitest",
      "required": true,
      "timeoutMs": 120000
    }
  ],
  "requiredChecks": ["requirements", "design", "constitution", "trace", "graph", "commands"],
  "thresholds": { "design": 1, "implementation": 1, "tests": 1 },
  "formal": { "solver": "none", "minModeledFraction": 0, "timeoutMs": 12000 },
  "mutation": { "mode": "compatible" },
  "tdd": { "redPreflightCommands": [] },
  "approval": { "mode": "required" },
  "workflow": {
    "mode": "compatible",
    "maxAgeSeconds": 3600,
    "maxFutureSkewSeconds": 60,
    "maxEventSkewMs": 1000,
    "maxTranscriptBytes": 250000000,
    "maxTranscriptLineBytes": 2000000
  },
  "attestation": {
    "mode": "local",
    "maxAgeSeconds": 3600,
    "maxFutureSkewSeconds": 60,
    "trustedPublicKeys": [],
    "githubOidc": { "mode": "off" }
  },
  "codeGraph": { "mode": "compatible" },
  "architecture": {
    "forbidCycles": true,
    "rules": [
      { "name": "domain-isolation", "from": "src/domain/**", "disallow": ["src/ui/**", "npm:express"] }
    ]
  }
}

Config is validated strictly; misspelled keys, invalid bounds and duplicate commands fail closed. Globs support *, **, ?; external imports use npm:. A command may declare an optional cwd (a project-root-relative directory) so it runs from a service subdirectory instead of the project root — useful for a polyglot monorepo where a language's tooling expects to run from its own package/module directory. config lint reports CONFIG_CWD_INVALID for a cwd that escapes the project root or does not exist, and checks that command's repository-relative path arguments (CONFIG_ORPHANED_PATH) against its own cwd instead of the project root. Evidence and report paths (tddReport/testReport/mutationReport, .musubix/config.json itself) are always resolved from the project root regardless of cwd; only the spawned process's own working directory changes. qualityProfile is custom by default. minimal preserves the core SDD gate, recommended also requires strict Code Graph, TDD and structured test identities, and release requires the complete formal, mutation, workflow, change, performance and CI-attestation checks. Stronger profiles reject missing or weakened settings rather than silently filling in evidence. approval.mode is required in newly initialized projects and requires current requirements, design, and release approvals. Existing schema-v1 configs that omit approval load in compatible mode. Approval files store the stage, approver, approvedAt, per-artifact SHA-256 values, and a deterministic manifest SHA-256. Run approval prepare before review and pass that exact hash to approval record; an intervening change is rejected and later changes become stale. Release recording recomputes the gate and requires every required non-approval check to pass rather than trusting cached quality evidence. The approver string is explicit local evidence, not authenticated identity; repositories that require independent identity must also use protected review, CODEOWNERS, or CI/OIDC controls. Local approval evidence records explicit intent but does not cryptographically authenticate the approver; protect release authorization with repository review, CODEOWNERS/branch protection, or CI/OIDC attestation. Candidate release approval additionally requires the closed GitHub Actions matrix in .github/workflows/candidate-gate.yml. Prepare its bound inputs with musubix5 candidate-gate context, dispatch the workflow for the exact candidate, download all five opaque artifacts, ingest them with musubix5 candidate-gate ingest <artifact...>, and verify the set with musubix5 candidate-gate validate. Ingestion rejects unsigned, stale, wrong-candidate, same-batch duplicate-job, or reused-run artifacts; validation rejects any accepted record whose gate reported a tracked-tree change. Dispatch with a branch or tag ref whose tip is exactly the candidate commit; the verified workflow_sha claim is required to match that commit. Moving the ref after candidate selection requires a new candidate or restoring an authorized immutable ref before rerunning the workflow. Use tdd.redPreflightCommands to reference plain configured formatter commands; they must pass before Red captures the authoritative test fingerprint. Conventional .venv and venv Python environments containing a regular pyvenv.cfg, plus generated __pycache__/ directories, are excluded from source snapshots and Code Graph indexing. Standalone .pyc/.pyo files remain tracked because Python can execute source-less bytecode modules. Gradle .gradle/, Dart .dart_tool/, SwiftPM .build/, Zig .zig-cache//zig-out/, and .NET .dotnet/ CLI homes are excluded only when their parent contains the corresponding project manifest. Arbitrary same-named source directories remain tracked. codeGraph.mode defaults to compatible, where unresolved computed import()/require() calls remain warnings. Set it to strict to make those diagnostics gate-blocking errors. A trusted strict policy baseline prevents downgrading the project back to compatible mode. Coverage bounds are fractions [0,1] of mandatory requirements. Bare trace check --strict always requires full coverage; the aggregate gate uses config thresholds. The reported value is link coverage, not proof; with zero mandatory requirements it is null (not applicable). Add test-identities to requiredChecks to require every annotated TEST-* ID to be reported passed by a fresh structured report from a successful configured command. Add formal to enforce the configured solver and minimum modeled fraction. Every requirement containing explicit Formal: JSON automatically requires model-correspondence: its current formal constraint and generated trace must lead to at least one authoritative TEST-* that passed in a fresh structured command report. Missing, changed, unlinked, or stale evidence fails closed. .musubix/evidence/model-correspondence.json is only produced by evidence refresh; running model-correspondence validate before that file exists fails with MODEL_CORRESPONDENCE_MISSING, whose message and the command's own --help output both name evidence refresh as the fix. Add tdd to require complete Red-Green cycles. Red must be an observed nonzero test result; Green/Refactor must pass with the same configured command and unchanged test file. Test names/output must contain their TEST-* ID. language records project preference; skills follow input language. Machine diagnostic codes are stable English; human status labels include Japanese.

.musubix/policy-baseline.json records minimum required checks, coverage, architecture, formal policy, mutation and approval modes, workflow strict/session/freshness settings, CI-required attestation and strict OIDC identity/key binding, and required command names. A baseline that requires TDD Red preflights must also include their normalized commands definitions, which prevents replacing a trusted formatter while retaining its name. Weakening is rejected; changing the baseline in gate --changed requires independent approval. Protect the baseline with review/CODEOWNERS.

Only run trusted configuration: gates execute its commands with inherited environment, no shell interpretation and bounded time/output. Required command failure or skip blocks readiness regardless of requiredChecks.commands. A structured test command also fails if it reports no executed tests or any skipped, failed, or errored test, even when its process exits zero; this prevents integration suites from silently passing without their dependencies. Optional command failures are nonblocking unless a constitution rule rejects the measured count. No configured commands is skipped, not passed. Adapter test-ID declaration reference (each mechanism is distinct; see the dual-requirement note above for how this relates to the @id/@verifies doc comment):

| Adapter | ID-declaration mechanism | Worked example | | --- | --- | --- | | vitest / jest | ID as a substring anywhere in the test title | it('TEST-APP-001 rejects empty input', () => { ... }) | | pytest | ID in the underscore-form test function name | def test_TEST_APP_001(): ... | | go-test | ID as the trailing suffix of the test/subtest name | func TestTEST_APP_001(t *testing.T) { ... } | | cargo | ID as the trailing suffix of a Rust test identifier | fn test_app_001() { ... } | | junit | Exact @Tag("TEST-APP-001") plus an ID-bearing method name or @DisplayName | @Tag("TEST-APP-001") @Test void test() { ... } | | dotnet (xUnit) | ID inside [Fact(DisplayName = "...")] | [Fact(DisplayName = "TEST-APP-001 rejects empty input")] |

junit is the only adapter that requires a separate tag annotation in addition to an ID-bearing name/@DisplayName; every other adapter matches the ID directly from the test's own name/title string.

TDD commands require either command-specific tddArgs plus a tddReport, or a built-in vitest, jest, pytest, go-test, cargo, junit, or dotnet adapter. The junit adapter drives the Java JUnit Platform Console launcher, not arbitrary JUnit-XML producers; runners such as PHPUnit that only emit JUnit XML need explicit tddArgs/tddReport (or testReport) configuration instead. A custom musubix-json report is a single-line-safe JSON document {"schemaVersion":1,"tests":[{"id":"TEST-APP-001","status":"passed"}]} where status is passed, failed, skipped or error, and an optional "operations":{"counter":12} map carries deterministic performance counters. Explicit custom configuration takes precedence. Adapters derive targeted arguments and normalize native JSON/JSONL/XML into musubix-json. Vitest/Jest reports may contain unrelated skipped tests; targeted TDD selects only the requested ID. pytest requires the JSON-report plugin and underscore-form test names such as test_TEST_APP_001. Go uses a TEST-* subtest name, Cargo uses a Rust identifier such as test_app_001. JUnit methods should carry an exact @Tag("TEST-APP-001") and an ID-bearing method name or @DisplayName; the normalizer reads both testcase attributes and JUnit Platform display-name output. Surefire/Failsafe testcase elements are parsed whether they are self-closing or carry <system-out>/<system-err> children, so framework logging such as the Spring Boot banner does not hide passing identities. xUnit tests use [Fact(DisplayName = "TEST-APP-001 ...")] so TRX preserves the identity. Before each phase, musubix5 deletes the previous report, creates any required report parent directory, and requires a fresh musubix-json document containing exactly the selected test. Its status must be failed during Red and passed during Green/Refactor; skipped, error, missing and malformed reports fail. A non-test project input must change before Green. Identical phase output reused by different tests is rejected. Every phase is also appended to a SHA-256-linked immutable record chain. TDD and change checkpoints additionally share a persisted monotonic order ledger, which is authoritative for Red/Green boundaries; wall-clock timestamps are informational. Legacy chronology without order evidence fails with an explicit migration diagnostic. Missing, reordered, altered or orphaned records invalidate the evidence. Superseded cycles are never replaced by a newer recording: if any cycle lacks test-scoped provenance or a valid Red/Green, move .musubix/evidence/tdd.json aside and re-record every cycle from a clean Red baseline. There is deliberately no partial prune command, and hand-editing the evidence is unsupported.

Deterministic mutant identities come from musubix5 mutation identity <REQ-ID> <TEST-ID> <sourcePath> <operator> <line> <column>, which prints the exact MUT-* value a schema-v1 mutation report must declare. mutation validate reads .musubix/evidence/mutation.json; a configured mutationReport is converted into that file by the gate, so validating before a gate run reports absent rather than passing evidence.

CI executes isolated native contracts for Vitest, Jest, pytest with pytest-json-report, Go test, Cargo test, and the pinned JUnit Platform Console. The .NET adapter consumes standard TRX and is additionally validated by unit contracts and the C# application experiment. Each fixture contains an unrelated failing test, proving that the generated selector executes only the requested identity and that the real native report normalizes correctly. Jest is development-only; the Python, Go/Rust, and Java/JUnit tooling is provisioned only in CI and is not shipped as a package runtime dependency.

Change checkpoints fingerprint only implementation files linked to each changed requirement, plus their Code Graph dependencies. An unrelated source change cannot satisfy the implementation phase. The automatic change-completeness gate checks each CHANGE-ID for classified functional/non-functional requirements, measurable Acceptance criteria, concrete design responsibilities/interfaces/ constraints, an existing ADR, linked code, authoritative annotated tests, bounded TDD and trace edges. Each CHANGE document must contain a Requirements: line enumerating exactly the chronology's normative requirement IDs.

Structured test results may add "operations":{"visitedNodes":42}. A declared deterministic performance budget automatically requires the performance gate; elapsed time alone cannot satisfy it. For every observation, performance.json records a gate-generated run identity and SHA-256-linked provenance covering the configured command name, executable and rendered arguments, report path/source, fresh report bytes, test ID/status, counter/value, and process status/exit code. Validation re-reads persisted file, directory, and captured stdout reports and rejects missing or altered reports, record mutation, configuration drift, duplicate counter sources, non-passing tests, and results not produced by a successful configured command. The signed performance head hashes stable semantic fields while the JSON retains run/execution IDs, timestamps, report hashes, and chained provenance, so an equivalent gate can be rerun after signing without invalidating the signature. This provenance also gates CHANGE completeness and status freshness. Native runner reports do not expose application operation counters, so projects with such budgets must also configure an instrumented musubix-json report. Native adapters and custom reports can coexist; only the instrumented report that actually emits the named operation counter can prove the performance budget.

Mutation evidence uses a configured command with "mutationReport":{"format":"musubix-mutation-json","path":"..."}. Each fresh schema-v1 mutant record carries a deterministic MUT-<hash> identity (derivable with the mutationIdentity helper exported from musubix5/analysis), must-functional requirement ID, authoritative test ID, source/test paths and SHA-256 fingerprints, operator, one-based line/column, and killed|survived|skipped|error status. The gate adds command, rendered-argument, report, process, and exit provenance to mutation.json. Supplied evidence must cover every must functional requirement with a current linked killed mutant. Duplicate/conflicting, non-killed, stale, unlinked, altered-report, and configuration-drift evidence is rejected. mutation.mode defaults to compatible (absence is allowed); set it to strict and protect it plus the mutation command in the policy baseline for release. No mutation engine dependency is bundled. For Python, mutation doctor recommends removing existing __pycache__ directories before each run, then using python -B -m mutmut and python -B -m pytest to avoid new bytecode. Mutation and model-correspondence semantic heads are included in attestations and their underlying provenance is revalidated.

Quality evidence records required flags, actual exits/output, metrics, timestamps and input fingerprints. Changed-run paths, HEAD and impacts survive a later full gate. workflow-record stores a self-reported Skill/phase/status and optional command SHA-256 without storing command text. workflow-verify imports only Skill invocation metadata from a Copilot JSONL log and binds every completed declaration one-to-one, in order, to a distinct completed successful tool call. Use workflow-sanitize first when the source transcript contains messages, non-Skill tool arguments, or output that should not enter review evidence. Each Skill invocation must therefore record exactly one final workflow outcome; multi-phase chronology belongs in change-record, not duplicate workflow events. Incomplete, failed, reused, out-of-order and stale bindings fail. Set "workflow":{"mode":"strict"} or pass --strict to additionally require valid JSON on every nonempty line, valid event timestamps, consistent one-to-one tool start/completion lifecycles, and exactly one successful final terminal state. Supported terminal formats are result with exitCode: 0, or the current Copilot CLI lifecycle format with one session UUID and a final session.shutdown whose data.shutdownType is routine. The shutdown format also accepts one or more intermediate routine shutdowns when each is immediately followed by session.resume; workflow-sanitize retains those lifecycle boundaries. Mixed terminal formats, unmatched shutdown/resume transitions, multiple session identities, abnormal shutdowns, and trailing events fail closed. Compatible mode alone accepts more than one transcript path; supplied files are concatenated in ascending order of each file's earliest event timestamp (not command-line order), while each file's own internal event order is preserved untouched — this lets declarations whose invocation occurred in an earlier Copilot CLI session be reconciled by additionally supplying that session's transcript file. A toolCallId that appears as a tool start in more than one supplied file is rejected. Copilot CLI writes each session's JSONL transcript to ~/.copilot/session-state/<sessionId>/events.jsonl; this path is an internal detail of the installed Copilot CLI version, not a musubix5-owned contract, so confirm it against your installed version rather than assuming it is stable across releases. The terminal sessionId, exit code, event count, terminal timestamp, raw source hash and canonical transcript hash are persisted. workflow.expectedSessionId or --session-id rejects substitution with a different caller-declared session. Strict verification also bounds terminal transcript age and future clock skew with workflow.maxAgeSeconds and workflow.maxFutureSkewSeconds. Unrelated concurrent events—and even timestamps produced by different execution clocks—may be non-monotonic, so strict mode uses JSONL source order for causal tool/result lifecycles rather than imposing a timestamp sort. Pair/terminal clock skew is enforced only when maxEventSkewMs is explicitly supplied; terminal age and future-skew policies remain independently enforced. Verification remains streaming and resource-bounded: transcripts default to 100,000,000 bytes, while workflow.maxTranscriptBytes can explicitly raise the limit up to 1,000,000,000 bytes. Individual JSONL records default to 1,000,000 bytes and can be bounded up to 10,000,000 with workflow.maxTranscriptLineBytes. Protect both chosen bounds in the policy baseline so they cannot be widened silently. If project inputs change while a gate is running, input-stability reports each added, modified, or deleted path with before/after SHA-256 values. Standard Cargo/Maven target/, manifest-scoped .NET bin/ and obj/, and project-local .nuget/packages/ output are excluded, but source-like generated inputs remain fail-closed. Write command-generated reports under .musubix/evidence/native/ rather than the tracked source tree, otherwise a command that writes its own report during the gate invalidates input stability. Built-in adapters own their targeting and report arguments. A legacy leading Cargo/Go test subcommand is merged safely; conflicting report flags such as --json-report are rejected. Changes during a gate fail input stability; later source/config changes make status stale. Attestations older than maxAgeSeconds, or issued farther in the future than maxFutureSkewSeconds, fail. Local mode explicitly reports unsigned evidence.

ci-required supports two deliberately distinct trust models:

• Static trusted-key mode (githubOidc.mode: "off"): keyId must select a configured Ed25519 public key. The signature covers repository, Git HEAD, CI provider/run ID, evidence heads, and the non-generated workspace snapshot.
• GitHub OIDC strict mode: configure githubOidc.mode: "strict" and a custom audience base. The verifier discovers GitHub's issuer metadata and JWKS, verifies the RS256 JWT, and checks issuer, bound audience, exp/nbf/iat, repository, commit sha, and run_id, plus optional workflow and ref. keyBinding: "public-key" authorizes an attestation-carried ephemeral Ed25519 public key by its SPKI SHA-256 in the custom audience. keyBinding: "key-id" instead adds OIDC authorization to a statically trusted key ID. If metadata/JWKS cannot be fetched, strict verification fails closed.

Evidence heads also bind stable non-attestation quality verdicts and formal solver status, total requirements, modeled count/fraction, consistency, and artifact identity. Excluding the attestation check from the quality head avoids a circular signature dependency. A missing ci-required attestation is reported as a failed/missing check, never as skipped local evidence.

Attestation evidence-head composition

collectEvidenceHeads (packages/analysis/src/attestation.ts) canonicalizes up to ten independent evidence entries into stable per-entry digests. Each entry's direct input/projection is:

• tdd: the last entry's recordSha256 from .musubix/evidence/tdd.json's hash chain — a chain-tip digest, not a projection over every recorded phase field.
• workflow: workflowEvidenceHead's projection of .musubix/evidence/workflow.json's verification block only (eventsSha256, sourceSha256, transcriptSha256, mode, sessionId, exitCode, terminalAt, eventCount, sourceBytes, maxTranscriptBytes, maximumLineBytes, maxTranscriptLineBytes, and invocations (each entry's skill/toolCallId/invokedAt/ completedAt/status, unsorted/order-sensitive as stored), or just eventsSha256/sourceSha256 when mode, transcriptSha256, and sessionId are all absent); the raw events log itself is excluded.
• changes: a canonical digest of .musubix/evidence/changes.json's changes array directly — not the .musubix/changes/*.md documents themselves, which are a separate upstream input to that evidence.
• order: the last entry's recordSha256 from .musubix/evidence/order.json's records — a chain-tip digest, not a projection over every recorded declaration.
• formal: retains only fingerprints, totalRequirements, modeledRequirements, modeledFraction, and the solver's artifact/status/result.consistency from .musubix/evidence/formal.json, excluding generatedAt and every other result field such as solver duration, diagnostics, literals, and constraints.
• performance: performanceEvidenceHead's projection of .musubix/evidence/performance.json, retaining per execution commandName/commandSha256/reportPath/sourceKind/processStatus/ exitCode/a canonically-sorted tests array (each test entry kept in full), and per observation requirementId/testId/counter/observed/ maximum/status/an optional provenance object retaining exactly commandName/commandSha256/reportPath/sourceKind/testId/ testStatus/counter/value/processStatus/exitCode; both the executions and observations arrays are canonicalized order-independently.
• mutation: mutationEvidenceHead's equivalent projection of .musubix/evidence/mutation.json, retaining per execution commandName/commandSha256/reportPath/processStatus/exitCode/a canonically-sorted mutants array (each mutant's full record); both the executions and nested mutants arrays are canonicalized order-independently.
• modelCorrespondence: modelCorrespondenceEvidenceHead's projection of .musubix/evidence/model-correspondence.json, retaining schemaVersion, formalEvidenceSha256, traceEvidenceSha256, and a canonically-sorted entries array (each retaining requirementId/requirementPath/ formalSha256/modelSha256/traceSha256/a canonically-sorted tests array retaining exactly testId/testPath/testSha256/commandName/ commandSha256/reportPath, excluding reportSha256/provenanceSha256); any other stored run metadata is excluded.
• quality: retains schemaVersion, mode, a derived pass/fail status, and each non-attestation check's name/required/status/a narrow diagnostics projection (code/severity/path/line), plus metrics with the attestation.errors entry excluded; also excludes generatedAt, durationMs, and stdout/stderr.
• workspace: not an evidence file at all — a content digest over the non-evidence repository file set returned by files(root), filtered by evidenceInputPaths; .musubix/evidence/** itself is excluded from this walk so writing evidence never perturbs the workspace snapshot it is bound into.

See collectEvidenceHeads and the per-entry head functions it delegates to (workflowEvidenceHead, performanceEvidenceHead, mutationEvidenceHead, modelCorrespondenceEvidenceHead) for the authoritative implementation; this list is a summary, not a substitute for reading the source when precision matters.

Example strict configuration:

{
  "attestation": {
    "mode": "ci-required",
    "repository": "owner/repository",
    "maxAgeSeconds": 600,
    "maxFutureSkewSeconds": 30,
    "trustedPublicKeys": [],
    "githubOidc": {
      "mode": "strict",
      "audience": "https://example.invalid/musubix5",
      "keyBinding": "public-key",
      "workflow": "release.yml",
      "ref": "refs/heads/main"
    }
  }
}

For normal CLI use, generate an Ed25519 key outside musubix5 and pass only its public PEM to attestation oidc-audience, request the GitHub Actions OIDC token with that exact audience, then pass the public PEM and JWT files to attestation payload and sign the emitted payload externally. The musubix5 CLI never accepts, reads, or stores a private key. This repository's release-only automation separately generates an ephemeral private key under the ignored .test-work directory, uses it for signing, and deletes it before invoking CLI verification. The short-lived JWT is included in the signed attestation and is intentionally checked for current expiration, so verification must occur within its validity window. This establishes that GitHub's OIDC identity authorized the signing key and stated claims; it does not prove arbitrary runner behavior or the semantic correctness of the workflow. The workflow evidence head separately binds transcript/session fields into the Ed25519 signature.

Formal methods, codegraph and retrieval limitations

• Deterministic formal checking works without external solvers. Controlled unconditional English/Japanese obligations retain the Boolean abstraction; strict Formal: JSON additionally models branch-scoped conditional truth, exact integer bounds with documented compa