docs: write the threat model

[carlok]

The last item from the plan, and the piece §3 called the publishable asset: the document another maintainer reads before deciding whether mechanical admission could work for them.

Structure

• What the receiver guarantees, each backed by a check that exists: kernel replay, the axiom allowlist, corpus regression, Mathlib duplicate comparison, bounded triviality probes (both directions for conjectures), deprecation rejection, downstream import.
• What it does not: interestingness, honest prose, true provenance, or that a name matches its statement.
• Six failure modes found in practice, each with its fix: import-time code execution (fix: reject build- and import-time code, and make submissions add-only #216), meaning drift under a stable name (fix: reject build- and import-time code, and make submissions add-only #216), deprecation debt (feat: reject deprecated APIs in submissions, report them in upgrades #239), a conjecture probe that silently never ran (fix: probe conjectures the claim does not list #241), orphaned processes exhausting a contributor's host (fix: kill a timed-out command's whole process group, and time the probes #201), and a stale-branch rejection that blamed the submitter for our merges (feat: name a stale branch as stale instead of blaming it for main's changes #254).
• Trust boundaries: trusted code from the base checkout, candidate code only in a --network none --read-only --cap-drop ALL container, no pull_request_target, branch names granting nothing, narrow auto-merge, docs proposals carrying no code.
• What remains unguarded, stated plainly: prose, maintenance PRs bypassing the receiver, upstream dependencies, and one producer's taste.

The closing point is the one worth making publicly: admission can be mechanical only if the checks cover what actually goes wrong, and that list is learned by running the thing in the open and writing down each failure.

Keeping it honest

A contract test asserts that every diagnostic code and sandbox flag the document advertises also appears in frontier_validate.py and validate-submission.yml, so the document cannot drift away from the code. Writing that test immediately caught the deprecation section describing the rule without naming DEPRECATED_API.

README.md links it. Full suite: 152 tests, 6 skipped.

🤖 Generated with Claude Code