MTL capstone: writeup + one-command replication kit

[madmax983]

What this adds

Before: MTL's headline claims — the compression ratios and the admit-free proof stack — lived scattered across the README, seven design docs, and a handful of BASELINE*.md files, and a third party could not reproduce any of it from a clean checkout without reverse-engineering the repo. There was no paper and no replication kit.

After: a single writeup states what MTL claims and why — with the honest negatives as first-class results — and a one-command kit regenerates every headline number and rebuilds all five proof gates from a clean clone.

The paper — docs/paper/mtl.md (~6,500 words)

Answers the day-one question: "Can a language co-designed for model tokenizers and formal verification reduce total inference cost without reducing agent reliability?" The measured answer, stated plainly:

• Reliability preserved — 100% pass@5 held-out writability, no measurable read-tax.
• Total cost NOT reduced in the cold single-session regime — the break-even session length N* is unreachable within N≤16; the cold preamble dominates.
• Compression is niche, not a headline — in-sample 3.72–3.92× collapsed to 1.67× on the first blind held-out set; the ≥3× Abrash gate failed out of sample and was retired (PR docs: restate compression claims to held-out truth; retire ≥3× Abrash gate #95). The co-evolution finding (dev corpora tuned together with the primitives) is written up as a reusable methodological warning for benchmarking LLM DSLs.
• What survives — per-solution economics (held-out CSPM 2.124×) and a machine-checked core: five Verus roots (76+118+101+116+145 = 556 obligations, 0 errors), 322 workspace tests, a two-stub trusted boundary, and runtime-enforced capability confinement.

Section map: design method (measurement-driven primitive admission, TAVDD, adversarial-review absorption) · the language · verification · the honest results arc · decision record · related work · limitations (all of them) · reproducibility.

The replication kit — REPRODUCE.md + kit/

• kit/replicate.sh — the full non-Verus pipeline; regenerates every ratio and asserts it byte-identically.
• kit/proof-gates.sh — reviewer-runnable; builds/locates the pinned Verus, runs the 5 gates, exits non-zero if any hard gate misses its count. Usable by someone who does not trust the repo's CI.
• kit/build-verus.sh — the sanctioned from-source Verus + Z3 build (the GitHub release zip is 403-blocked in this environment).
• A 16-row claim → command map: every published number → the exact copy-pasteable command → its expected output line.
• kit/EVIDENCE.md — captured transcripts of both observed reproductions.

Reproduced in-container from a clean checkout

Every number was independently regenerated here, not merely asserted:

• Non-Verus pipeline — 14/14 green from a strict git clone fresh checkout: 322 tests / 0 failed, T_v0 3.72×, tier-2 3.87×/3.92×, tier-3 1.86×/1.85×, sealed 14/14, differential oracle 148/148, factorial HALT: 120; all baselines byte-identical.
• Verus gates — built Verus 0.2026.07.05.49b8806 + Z3 4.12.5 from source (≈18 min, 4 cores) and reproduced all five exactly: mtl_core 76, p5_universality 118, p4_verus 101, checker_verus 116, arena_verus 145, 0 errors; --no-cheating flags exactly the two Clone stubs and nothing else.

What is NOT push-button

The live-model agent trials (CSPM, pass@5, read-tax, session economics) need model access; the kit reproduces the scorer + ground truth + recorded per-attempt JSON, not the raw model outputs. This boundary is stated plainly in REPRODUCE.md.

Corrections to the record

Writing the paper surfaced five stale or internally contradictory in-repo numbers; the paper uses the current merged value for each and consolidates them in §5.6: P4 42→101, P2 stubbed→discharged (76/0), tier-3 1.90→1.86× (README vs artifact), checker 27/79→27/87, workspace tests 275→322. Fixing the stale README/spec prose itself is tracked separately in #78.

Closes #71.

---

Generated by Claude Code