# FrankenLean — RULEBOOK v1.0 Assessment Packet v5

**Repository:** `Dicklesworthstone/franken_lean` · **Language:** Rust [Code-verified, High] · **Pinned commit:** `e91da19970591cf5c0ed0c113b475d748577291c` (2026-09-22 11:17:18 −0400, [Git-observed, High]) · **Last push:** 2026-09-22 (pin date; the pin is the latest push confirmed via the GitHub API, [External, High]) · **Scope:** the pinned commit only, shallow clone. Stars: 17 · forks: 4 · created 2026-07-21 ([External, High]; the task brief's "~9 stars" is stale — the API count is 17). License: MIT + OpenAI/Anthropic Rider — **non-OSI** ([Verified, High], full rider quoted in §4.8).

**Method (analyst):** shallow clone at the pin under `~/workspace/.scratch/franken_lean` (839 `.rs` files, 731,657 lines, 32 crates — all [Counted, High]). Read: `README.md` (533 lines), `IMPLEMENTATION_STATUS.md` (257 lines, including its five-tier evidence vocabulary: landed / model-verified / artifact-bound / observed / target), `LICENSE` (verbatim), `SUITE.lock`, `AGENTS.md` (doctrine), `KERNEL_CONTRACT.md`, `CHANGELOG.md`, `ci/UNSAFE_LEDGER.txt`, all 32 crate roots' dependency sections and `lib.rs` charter headers, `Cargo.lock` (source analysis), kernel/checker/wasm/jit source samples. Counted: `.rs` files/lines, `#[test]` annotations (7,140 in 603 files — declared inventory, never executed), `unsafe` sites per crate via regex on `unsafe {`, `unsafe fn`, `unsafe impl`, `unsafe extern` (occurrence-level upper bound: includes comments and string literals, e.g. a test that asserts the *absence* of `unsafe {`). Queried the GitHub Actions REST API for the pin's CI: run `35746280136` (`ci` workflow, head = pin) with per-step conclusions; repository releases/tags (0/0); contributors (Dicklesworthstone 929 commits, web-flow 78, github-actions[bot] 42, codex 2 — effectively one human author [External, High]). Verified all 9 shareable URLs return HTTP 200. **Not done:** no cargo or rustc on the analysis host — the workspace was never compiled, no test was executed, no benchmark was reproduced, no full CI log text was read (step-level conclusions only), and the git history is unusable (depth-1 clone; authorship/velocity assessed via the API instead). "Beads" below = the repo's issue-tracker unit (`.beads/issues.jsonl`); "G0→G6" = the plan's six convergence gates from de-risking spikes (G0) to the sovereign toolchain (G6). Assessment date: 2026-09-22.

**Tier legend (Rulebook §1):** **[Verified]** direct inspection of the pinned clone or a live page read by the analyst — flavors **[Counted]** (I ran the count), **[Git-observed]** (git metadata), **[Code-verified]** (source read); **[CI-observed]** is Tier 2 (seen executing on live CI pages — attests the suite *runs*, not that it is green); **[Maintainer claim]** asserted in README/docs, not independently executed; **[External]** independent sources; **[Inference]** analyst judgment, always labeled. Confidence: **High** (multiple converging sources or direct inspection) / **Medium** (single solid source, plausible) / **Low** (thin evidence, extrapolation).

---

## Hook

A 731,657-line [Counted, High], single-maintainer, ground-up Rust reimplementation of the *entire Lean 4 toolchain* whose README opens by confessing it is written "in the present tense, as if the entire design… is fully realized," and whose kernel crate contains a module (`council.rs`) that opens by listing what it does *not* claim. Its most distinctive engineering asset is that honesty, enforced as machinery; its defining risk is the gap between the admitted target-state and the live bounded slices. **CI at the pin is red on the main gate — 11 of 30 steps failing.**

## TL;DR

**Verdict:** franken_lean is the most self-auditing repo in this assessment program — an attempt to rebuild Lean 4's whole substrate natively in Rust with a methodology export (machine-checked claim matrix, anchor-bound kernel contracts, a CI-enforced unsafe-site ledger) that is arguably more valuable than the prover itself. What demonstrably exists: a zero-external-dependency 731k-line workspace [Counted, High], a `forbid(unsafe)` kernel with zero project-authored unsafe blocks [Code-verified, High], a bounded Nat/Bool/String source pipeline that parses, dual-checks (K1 + independent checker), compiles to a register VM, and executes [Maintainer claim, Medium — CI shows a 103-pass elaborator run on a neighboring commit, not the pin], and contract machinery (ABI/olean censuses mechanically extracted from the pinned Reference; kernel rules anchored to upstream source lines with `expect=` tokens that fail CI on drift) [Verified, High]. What does not exist: K2/NbE (explicitly disclaimed in `council.rs`), corpus-scale differential checking, any measured performance gate (README states "0 bench targets"), a release artifact, and a green CI gate at the pin. **TRL 4** — bounded slices execute in a lab environment (relevant-environment validation), short of TRL 5 (no integration in a relevant environment). **NODUS ring: Explore.** Strongest strength: the evidence-governance machinery (B8) — a claim matrix with evidence states and documentation CI that rejects wording stronger than the matrix permits — is a genuine methodological contribution, and it is partly *already enforced* (the bidirectional unsafe-ledger census passed CI at the pin [CI-observed, High]). Strongest ceiling: **institutional un-adoptability** — one maintainer who refuses outside contributions, a license rider that bars the AI labs most able to validate it from even benchmarking it, and CI red at the pin, so the project's own gates cannot currently certify its own claims. These three are one mechanism, not three problems.

## Quick Links

- [Repository](https://github.com/Dicklesworthstone/franken_lean)
- [README](https://github.com/Dicklesworthstone/franken_lean/blob/main/README.md) — read the "note on tense" first
- [Implementation status (the honest current-state file)](https://github.com/Dicklesworthstone/franken_lean/blob/main/IMPLEMENTATION_STATUS.md)
- [License (MIT + rider, verbatim)](https://github.com/Dicklesworthstone/franken_lean/blob/main/LICENSE)
- [CHANGELOG](https://github.com/Dicklesworthstone/franken_lean/blob/main/CHANGELOG.md)
- [Master plan (design spec)](https://github.com/Dicklesworthstone/franken_lean/blob/main/COMPREHENSIVE_PLAN_FOR_THE_DESIGN_OF_FRANKEN_LEAN.md)
- [Kernel contract (rule-by-rule judgments)](https://github.com/Dicklesworthstone/franken_lean/blob/main/KERNEL_CONTRACT.md)
- [CI workflows](https://github.com/Dicklesworthstone/franken_lean/tree/main/.github/workflows)
- [Contracts (mechanically extracted censuses)](https://github.com/Dicklesworthstone/franken_lean/tree/main/contracts)

## Did you know?

Every rule in the kernel's judgment specification is handcuffed to the enemy's source code: `KERNEL_CONTRACT.md` gives each rule an `anchor:` line naming the exact upstream file and line at the pin — e.g. `anchor: vendor/lean4-src/src/kernel/type_checker.cpp:289 (infer_type_core) expect="infer_type_core"` — and a conformance test (`crates/fln-conformance/tests/kernel_contract.rs`) fails CI if the token on that line ever changes [Code-verified, High]. The spec doesn't just describe the type theory; it machine-detects when upstream moves underneath it.

## Franken-worthy next steps

1. **Export the claim matrix, not the prover.** Port the B8 apparatus — per-claim evidence states, freshness bounds, documentation CI that rejects wording stronger than the matrix permits — to a second FrankenSuite repo as a standalone crate; the Tribunal's `fln-conformance` census tests are the prototype. *Falsifiable:* within 60 days, one sibling repo's CI blocks a PR for an overstated claim. If none adopts it, the methodology is ceremony, not export.
2. **Productize the upstream handcuffs.** Generalize KERNEL_CONTRACT's `anchor:`/`expect=` mechanism into a `contract-anchor` tool any clean-room project can use to bind its spec to upstream source lines with drift-failing CI — a different artifact from #1 (spec-vs-upstream binding, not claim-vs-evidence governance). *Falsifiable:* at the next Lean epoch bump, the anchors machine-flag the moved upstream kernel lines before any human notices; if humans find them first, the mechanism is ornament.
3. **Ship the WASM Judge before the prover.** The sealed-capsule verifier design exists (`fln-wasm` charter: K1 + `fln-checker` + capsule verifier behind a `verify_capsule` C-ABI surface [Code-verified, Medium — the crate is currently a 161-line charter, not a working WASM build]), and the bounded-live `check-olean` path plus the anti-hollow-green council script (`scripts/check_pinned_nat_council.py`, which "cannot produce a hollow green when the artifact is absent" [Maintainer claim, Medium]) supply the demonstrated rigor. *Falsifiable:* one party outside the maintainer's household verifies a sealed capsule in a browser tab and publishes the receipt within 90 days. If nobody does, the trust story is marketing.
4. **Generalize the thread-matrix determinism harness.** The per-commit {1, 8, 32}-thread schedule-independence test over the Prelude is real infrastructure (`thread_matrix_determinism.rs` exists [Code-verified, High]); factor it into a reusable crate with the corpus-scale on-demand lane as its second tier. *Falsifiable:* a second project adopts the harness and reports a schedule-dependent bug it caught. No adopter candidate is currently identified — that absence is itself the experiment's first datum.
5. **FLBC + O(1) snapshots as the agent-proof-search substrate.** The register VM whose values are ABI objects, combined with persistent-map environment snapshots, is exactly what the 2026 proof-search literature hand-rolls per paper (the README's own framing); publish the snapshot/fork API as a standalone benchmark: branches-per-second vs. the subprocess-per-branch baseline. *Falsifiable:* a published measurement on a fixed tactic micro-corpus. If the measurement never appears, the "agent-native" bet is a slide.

---

## 4.1 Header

Covered above: repo, pin `e91da19970591cf5c0ed0c113b475d748577291c` (2026-09-22 11:17:18 −0400), Rust, MIT+OpenAI/Anthropic rider (non-OSI), 17 stars / 4 forks, last push 2026-09-22, created 2026-07-21, assessment 2026-09-22, analyst method including what was not done. The task brief's "100% safe Rust, zero unsafe blocks" tagline is **disproven**: project-authored `unsafe` exists in three named boundary crates (≈750 occurrence-level regex matches in `fln-unsafe-abi` as an upper bound, [Counted, Medium]), which the repo itself documents as the design, not a violation.

## 4.2 Executive verdict

franken_lean is a ground-up native-Rust reimplementation of the *entire* Lean 4 toolchain (parser, elaborator, kernel, VM, ABI twin, build system, language server) currently realized as bounded vertical slices — a working source→kernel→VM pipeline for a Nat/Bool/String subset, a `forbid(unsafe)` kernel with zero unsafe code, and an unusually rigorous evidence-governance apparatus — under a present-tense README that explicitly describes the 1.0 target state rather than the pin (the "note on tense" is verified README text [Verified, High]). **TRL 4** (component validation in a laboratory environment: bounded slices execute; no corpus-scale or integration validation). **NODUS: Explore** — substantive but unproven; no release artifact (0 tags, 0 releases [External, High]) rules out Pilot under the ring rules, and there is real technical substance beyond a plan. The single most important strength is the evidence machinery: a machine-checked claim matrix, kernel rules anchored to upstream source lines with drift-failing CI, and an unsafe-site ledger with a bidirectional CI census — methodology that would survive the prover's failure. The single most important ceiling is institutional un-adoptability (see TL;DR). No hedging beyond the attached confidence grades.

## 4.3 Claim inventory

| # | Claim (source) | Status | Evidence |
|---|---|---|---|
| 1 | Entire Lean 4 toolchain reimplemented natively in Rust, drop-in at six binary surfaces (.olean, `lean_object` ABI, LSP, CLIs) | **aspirational** | README describes the 1.0 target state by its own admission ("note on tense") [Verified, High]; LSP currently returns no-information nulls for goals/hover/completion [Maintainer claim, Medium] |
| 2 | Kernel is ≤ 12 KLOC, dual-engine (certified small-step K1 + NbE accelerator K2), `forbid(unsafe)` | **partially demonstrated** | `fln-kernel` lib is 17,051 lines [Counted, High] — already 1.42× the ≤12 KLOC badge; kernel root carries `#![forbid(unsafe_code)]` and zero actual unsafe blocks [Code-verified, High]; **K2/NbE does not exist** — `council.rs` "does not claim K2 or NbE exists" [Code-verified, High] |
| 3 | Independent checker (`fln-checker`) provides a second, foreign-blooded implementation | **partially demonstrated** | 68,243 lines [Counted, High] — 4× the kernel's 17,051 lib lines (2.2× on all-in totals); wired as an independent seat in the bounded `fln` Engine admission path [Code-verified, Medium]; full completion is a named future bead (`franken_lean-gii`), "corpus-complete" explicitly disclaimed [Code-verified, High] |
| 4 | "100% safe Rust, zero unsafe blocks" (task brief) / README badge "unsafe: forbidden\*" | **disproven** (brief) / **partially demonstrated** (README's own framing) | ≈750 occurrence-level regex matches in `fln-unsafe-abi` (upper bound — includes comments/strings), 10 in `fln-unsafe-region`, 0 in `fln-unsafe-jit` (a 15-line stub) [Counted, Medium]; **every one of the 32 crate roots** carries `#![forbid(unsafe_code)]` (ordinary crates) or `#![deny(unsafe_code)]` (the three boundary crates, whose narrowly-scoped `#[allow]` sites are ledgered) [Code-verified, High — all roots checked]; 697-row `ci/UNSAFE_LEDGER.txt` with a bidirectional CI census that passed at the pin [CI-observed, High] |
| 5 | Closed dependency universe: std + pinned nightly + named FrankenSuite, no serde/tokio/LLVM/GMP | **demonstrated** | `Cargo.lock` contains zero `source =` entries — every dependency, including dev-dependencies, is a workspace path crate [Verified, High]; the named suite deps (asupersync, frankensqlite, …) are pinned in `SUITE.lock` to `/dp/*` paths but appear in **no** crate's `Cargo.toml` — allowed but currently unwired [Verified, High] |
| 6 | Deterministic parallel elaboration: same results at {1, 8, 32} threads, tested per commit | **partially demonstrated** | Per-commit thread-matrix test exists (`thread_matrix_determinism.rs`) but its input is the Prelude; the corpus-scale matrix ran once on demand (README documents this as a shortfall vs. the gate, bead `fln-corpus-thread-matrix-93te`) [Maintainer claim, Medium]; a SUITE.lock/toolchain pin inconsistency (preflight expects nightly-2026-07-13 vs. functional run on nightly-2026-08-31) is self-reported [Maintainer claim, High] |
| 7 | Performance gates (PG-1…PG-M): kernel-recheck ≤ 5 min, corpus ≤ 0.5× Reference, etc. | **aspirational** | README states verbatim: "No gate above has been measured… **0 bench targets, 0 committed baselines and 0 flame artifacts**… Every number in the table is therefore `TARGETED`, none is `OBSERVED`" [Maintainer claim, High — a disavowal, not a result] |
| 8 | `fln check-olean` re-checks mathlib oleans on a foreign kernel with receipts, "in minutes" | **partially demonstrated** | Bounded `.olean` tooling (inspect/diff/verify-rebuild) is in the "Live today (bounded)" list [Maintainer claim, Medium]; the pinned-Nat-council artifact-bound regression exists with a non-vacuous runner script [Maintainer claim, Medium]; "minutes on all of mathlib" is unmeasured (see claim 7) |
| 9 | Native elaborator handles real Lean source (Nat/Bool/String defs, `#eval`, `#check`, bounded imports) | **partially demonstrated** | CI run 35742621315 (the preceding commit observed via the Actions API, `dff590f8`, not the pin) reported 103 passed / 0 failed for `fln-elab` [CI-observed, Medium]; IMPLEMENTATION_STATUS documents the bounded slice in detail and lists general elaboration (implicits at scale, tactics, instance search, TC synthesis) as open [Maintainer claim, High] |
| 10 | KERNEL_CONTRACT.md: rule-by-rule judgment spec anchored to exact Reference source lines, CI-checked | **demonstrated** | 731-line normative doc; sample anchors name `vendor/lean4-src/src/kernel/type_checker.cpp:289` with `expect="infer_type_core"` [Code-verified, High]; the `kernel_contract.rs` conformance test's mechanism — resolving every anchor against the pinned Reference source tree — is code-verified [Code-verified, High]; test execution not observed |
| 11 | ABI/`lean.h` layouts and `.olean` codec mechanically extracted from the pin (never hand-copied) | **partially demonstrated** | `contracts/` holds `ABI_TARGET_LAYOUT.txt`, `ATTRIBUTE_STATE_CENSUS.txt`, etc.; `ABI_CONTRACT.md`/`OLEAN_CONTRACT.md` exist at root [Verified, High]; the extraction scripts' outputs were inspected but their mechanical provenance was not re-executed [Medium] |
| 12 | Reference (lean4 v4.32.0) and Corpus (mathlib4 v4.32.0) pinned; upstream never executes as a component (Oracle-Only Law) | **partially demonstrated** | `SUITE.lock` pins `leanprover/lean4 tag=v4.32.0 commit=8c9756b2…` and `mathlib4 tag=v4.32.0 commit=81a5d257…` [Verified, High]; `vendor/` carries upstream sources under Apache-2.0 [Verified, Medium — directory seen, contents not audited]; the Oracle-Only Law is asserted as doctrine, but the `ci` gate that would enforce it is red at the pin (see §4.5) |
| 13 | MCP/agent surfaces (`fln serve-mcp`, O(1) proof-state snapshots, `fln goals`) | **aspirational** | `fln-mcp` crate exists; README lists `serve-mcp`, `goals`, `cache`, `doctor --sql`, `replay`, `build explain` as "the 1.0 target… not shipped code" [Maintainer claim, High] |
| 14 | `lake`/`leanc` binary personalities, flag-compatible CLIs | **aspirational** | A native `lean` personality binary exists in bounded form (one source path, no `LEAN_PATH`/package discovery/diagnostic parity) [Maintainer claim, Medium]; `lake`/`leanc` listed as 1.0 target, not shipped [Maintainer claim, High] |

## 4.4 Architecture (reconstructed from the code)

The workspace is **32 crates** under `crates/*` plus `tools/*` (members via glob [Code-verified, High]), organized by an explicit cycle-free crate map acknowledged in `WORKSPACE_GRAPH.txt` and enforced by `tools/structure-guard` (tool exists with src and tests [Code-verified, High]; enforcement not executed here). Verified line counts (`.rs`, lib + tests): whole tree 731,657 lines / 839 files [Counted, High]; `fln-kernel` 30,949 (lib-only 17,051; `tc.rs` alone 10,399); `fln-checker` 68,243 [all Counted, High]. Crate→subsystem mapping confirmed from each crate's `lib.rs` charter header [Code-verified, High]: Marrow (`fln-rt`, `fln-unsafe-abi`), Grimoire (`fln-env`, `fln-olean`), Crucible (`fln-kernel`, `fln-bignum`, `fln-checker`), Vellum (`fln-parse`, `fln-syntax`), Athanor (`fln-elab`), Golem (`fln-comp`, `fln-vm`, `fln-unsafe-jit` — 15-line stub), Anvil (`fln-anvil`) + Verdict (`fln-verdict`, the owned CDCL solver), Ledger (`fln-ledger`, `fln-lake`), Lantern (`fln-server`), Palimpsest (`fln-trace`), Bloodhound (`fln-hound` — in-toolchain search), Folio (`fln-doc` — doc-gen4-compatible docs), Envoy (`fln-mcp`), Tribunal (`fln-conformance`), WASM Judge (`fln-wasm` — 161-line charter), terminal InfoView (`fln-tui` — over frankentui), owned deterministic transcendentals (`fln-libm`), measurement substrate (`fln-bench` — 0 bench targets), plus `fln-core`, `fln-hash`, `fln`, `fln-cli`. The *live* bounded data flow — source bytes → Pratt parser → bounded elaborator (constraint/unify worklists) → K1 admission + independent-checker veto → FIR/FLBC compiler → Golem register VM — is edge-verified at the critical junction: `fln-elab` declares `fln-kernel` as a path dependency and `use fln_kernel` appears in its constraint solver (`constraint/unify.rs`, `constraint/unify/residual.rs`) and `inductive.rs` [Code-verified, High]. The remaining sequencing (compiler→VM handoff, checker-veto wiring) is manifest-plausible and status-described, not edge-traced here [Medium]. **The asupersync question:** asupersync appears in `SUITE.lock` (commit `8522f941…`, path `/dp/asupersync`) and in AGENTS.md's dependency doctrine — but in **zero** crate manifests and **zero** `use` statements: a pinned-but-unwired future substrate, not a runtime dependency [Verified, High]. The dependency posture is *stronger* than claimed in one dimension (zero external crates.io deps of any kind) and weaker in another (the vaunted FrankenSuite integration is currently documentation, not code). README-vs-code drift: (a) kernel 17k lib lines vs. ≤12 KLOC badge; (b) dual-engine badge vs. K2's explicit non-existence; (c) "closed universe" naming deps that aren't wired. Each is consistent with the README's stated target-state tense, but the badges are the one place the tense note doesn't fully protect — a badge asserts the present [Inference, Medium].

## 4.5 Benchmark and conformance audit

**Maintainer numbers:** none claimed as results. The README's performance-gate table (PG-1…PG-M, PG-K, PG-1b) is explicitly disavowed: "0 bench targets, 0 committed baselines and 0 flame artifacts… Every number in the table is therefore `TARGETED`" [Maintainer claim, High]. `crates/fln-bench` exists as measurement *substrate* with 0 bench targets [Code-verified, High]. This is the correct posture — an honest zero, with nothing to audit.

**Independent numbers:** none exist. Web-searchable coverage of franken_lean: none found beyond the repo itself (absence reported with the caveat that search recall on a 17-star repo is thin) [External, Low].

**CI at the pin — the conformance story is red:** the `ci` workflow run `35746280136` (head = pin `e91da199`) concluded **failure** [External, High]. Its single job "quality gate (check.sh + e2e smokes)" failed at **11 of 30 steps**, including `quality gate (scripts/check.sh)`, `ownership evidence — clean source-bound matrix`, `tribunal epoch-lab nested workspace`, `gate self-test`, and six e2e smoke steps (Vellum lexer real-file contract, Vellum parser-corpus real-file contract, Vellum macro hygiene, structural gate, dependency-closure audit, Tribunal campaign frameworks), plus `verify and index complete evidence attempt` [External, High — per-step conclusions from the Jobs API; full log text not read]. Two other pin-headed runs (`fln-lsp-jsonrpc-lifecycle-landing`, `windows-functional`) also failed [External, High]. On the preceding commit observed via the Actions API (`dff590f8`, same day), the native-elaborator lanes were mixed: `Native elaborator functional tests` **success** (the 103-pass observation cited in IMPLEMENTATION_STATUS), while `Native instance variant integration`, `Native propositional logic`, `Native equality decision tests`, `Native mutual source checking`, and `Native unifier integration` **failed** — 5 of 8 lanes failing, 3 succeeding (`Native named arguments` and `Native goal inspection` also succeeded) [External, High]. How long the gate has been red is unknown — the 30 most recent runs sampled all date from 2026-09-22 (high push velocity); longer history was not sampled [External, Medium]. Reproduction cost: a cold checkout is the whole 731k-line tree; the pinned toolchain is `nightly-2026-08-31` (`rust-toolchain.toml`); Reference/Corpus checkouts are pinned in `SUITE.lock` and are large multi-gigabyte trees [Inference, Medium — sizes not measured]. Reproduction was not attempted (no cargo on the analysis host), and CI itself currently demonstrates the gate does not pass. One structural note: the steps that *passed* at the pin include the bidirectional unsafe-note census, the extern/builtin census, the attribute-state census, and the environment-snapshot smokes — the gates that enforce honesty pass while the gates that assert capability fail [External, High].

## 4.6 Comparison: who owns the lane

The lane — a trustworthy, fast, agent-legible Lean 4 toolchain — is owned by the **Reference itself** (`leanprover/lean4`): it is the only implementation that runs mathlib, elaborates real Lean, and ships a working toolchain; its costs (C++ TCB, stage0 bootstrap, file-granular builds, ~60 s/worker import tax, schedule-sensitive async elaboration) are the problems franken_lean names. Kernel-only checkers (`lean4lean`, `lean4checker`, nanoda-class Rust kernels — small independent kernel re-checkers) own the narrow "independent re-check" lane but run no tactics and move none of the ecosystem bottlenecks — franken_lean's comparison table concedes their existence and correctly argues they don't address the build treadmill [Maintainer claim, Medium — the concession is accurate as far as it goes]. Adjacent lanes: Rocq (the former Coq — mature, large corpus, but a different language and no Lean compatibility), and the 2026 agent-proof-search literature that hand-rolls prover harnesses per paper. Why the incumbent wins today, in one paragraph: the Reference is the only artifact that satisfies the *entire* compatibility surface — it elaborates all of mathlib, its tactics run, its `.olean`s load, its LSP serves editors — while franken_lean's compatibility is staged at L0–L4 per surface with most surfaces at L0/L1 and the corpus-scale differential rig an on-demand lane rather than a per-commit invariant; a prover toolchain is adopted on "runs my project," and nothing in this repo yet does. The genuinely unoccupied lane [Inference, Medium]: **evidence-native prover engineering as a product** — no other prover project ships a machine-checked claim matrix, drift-failing upstream-anchored specifications, and a CI-enforced unsafe ledger as first-class artifacts; and the **WASM-sealed-capsule third-party verification** story has no incumbent at all.

## 4.7 Technical merit and adversarial review

**Strengths.** (1) The evidence-governance apparatus (B8) is real and partly CI-enforced: the bidirectional unsafe-note Clippy census passed at the pin even inside a failing gate [CI-observed, High], and KERNEL_CONTRACT's `anchor:`/`expect=` mechanism binds the spec to the enemy's source with machine-checked drift detection [Code-verified, High]. (2) The dependency posture is extraordinary: zero external crates.io dependencies across 731k lines [Verified, High] — the "closed universe" is not marketing. (3) The bounded vertical slice is genuinely integrated, not a mock: one source file traverses parser → elaborator → K1 + independent checker → compiler → register VM with budgets, receipts-shaped robot output, and a non-vacuous pinned-artifact council regression that "cannot produce a hollow green when the artifact is absent" [Maintainer claim, Medium — the anti-vacuity design is in the script; execution was not observed here]. (4) The codebase's self-negation culture — `council.rs`'s "What this does NOT claim," IMPLEMENTATION_STATUS's five-tier evidence vocabulary with "landed ≠ verified," the README's tense note — is a substantive engineering control against the exact failure mode (README marketing) the Rulebook's claim inventory exists to kill.

**Weaknesses.** (1) The TCB geometry is lopsided: the "independent" checker is 68k lines vs. the kernel's 17k lib lines (2.2× on all-in totals) — the second implementation is several times the thing it checks, written by effectively one author (929 of 929 human-attributed commits [External, High]), so "independent" means implementation-diverse, not institutionally independent. (2) Scale without integration: 731k lines across 32 crates, but the flagship integrations (asupersync runtime, frankensqlite store, atp cache federation) are pinned in a lockfile and described in doctrine while appearing in zero manifests — the architecture's load-bearing foundations are unwired [Verified, High]. (3) CI is red at the pin on the main gate with 11 failed steps, and the preceding commit shows 5 of 8 native-elaborator lanes failing — the project's own verification apparatus does not currently certify the project's own code [External, High]. (4) Bus factor 1 with an explicit no-outside-contributions policy (README "About Contributions") — velocity is entirely coupled to one maintainer's bandwidth, and the policy is stated as non-negotiable [Verified, High]. (5) Reviewability: the plan promises K1 as "the certified evaluator a skeptical logician reads in an afternoon," but the checking core is a single 10,399-line `tc.rs` — no logician reads that in an afternoon, and the ≤12 KLOC budget is already spent before K2 exists [Counted, High; Inference, Medium].

**Bear-case steelman.** franken_lean does not matter because a prover toolchain is a *compatibility* product, and compatibility is won by running the corpus — which this project structurally cannot reach at its current velocity: the bounded slice covers Nat/Bool/String definitions while mathlib needs the full elaborator, TC synthesis, and tactic framework; the maintainer refuses the contributions that could parallelize that climb; the license rider excludes the AI labs whose proof-search programs are the named customers; CI is red at the pin, so even the existing slices aren't certified; and the Reference improves monthly, meaning the epoch ratchet is a treadmill the project runs alone. The honest documentation is admirable, but honesty about being at a small fraction of a multi-year goal is still a small fraction of a multi-year goal. What survives this steelman is only the methodology export — which is precisely next-step #1.

## 4.8 License and governance (material, not boilerplate)

LICENSE read verbatim (73 lines) [Verified, High]. It is the MIT text **plus a rider** that is part of the license's "conditions" and controls in any conflict. Exact scope, quoted: *"Restricted Parties" means OpenAI, L.L.C.; Anthropic, PBC; any of their respective Affiliates; and any person or entity acting directly or indirectly on behalf of, for the benefit of, or under the direction of any of the foregoing* … *"Notwithstanding any other provision of this License, no rights are granted to any Restricted Party"* … *"use" includes, without limitation: copying, modifying, merging, publishing, distributing, sublicensing, selling, transferring, making available, hosting, deploying, executing, **benchmarking, testing, analyzing, indexing**, or incorporating the Software or any Derivative Works into any dataset, training corpus, evaluation harness, or pipeline for machine learning or other automated systems.* **This is non-OSI** (discriminates against persons/groups and fields of endeavor; OSD 5/6) [Inference, High — the discrimination is textual, not interpretive]. Material consequence: the two organizations most capable of independently validating the prover (and the named agent-era customers) are *legally barred from even benchmarking it* — an adoption and validation ceiling, not just a licensing footnote. Vendored upstream Lean sources under `vendor/` remain Apache-2.0 with NOTICE files [Maintainer claim, Medium]. Governance: effectively one human author (929 commits; the only other human-attributed account, web-flow with 78, is GitHub's web editor — plausibly the same person [External, Medium]), explicit no-outside-contributions policy, same-day multi-push cadence visible in the Actions API on 2026-09-22 [External, Medium]. No releases, no tags, no release process observed.

## 4.9 NODUS factsheet

| Criterion | Score | Justification (one line) |
|---|---|---|
| Technology readiness | **TRL 4** | Bounded slices (parse→elaborate→dual-check→compile→VM) execute in-lab; no corpus-scale or integration validation; K2 absent |
| Strategic relevance | **3/5** | Prover substrate is strategic for the 2026 AI-for-math program the README targets, but the project cannot yet serve that program |
| Impact potential | **4/5** | If the 1.0 target existed, it would restructure the Lean ecosystem's build/trust economics; the methodology export alone could shift clean-room practice |
| Implementation feasibility | **2/5** | 731k lines at bus factor 1, red CI at pin, unwired foundations, and a multi-year compatibility climb against a monthly-moving upstream |
| Time to mainstream | **2/5** | G0→G6 staging is honest; G4 (full-mathlib elaboration) is multiple years out at current demonstrated velocity [Inference, Medium] |
| Collaboration potential | **1/5** | No-contributions policy + non-OSI rider excluding AI labs + single maintainer = collaboration is structurally refused |

**Ring: Explore.** Substantive but unproven is exactly this packet: real kernel, real VM, real methodology, zero release artifacts, zero independent validation, red CI. Pilot requires a release artifact plus a bounded real workload fit — neither exists. Ring down, not up.

## 4.10 Wardley placement

- **Commodity surface:** the Lean 4 *language and toolchain contract* (grammar, `.olean`, LSP dialect, `lean`/`lake` CLIs) — open, standardized by the Reference; franken_lean must clone it, not innovate on it. Movement: only upstream epoch bumps move it.
- **Custom-built reimplementation:** the native toolchain itself (kernel, elaborator, VM, ABI twin) — custom-built, pre-product; franken_lean's bounded slices sit here. Movement: corpus-scale differential parity would move components toward product.
- **Genesis-stage novel elements:** the evidence machinery (machine-checked claim matrix, upstream-anchored kernel contracts, CI-enforced unsafe ledger) and the WASM Judge / sealed-capsule verification story — genesis, unoccupied lane. Movement: adoption by a second project (next-step #1) would move the claim matrix from genesis to custom; an external sealed-capsule verification would move the WASM Judge to custom.

## 4.11 Trajectory (12 / 24 / 60 months) **[Inference]**

**Base case:** the project continues as a single-maintainer research program producing increasingly deep bounded slices and ever-better evidence machinery; the prover never reaches corpus parity, but the methodology artifacts (claim matrix, anchored contracts, unsafe ledger, thread-matrix harness) get copied by sibling FrankenSuite repos and possibly by outsiders who read the code despite the rider. CI stays intermittently red because the gate's ambition exceeds one person's green-keeping capacity.

**Bifurcation — upside:** the WASM Judge ships and one external party verifies a sealed capsule (next-step #3), creating the first independent validation event; or the claim-matrix apparatus is adopted by a second repo (next-step #1), making the methodology the product and the prover the demo. Either event justifies revisiting the ring. **Decay:** the epoch ratchet slips (upstream moves monthly; each missed ratchet doubles the conformance debt), the unwired foundations (asupersync, frankensqlite) rot in the lockfile, and the repo becomes a 731k-line monument — still the best-documented unfinished prover rewrite, but unfinished. At 60 months the live question is whether the methodology export outlived the prover: if yes, the repo mattered as a methods paper in code form; if no, it is an unusually honest ruin.

**Revisit triggers:** (1) first tagged release or installable toolchain artifact; (2) CI green at a pin on the main gate; (3) an external sealed-capsule verification published; (4) a second maintainer or a contribution-policy change; (5) an independent benchmark of any claimed slice; (6) K2/NbE landing (the badge becoming true).

## 4.12 Limitations and open questions

**Not done:** the workspace was never compiled (no cargo/rustc on the analysis host); no test was executed (the 7,140 `#[test]` annotations are a declared inventory, not an executed result); no benchmark was reproduced (none exist to reproduce); no full CI log text was read (step-level conclusions only); the vendored upstream sources were not audited; git history was unavailable (depth-1 clone); web-search recall on a 17-star repo is thin; longer CI history was not sampled (the 30 most recent runs all date from 2026-09-22). **Open questions that would most change the verdict:** (1) Would `cargo test --workspace` pass at the pin? (CI says the gate fails, but the exact failing assertions are unknown.) (2) Is the `fln-elab` 103-pass observation reproducible at the pin, or only on the preceding commit? (3) What fraction of the 731k lines is tests/fixtures/generated tables vs. logic? (4) Has anyone outside the maintainer ever run any of it? (5) What is the actual current L0–L4 level per compatibility surface in the Parity Ledger?

---

## The eight deepening questions

1. **Provenance.** The repo records artifact provenance obsessively at the *claim* level — every kernel rule carries an `anchor:` line with an `expect=` token bound to an exact upstream source line, every unsafe site carries an `// UNSAFE-LEDGER:` marker with a row in `ci/UNSAFE_LEDGER.txt`, and SUITE.lock pins the Reference, Corpus, toolchain, and suite commits in one ceremony [Verified, High]. Making that attestation portable is exactly what the sealed-capsule + transparency-log design (B3) proposes: a Merkle-logged receipt set a third party re-checks without trusting the producer [Maintainer claim, Medium]. Today the provenance is strong inside the repo and non-portable outside it — there is no published receipt anyone has verified.

2. **The embeddable unit.** The smallest adoptable piece is the *methodology*, not the code: the claim-matrix + docs-CI pattern and the `anchor:`/`expect=` upstream-binding mechanism are each liftable without the prover (next-steps #1–2). Of the code, the most plausible unit is `fln-bignum` (owned kernel-grade bignum, no GMP) or the thread-matrix determinism harness — small, dependency-free (zero external deps workspace-wide [Verified, High]), but adoption cost is currently prohibitive in practice: no releases, no crates.io publication, a license rider that bars AI-lab use, and a no-contributions policy that makes even bug reports one-directional.

3. **Unexercised option value.** The architecture holds three large unused options: (a) the pinned-but-unwired FrankenSuite foundations (asupersync's regions/networking, frankensqlite's store, atp's CAS federation) — unlocked the moment any crate manifest actually depends on them; (b) the `fln-wasm` crate — the WASM Judge needs only K1 + codec + `check-olean`, all bounded-live, and would create the project's first externally checkable artifact; (c) the `fln-bench` substrate — finished measurement machinery with zero consumers, unlocked by the first real measurement campaign. The Tribunal's differential rigs are a fourth: built for corpus scale, currently fed bounded fixtures.

4. **Benchmark honesty.** No number would survive an independent rerun because no number is claimed as a result: the README's gate table is explicitly `TARGETED`, with "0 bench targets, 0 committed baselines and 0 flame artifacts" stated verbatim [Maintainer claim, High]. The numbers load-bearing for the thesis are therefore not benchmarks but *absence-of-benchmark* honesty itself — the thesis currently rests on methodology and bounded slices, not measurements. The first honest measurement (any PG gate moving to `OBSERVED`) would be the single most informative event in the repo's history.

5. **The governance path.** There is no credible route from one maintainer to an institution under current policy: contributions are refused as a stated principle, the license bars the most likely institutional adopters from even benchmarking, and CI is red at the pin. What breaks first if velocity decays is the epoch ratchet — upstream Lean releases monthly, and each missed pin regeneration doubles the conformance debt across every `anchor:` line, census, and extracted contract simultaneously. The credible path would require, in order: green CI, a tagged release, a contribution policy, and a license exception or replacement for validation — each is currently refused or unattempted.

6. **The license as strategy.** The rider excludes OpenAI, Anthropic, their affiliates, and anyone acting for them — from *all* rights including "benchmarking, testing, analyzing, indexing" (quoted verbatim in §4.8). As strategy it is coherent only if the mission is expressive refusal rather than ecosystem impact: the named customers of the agent-era bets (frontier labs benchmarking reasoning models inside Lean) are precisely the excluded parties, and independent validation — the thing the project's trust story needs most — is legally barred from the validators most able to provide it. It serves the maintainer's stated desire for control ("it's my name on the thing"); it sabotages the stated mission of restructuring the Lean ecosystem's trust economics.

7. **Agent-era fit.** The concrete workload is proof-search at branch scale: thousands of tactic applications against forked proof states without the ~60 s/worker import tax — the README's own framing of what the 2026 literature hand-rolls per paper. What would have to become true first: `fln goals`/`serve-mcp` shipping (currently 1.0-target, not code), O(1) snapshots demonstrated on real (not bounded-slice) proof states, and a published branches-per-second measurement against the subprocess baseline (next-step #5). Until then, agents pick the Reference, because agents pick the thing that runs their project.

8. **The kill test.** Run the full mathlib corpus through the Tribunal's differential elaboration rig at the pin and count divergences — or, cheaper: green the main CI gate at a pin. Either event is decisive in both directions: a green gate with the corpus-differential lane passing would promote the ring; a divergence count in the thousands (or a gate that cannot be greened after a serious attempt) would confirm the bear case that the compatibility climb exceeds the project's structural capacity. A softer kill test: the next upstream epoch bump — if the `anchor:` machinery does not machine-flag the moved kernel lines before a human does, the methodology's flagship mechanism is ornament.