formal: add local prefix-cache contract registry

[dusterbloom]

Dependency and review order

Depends on #563. Do not merge this draft before #563.

This is PR 2 of the staged replacement for #561. GitHub currently compares
this fork branch with upstream main, so its Files Changed tab temporarily
includes PR 1 as well. The PR 2 commit itself is
6d1c428:
17 files and 1,444 added lines.

After #563 merges, this branch will be rebased onto the updated upstream
main and force-pushed. The Files Changed tab will then shrink to this PR's
formal-registry work only.

Why

The original #561 mixed a production cache fix, a reusable formal-verification
platform, five targets, hosted workflows, image policy, and later rollout
decisions into one large review. This draft keeps the second unit local and
deliberately narrow: establish the registry and prove it works against the two
prefix-cache properties introduced by #563 before asking maintainers to trust
or activate it in CI.

What changed

• adds a versioned TOML manifest and contract registry;
• adds a deterministic planner with validate, plan, and emit commands;
• adds local container runners and a mutation-sensitivity check;
• pins verifier and repair image references by immutable digest;
• adds two initial targets:
  • prefix-cache-inline;
  • prefix-cache-abort-hole;
• documents the contract schema, local workflow, evidence boundary, and the
  five candidate areas that remain outside this first wave;
• adds unit tests and fixtures for registry validation and selection.

Scope boundary

This draft is local tooling plus two contracts. It does not:

• add or modify a hosted formal-verification workflow;
• change branch protection, required checks, or CODEOWNERS;
• use credentials or invoke AI;
• add speculative-decoding or full KV-cache lifecycle targets;
• make the registry's policy = "required" metadata enforce anything.

The repair-image digest is compatibility metadata only in this draft. No
repair or AI path is invoked. Hosted CI integration, image trust/provenance,
permissions, and any required-check policy need a separate maintainer/security
review and a later PR.

Validation

• python3 scripts/formal_plan.py validate;
• planning selects exactly the two registered targets with no coverage gaps;
• manifest emission succeeds;
• all six planner/registry unit tests pass;
• bash -n scripts/formal.sh scripts/formal_mutation_test.sh;
• uv run --frozen --extra dev ruff check .;
• git diff --check;
• clean-clone ./scripts/formal.sh --all: both contracts verified with the
  pinned verifier image;
• clean-clone mutation campaign: control verifies and the abort-hole mutation
  produces the expected counterexample.

Proposed release sequence

1. Review and merge fix(prefix-cache): reuse slots after aborted snapshots #563 as the independently useful correctness fix.
2. Rebase this draft onto upstream main and confirm its reduced diff.
3. Review the local registry, pinned image references, and the two contracts.
4. Merge this PR without activating hosted enforcement.
5. Propose CI integration and policy activation separately, with explicit
   maintainer/security approval and evidence from the local phase.

This sequence gives maintainers a useful production fix first, then a
revertible local verification layer, while keeping CI trust and enforcement as
an explicit later decision.