lypning

lypning — the Coding Harness Interpreter Optimizer

lypning optimizes the interpreter layer underneath a coding harness: it runs a Python program on the cheapest interpreter that can actually run it. The architecture is a mixture of Pythons — a spectrum of from-scratch Python subsets written in Rust, built from one crate at two sizes (lypning and lypning-l, budgeted 9 and 32 device blocks on x86_64-unknown-linux-musl — gate.VARIANT_BLOCK_BUDGET is keyed by target, because a block count is a property of code AND toolchain AND target), and the real CPython for everything they refuse — with a classifier that asks the Rust core’s own parser which one, per program. The subset is sized not to Python but to the one-liners a coding agent actually types, the only reason this is affordable. And that is a moving target, which is the point of the name: the corpus is captured from live sessions, the loop re-derives the tables from it, and the whole thing is built to be forked and re-tuned to your harness, your agent, your programs — models drift, and this optimizer drifts with them (docs/FORKING.md).

Every tier refuses the same way: exit 90, one line on stderr, nothing on stdout. That is what makes the three interchangeable, and what makes a wrong route cost one wasted process spawn instead of a wrong answer. docs/PAPER.md is the write-up, the baselines that beat us included.

The other direction — teaching a model to write the subset, so fewer programs need refusing at all — is measured in §7b: a rank-16 LoRA moved the held-out pass rate +4.46pp [+1.52, +7.86] against a same-stack control, and the pre-registered rule still returns no win, because the effect was broad rather than concentrated. The rule was fixed before the adapter existed and the result is written back against it.

How a program reaches an interpreter

  python3 -c '…'   the shim on PATH — or the PreToolUse hook — hands the program to
       │           `lypning run`; the dispatcher IS the Rust binary, not a wrapper
       ▼           route: one parse of lypning's own front end grades every variant
  ┌─▶ lypning      the Rust core — runs IN-PROCESS, no spawn; on refusal, exit 90:
  │      │         one line on stderr, none on stdout, and the chain moves on
  ├─▶ lypning-l    the same crate, larger — FORKED, stderr piped, so its 90 is caught
  └─▶ cpython      the reference — EXEC'D: replaces the process, no way back, none needed
         ▼         the program's own stdout, the program's own exit code

1. Measurement

One instrument per question (§5, §6), and every instrument prints the corpus size it loaded: quote that number with its date, never a remembered one (CLAUDE.md invariant 3).

Coverage: lypning conformance --mixture both, 2026-09-26, commit f6b0728, corpus 14,816 loaded and 10,173 graded. How much of the Python that coding agents actually ran each engine answers by itself, compared with CPython 3.14.5 on a macOS arm64 build. The other 4,643 programs were skipped by the tool’s own rules: absolute paths outside the sandbox, programs that drive a lypning test run, external mutation, or no reproducible CPython answer.

engine answers itself, as CPython does declines, passes it on answers differently share answered
lypning 4,583 5,590 0 45.1%
lypning-l 7,357 2,816 0 72.3%
mixture (the chain) 10,173 0 0 100%

A program an engine declines goes to the next one up (lypning-l, then CPython), so declining costs a spawn and never an answer. No engine answered a graded program differently from CPython, and the Python and Rust dispatchers agreed on all 10,173. The router picked the cheapest engine that answers for 94.6% of programs. What each round added, and why the rest still decline, is in docs/HILLCLIMB.md. Re-run the command before quoting a number: capture grows the corpus every session.

lypning bench, 2026-09-06 — corpus 3,688 loaded, 2,504 measured, shared subset 1,572, min of 3, arms interleaved per entry. Darwin arm64, 10 cpus, load 1.2–3.3: a shared box, so the ratios are the reading and the milliseconds are not. cpython is 3.14.5; pypy3 is 7.3.23 (Python 3.11.15), a comparison arm — measured, never routed to.

arm startup -c 'pass' shared subset per program whole corpus answers
lypning 0.151x 0.167x 0.178x 0.107x refuses 932
lypning-l 0.146x 0.161x 0.165x 0.102x refuses 537
mixture 0.143x 0.196x 0.166x 0.523x all 2,504
cpython 1.000x 1.000x 1.000x 1.000x reference
pypy3 0.907x 0.947x 0.923x 1.019x all 2,504

per program is the geometric mean of per-program ratios over the 532 programs every arm ran to exit 0; a sum over the corpus would be weighted by its slowest program. A variant that refuses is cheaper in the whole-corpus column for a reason that is not speed, which is why the number this project stands on is the dispatcher’s 0.523x with nothing unanswered — a session of 2,504 one-liners for 47.7% less wall clock than CPython, answering every one of them.

The startup cell is the one number here not to lean on: pypy3 and cpython land within about 10% of each other and the ordering is not stable, ranging 0.89x–1.01x over four min-of-15 samples on this host the same day.

Where the subset stops paying. The corpus is spawn-bound and cannot see a compute win in either direction, so one loop swept across decades locates the crossing (same run, compute-only, startup subtracted, mean of 6 after the first sample is discarded):

iterations of n = (n + i * 7) % 999983 lypning lypning-l pypy3
1,000 0.18x 0.22x 1.17x
10,000 0.38x 0.45x 0.84x
100,000 1.08x 1.30x 0.36x
1,000,000 1.35x 1.49x 0.09x
10,000,000 1.36x 1.55x 0.07x

Under ten thousand operations the Rust variants win, because almost nothing but startup and parse has happened yet; past a million a tracing JIT wins by more than an order of magnitude and they lose by 1.4–1.6x. Agent one-liners live at the left-hand end, and that is the whole bet — falsifiable by a corpus whose programs got longer. pypy3 states the same boundary in its own documentation: below roughly 0.2 s of work its JIT has no chance to pay for itself.

Full entry and methodology: docs/BENCH-LEDGER.md. Older figures are dated there too — the last full lypning bench before this one (2026-08-25) and the upstream table it was written against moved there on 2026-09-04, with their original runtime identities.

2. Installation

pip install lypning       # pure Python, zero runtime dependencies (not on PyPI as of 2026-09-04: `pip install .` from a checkout)
lypning build --rust      # → `ok` per spectrum variant, and the seconds each took, into ~/.lypning/bin
lypning status            # → each engine's path, bytes and blocks; the corpus count loaded

Nothing compiles at install time: until lypning build --rust runs, status says not built and every program routes to CPython. The crate needs cargo and nothing from crates.io (CLAUDE.md invariant 6); a build is not ok until the refusal contract holds on the binary it just produced (build.check_refusal_contract; docs/VERIFICATION.md §C2). --lib builds the C ABI (§3b), and --all builds both. The wheel shape — pip install --no-build-isolation . into a venv, assets/ read-only — is tested on purpose, never by accident (docs/VERIFICATION.md §C13).

3. Integration with a coding session

lypning install wires a skill (what the subset refuses), three hooks merged into .claude/settings.json (SessionStart refreshes the shim, PreToolUse logs python-ish Bash commands, Stop publishes the session’s sightings) and a python/python3 shim in ~/.lypning/bin into a repository, so a Claude Code session routes its python through the mixture and records what it typed; --harness opencode,openhands does the same for those hosts (docs/HARNESSES.md). --dry-run prints the plan — one line per file, the backup, the merge, a warning when ~/.lypning/bin is not on PATH — then the settings.json diff, and writes nothing; a second lypning install prints all 3 hook entries already present.

settings.json is merged, never overwritten: hook entries whose command is absent are appended; unrelated keys, hooks and their order survive; the original is copied once to settings.json.lypning-backup and never re-backed-up; a file that does not parse is reported and left alone (CLAUDE.md invariant 7; docs/VERIFICATION.md §C10). A real before/after, given a repo that already had its own audit hook:

{
  "permissions": { "allow": ["Bash(pytest:*)"] },
  "hooks": {
    "PreToolUse": [
      { "matcher": "Bash",
        "hooks": [ { "type": "command", "command": "sh .claude/hooks/my-audit.sh" } ] }
    ]
  }
}

lypning install produces:

{
  "permissions": {
    "allow": [
      "Bash(pytest:*)"
    ]
  },
  "hooks": {
    "PreToolUse": [
      {
        "matcher": "Bash",
        "hooks": [
          {
            "type": "command",
            "command": "sh .claude/hooks/my-audit.sh"
          },
          {
            "type": "command",
            "command": "sh \"$CLAUDE_PROJECT_DIR/.claude/hooks/lypning-capture.sh\""
          }
        ]
      }
    ],
    "SessionStart": [
      {
        "hooks": [
          {
            "type": "command",
            "command": "sh \"$CLAUDE_PROJECT_DIR/.claude/hooks/lypning-session-start.sh\""
          }
        ]
      }
    ],
    "Stop": [
      {
        "hooks": [
          {
            "type": "command",
            "command": "sh \"$CLAUDE_PROJECT_DIR/.claude/hooks/lypning-harvest.sh\""
          }
        ]
      }
    ]
  }
}

The existing my-audit.sh entry keeps its position; ours is appended to the same matcher group. --user installs into ~/.claude; --no-shim, --no-hooks and --no-skill each drop one piece. The shim refuses to overwrite a python3 it did not write — a venv stub, a pyenv shim, a distro symlink; --force moves it to <name>.lypning-backup. lypning uninstall (--dry-run lists what would go) is the exact inverse: it removes the skill, our hook scripts, the hook entries whose command mentions lypning, and the shims, restoring anything --force moved aside; other hooks survive.

The capture log is never deleted by uninstall. The programs in it outlive the harness that captured them, and deleting them here would be unrecoverable. uninstall says so on its last line. rm -rf ~/.lypning is the manual step.

The shim only runs if ~/.lypning/bin is first on $PATH; lypning status and lypning shim status both shout when it is shadowed, because “installed but never runs” and “not installed” have the same symptom — an empty log — and only one of them looks fixed.

3b. Embedding the runtime in a host

The other way in is to link the runtime: liblypning (lypning build --lib, then gcc $(lypning lib --cflags) h.c $(lypning lib --libs)) is lypning-l reached through the C ABI in your own thread — no fork, no exec, no pipe — and its refusal line begins lypning-l:.

lypning_result *r = lypning_run(q);
if (lypning_result_should_fall_onward(r)) run_on_python3(src);  /* your path */
else                                      use(lypning_result_stdout(r, &n));

That branch is the whole integration, and getting it right is the whole contract: a refusal is not an error. It means the program is outside the subset, that lypning ran none of it, and that CPython should answer now. A harness that reports it as a failure has turned a speedup into a bug — silently, because the program was fine. Every host has a quickstart (docs/EMBEDDING.md §4); an embedded run takes a step limit, not a timeout, and reports one as a refusal (docs/EMBEDDING.md §6; docs/VERIFICATION.md §C14).

4. Command reference

Anything that calls python3 can call lypning instead. One row per subcommand; flags are in lypning <command> --help; run and hook have a caller-defined output, every other subcommand takes --json.

command what it does --json
lypning -c PROG [args…] exec the Rust core directly — no wrapper left in the process —
lypning FILE [args…], lypning - the same, from a file or stdin —
lypning run -c PROG route, run, and fall through to the next rung on exit 90 only no
lypning route -c PROG print the engine a program would run on, and why yes
lypning build build the spectrum into ~/.lypning/bin; --lib the C ABI yes
lypning lib the flags a C or C++ host needs to link liblypning yes
lypning pool a warm CPython backstop for the chain — opt-in, LYPNING_POOL points at it yes
lypning overview the map, every contract and whether it is pinned, and each variant against its OWN budget; --deep runs every pin and the suite yes
lypning status what is built, wired and captured yes
lypning doctor the same with an opinion; exit 1 on any FAIL yes
lypning install wire capture into a coding harness (--harness claude,opencode,openhands) yes
lypning uninstall remove exactly what install added yes
lypning shim {install,uninstall,status} the python/python3 capture shim on its own yes
lypning hook EVENT harness hook entry points: event JSON on stdin, protocol JSON on stdout no
lypning conformance run the corpus against CPython and grade the answers — §5 yes
lypning fuzz generate programs from the subset and diff against CPython; exit 1 on a counterexample yes
lypning bench time startup and the whole corpus, arm by arm yes
lypning corpus-time time the whole corpus on ONE binary, and diff two runs of it yes
lypning perf time one construct at a time against CPython yes
lypning gate [BIN] measure a binary against the acceptance table; exit 1 on a failed check yes
lypning harvest turn captured invocations into corpus entries yes
lypning corpus inspect the harvested programs yes
lypning routes the value-dependent refusals a static route could not see — write-only with respect to routing (docs/VERIFICATION.md §C11) yes

Exit codes (cli.py): 0 ok; 1 the command failed (a MISMATCH, a failed gate, a fuzz counterexample, a doctor FAIL); 2 usage, including “the core is not built” and engines.EngineError; 90 an engine refusal, passed through untouched; 127 the Rust dispatcher cannot run an engine; 130 interrupted. Timeouts, by command: docs/VERIFICATION.md §15. LYPNING_DEBUG=1 restores tracebacks. A clean route prints the engine name alone, a refusal-derived one <engine>\t<kind>: <detail> (run 2026-09-04 against the binaries in §7):

$ lypning route -c 'import collections; print(collections.Counter("abca").most_common(1))'
lypning-l   module: import collections
$ lypning -c 'import re'; echo $?
lypning: unsupported: module: import re
90
variable effect
LYPNING_HOME state dir (default ~/.lypning) — binaries, log, build trees
LYPNING_LOG capture log path (default $LYPNING_HOME/invocations.jsonl)
LYPNING_BIN, LYPNING_L_BIN pin a spectrum variant’s binary (engines.env_var_for)
LYPNING_LIB override the embeddable C ABI library (lypning lib, lypning.embed)
LYPNING_POOL socket of a warm CPython pool (lypning pool serve); the chain’s CPython tier uses it, and falls back to a cold spawn if it is unreachable
LYPNING_CPYTHON override the reference CPython
LYPNING_CAPTURE=0 disable the whole capture harness
LYPNING_HARVEST=0 keep capturing, stop the Stop hook publishing
LYPNING_ROUTES=0 stop the write-only route ledger (lypning routes), in both dispatchers; LYPNING_CAPTURE=0 also covers it
LYPNING_DEBUG=1 show tracebacks

5. Conformance contract

lypning conformance                 # exit 1 on any MISMATCH or UNSAFE; MISMATCH must be 0
lypning conformance --mixture both  # …and both dispatchers: prints `dispatchers agree N/N`

Every corpus program runs on CPython and on each built arm — by default lypning, lypning-l and the mixture (conformance.DEFAULT_ARMS); library (the C ABI) and mixture-rust (the Rust dispatcher’s chain) are opt-in by --engine. Each answer is one of three:

verdict meaning failure?
MATCH stdout, exit code and the exception (if either arm raised) identical to CPython no
UNSUPPORTED exit 90 with <engine>: unsupported: <kind>: <detail> on stderr no — this is coverage, and it is the build order
MISMATCH anything else yes, always

MISMATCH is the gate and UNSUPPORTED is a coverage number; never clear a MISMATCH by widening a capability table (CLAUDE.md invariant 1). Programs whose output cannot be equal on two interpreters — timestamps, pids, set order — run with stdout uncompared (conformance.is_nondeterministic, decided on the program’s AST so a name inside a string or a comment does not buy the waiver). The report says what each arm’s MATCHes rested on — stdout, stderr, exit only, both failed — because a verdict that compared nothing is not equal in standing to one that compared output; reference and engine share one deadline, so a reference timeout leaves the measurement and an engine-only timeout is a MISMATCH. The same run grades the routes — IDEAL, WASTED, LATE, UNSAFE (routing.py); UNSAFE must be 0, and accuracy is a census, not a cost model: a LATE is a CPython spawn, a WASTED an in-process parse (measured 2026-09-04, CHANGELOG.md #42) — and holds the two dispatchers to each other: dispatchers agree N/N, the floor rule, monotone violations 0 (CLAUDE.md invariant 10). --plan ranks the refusals by cost (->cpy, a CPython spawn per program); lypning routes --plan is its companion. docs/VERIFICATION.md §C3–C5.

6. Performance tools

bench compares arms; corpus-time compares runs. lypning bench prints two totals over cpython, lypning, lypning-l and mixture, interleaved: the shared subset every arm ran, the only apples-to-apples comparison, and the whole corpus, where an arm that refuses work is annotated cheaper because it REFUSES, not because it is faster. lypning corpus-time --record F, then --baseline F after the change, times one binary twice and diffs the runs. lypning perf finds the gradient — one loop per construct, startup subtracted — and is not an acceptance gate: find with perf, accept with corpus-time. lypning gate is static — bytes in blocks of 131,072 B (gate.DEVICE_BLOCK), file opens. bench is not in CI: a wall-clock benchmark on a shared runner measures the runner. Every battery runs behind the net (CLAUDE.md invariant 4; docs/VERIFICATION.md §C6, §C8).

7. Corpus, capture, and privacy

The corpus is the argument: what agents actually typed, captured from real sessions. Two feeds append JSON lines to ~/.lypning/invocations.jsonl — the shim catches every invocation that reached an interpreter, the PreToolUse hook the Bash command string. The Stop hook publishes a session’s captures under tests/corpus/sightings/, and lypning harvest derives corpus.jsonl from them, redacting before the id is computed (docs/CAPTURE.md, Privacy: the log itself is not redacted and stays outside the repository).

Nothing is ever committed on your behalf. The hooks write files; they do not run git. Hooks never block and never fail a session: every one prints {"continue":true,"suppressOutput":true} and exits 0 on every path (CLAUDE.md invariant 5; docs/VERIFICATION.md §C9). LYPNING_CAPTURE=0 disables both feeds; LYPNING_HARVEST=0 keeps capturing, stops publishing.

What this tree loads, from one run — lypning corpus --stats, 2026-09-14, commit a33a0c9, Linux x86_64-unknown-linux-musl: 9064 entries (hook 79.8%, transcript 10.9%, shim 7.4%, seed 1.8%); lypning status that run put lypning at 1,142,992 B / 9 blocks and lypning-l at 1,319,120 B / 11 blocks. hook and transcript are largely what sessions working on lypning typed, so a build order read off the corpus is partly a mirror; the split is printed so it can be read that way.

Publishing and deriving are two steps, and only the first is automatic. The Stop hook publishes sightings every session; lypning harvest — “run deliberately, never from a hook” — is what turns them into corpus.jsonl. On 2026-09-13 that second step had not been run in some time and 7,243 published programs were sitting underived, so every tool in the tree quoted 3,688 loaded against a corpus that was really 8,901. Folding them put 5,376 unseen programs in front of the engine and lypning conformance answered with 19 MISMATCHes — nineteen silent wrong answers, none of them a regression, all of them defects a stale denominator had never exercised. They are closed (CHANGELOG.md, 2026-09-13); the lesson worth keeping is that the corpus only argues with the engine after somebody runs lypning harvest.

7b. Teaching a model the subset — and what the measurement said

The engine refuses what it does not implement, and a refusal costs a CPython spawn. So: can a model be taught to write the subset instead? training/ is the apparatus that answers that with a number rather than an impression — a frozen held-out split, a pre-registration written before any adapter existed, and a decision rule fixed in advance.

Run of record, 2026-09-14. A rank-16 LoRA over Qwen3.8-27B, trained on 318 rejection-sampled examples (222 of them the rewrite task) that each provably reproduce CPython’s output and provably run on the engine. Both arms generated in one container — same transformers, torch, kernels, H200, sampling dict, the adapter the only difference — and graded by one engine, fingerprint 9d412a3131dc6a8a.

primary denominator, 70 non-degenerate held-out cases  
base arm 41.16%
tuned arm 45.62%
paired delta +4.46pp, 95% CI [+1.52, +7.86]
bootstrap leg fires
exact McNemar leg does not — gained 2, lost 2, p = 1.0000
pre-registered verdict no win

The two legs disagree, and training/PREREGISTRATION.md §3 registered in advance that the disagreement would be the finding. It is: the adapter shifted per-case rates broadly — 16 of 70 cases improved, 6 got worse — rather than acquiring cases. Only two crossed from never-solved to solved.

Nothing was traded for anything: the rewrite slice went +4.04pp and the ceiling slice, which exists to catch a model that learns “never import” and rewrites what it should leave alone, went +8.04pp.

Two things this does not say. It does not say the adapter is inert — an interval excluding zero is evidence of something. And it does not say the rule was tuned to produce this answer: the discordance definition was amended on 2026-09-13, before the data existed, to gain power against a concentrated effect; the effect came out broad instead, and the superseded statistic gives p = 0.0525, also failing. The prediction behind the amendment was wrong, it changed no verdict, and that is checkable only because it was dated first.

Whole run: $28.70. The apparatus, the pre-registration and its outcome are in training/ — §6 of training/PREREGISTRATION.md is the result written back against the rule it was measured by.

8. Credit

This package was extracted from github.com/kristerhedfors/deepresearch.se, where it was developed as mopy (the Rust subset) and pygram (the MicroPython variant) to make Python affordable inside that project’s in-browser CheerpX sandbox. The measurements in §1, the corpus, the conformance battery and the capture harness all come from there. CHANGELOG.md carries the dated history under Before the name, with links to the upstream pull requests; those two names appear in this repository only there, here, and inside the historical corpus JSONL, whose captured programs are left verbatim.

MIT licensed. See LICENSE.


9. Repository layout

src/lypning/   cli.py (the front door) · engines.py (find, run, route, dispatch) · paths.py · build.py · gate.py · conformance.py ·
               routing.py · routes.py · fuzz.py · bench.py · perf.py · pool.py · corpus.py · capture.py · harvest.py ·
               install.py · shim.py · embed.py · harness/ — and assets/: rust/ (the one crate) · include/ (lypning.h, .hpp) · examples/
               node/ go/ swift/ lua/ (one quickstart each) · corpus/ · prompt/ · claude/ opencode/
               openhands/ shim/ scripts/ (what install writes)   —   docs/ · site/ (Pages) · study/ · tests/ · Makefile (`make help`)

Start with lypning overview. It prints the map above from the tree itself, every contract docs/VERIFICATION.md declares with whether it is pinned and by what, and each variant measured against its own block budget. --deep runs every pin and the whole suite and replaces each not measured with a verdict. Nothing in it is a remembered number (invariant 3), and a contract declared with no runner or no pin shows up there as a hole rather than as silence.

doc what
docs/VERIFICATION.md the QA spine: every contract as a command, its expected output from a dated run of record, the failure text a regression prints, and the test that pins it
docs/LYPNING.md the design: the measurement, the subset, the refusals, the classifier, the dispatcher, the commit barrier
docs/SUBSET.md what the subset must execute, entry by entry
docs/DIFFERENCES.md how lypning and lypning-l differ from Python: the architecture, the names each one resolves, and the refusals that skip the larger engine
docs/L-COVERAGE.md the expanded L surfaces, their exact boundaries, and the evidence needed before manually starting the next training round
docs/BIGINT-NUMERIC.md wide byte conversion and exact finite-float ratios: representation, limits, and differential checks
docs/COOKBOOK.md unsupported Python, rewritten — what to type when an engine refuses
docs/CAPTURE.md the two capture feeds, the harvest, and the privacy rules
docs/MODEL-TRAINING.md model training end to end — capture, case banks, verification, SFT and RL, evaluation and every result so far, one figure per stage; the mechanisms live under training/
docs/HARNESSES.md wiring capture into opencode and the OpenHands SDK: what each install writes, what it refuses to write, and what is verified against a real install
docs/EMBEDDING.md linking the runtime into a harness: the C ABI, the hosts over it, and what a refusal means when there is no exit code
docs/SANDBOX-PERFORMANCE.md the cost model — cold blocks, the exec floor, spawns — measured upstream, dated
docs/PROMPTING.md can an agent be asked into the subset? nine prompt treatments, measured 2026-08-23
docs/COMPARISON.md against ADK-Rust CodeAct + Monty: one instrument over the corpus, both columns measured
docs/PAPER.md the write-up: what coding agents actually emit, and CPython / PyPy / MicroPython / Monty / lypning benchmarked on it
docs/EXECUTIVE-SUMMARY.md the verdict: where lypning improves, where it regresses, where it loses, and the biases that flatter it
docs/RESEARCH.md how the reimplementation was chosen — history
docs/BENCH-LEDGER.md append-only measurement history, including the losses
docs/HILLCLIMB.md append-only ledger of improvement steps — the four numbers each moved, and the ones that moved nothing
docs/FORKING.md fork it and tune it to YOUR programs: the capture→harvest→gate→step loop

site/build.py publishes this markdown at kristerhedfors.github.io/lypning (enable Pages once: Settings → Pages → Source: GitHub Actions). Working on this repository? Read CLAUDE.md first, then the hillclimb skill under .claude/skills/. Check it yourself, with ~/.lypning/bin built:

lypning build --rust && lypning conformance --mixture both && lypning doctor && lypning gate
# → `ok` per variant · MISMATCH 0, dispatchers agree N/N · 0 FAIL · PASS — docs/VERIFICATION.md §C1–C15