Archive — Open findings and the order to close them
Archive — not current documentation. Files in the last two groups describe the Seal family of research repositories or a past design state — they are kept for the record and are not claims about the Node CLI this repository ships.
Consolidated 2026-07-25; updated 2026-07-27. Everything currently known-broken
across seal-host, mcp-seal-dev and the shipped artifacts, in one place,
ranked.
Why ranked this way. The first tier is not the most severe. It is the tier that makes every other fix verifiable. Right now CI can pass while skipping the entire core, so anything closed below tier 1 is closed on trust. That is the exact failure this project keeps hitting: a control that exists but does not run. Fix the instruments first, then the defects they measure.
Status key: OPEN, IN PROGRESS, NEEDS BEN.
TIER 1 — make the signal trustworthy (front-load all of it)
Section titled “TIER 1 — make the signal trustworthy (front-load all of it)”Nothing below this line means anything until these land.
| # | Finding | Status |
|---|---|---|
| 1 | No release-evidence CI job. With SEAL_CI_READ_TOKEN absent, CI skips the Lean build, axiom checks, host unit tests, Rust conformance, the three-way differential, production startup conformance and the receipt demo, and still reports success. A missing secret must be RED, not a green skip. |
CLOSED 2026-07-25, job present in ci.yml |
| 2 | There are no external oracles at all. CORRECTED 2026-07-25. This row previously read “test/external/run.sh runs Wycheproof and JSONTestSuite but is manual”. That was false. The path does not exist and never has: a lane searched every branch, reflog, unreachable object and a fresh git fetch --prune origin, and test/external/ is absent from the tree. The gap is a full level worse than recorded. It is not a sound control left unwired, it is that no outside-authored evidence exists in this repository. Every corpus we test against, we wrote ourselves. Wycheproof and JSONTestSuite must be BUILT first, then gated, with a zero-vector-count floor so “ran, executed nothing” cannot pass. |
OPEN |
| 3 | Test/RepinStep2Guards.lean is in no lakefile target. The full Unicode-guard matrix is written and never executed. |
CLOSED 676c797. Wired to defaultTargets; ablating the NFD comparison in Host/UnicodeKeys.wireKeysSafe failed Test/RepinStep2Guards.lean:32 with “Tactic native_decide evaluated that to be false” |
| 4 | Proptest counterexamples are untracked. differential.proptest-regressions and parser_boundary.proptest-regressions hold shrunk failing seeds that a clean checkout discards. |
CLOSED 2026-07-25, both files tracked |
| 5 | PINS.md row 32 is factually stale (“18-field signed tuple”; the kernel is the ten-field v2 envelope) and pins_gate.mjs passed with it in place, because the gate checks structure and reachability, not currency. |
CLOSED 2026-07-26. Merged via 0fdef04; this row read FIXED, UNMERGED after the merge landed. Original note: 0b8f54a. Gate now parses the pinned kernel and compares field count, domain tag and declaration names; ablation reproduced. The 14 rows still checked shape-only are enumerated in that commit message |
| 22 | release/fleet-lock.json asserts a kernel hash that four of five fleet repos do not carry. Line 3 claims kernel_sha256: d7d81e27... across all five repositories. Fetched and hashed 2026-07-26 at exactly the lock’s own pinned commits: seal-check@bb5d572 a3790181, seal-verify-action@81077e5 a3790181, seal-demo@01da769 a3790181, seal-live-demo@b184d3d a3790181; only seal-assurance-kit@d5e14d1 matches. All five repo HEADs equal their lock-pinned commits, so this is the live serving state, not drift. Cause: merge 23f92d8 bumped kernel_sha256 without advancing the four repo commits. This is the project’s own defect class in its most load-bearing file: a document asserting a fact about the world that the world does not carry. Fix is a fork, not a typo: either advance the four repo commits to serve d7d81e27, or correct the lock to a3790181. Those are different truths. |
NEEDS BEN |
| 25 | The fleet lock records one kernel hash and five commits; the real kernel-identity footprint is 249 occurrences of 45 distinct hashes. Generated release/kernel-hash-footprint.json counts seal-verify-action 76, seal-live-demo 59, seal-check 57, seal-assurance-kit 46 and seal-demo 11, classified SIGNED 181 / STRING 62 / BINARY 6 / UNKNOWN 0. RUN kernel-hash-footprint-ablation-unlisted inserted an unmanifested occurrence and the gate named its repository, path, line, hash and classification. |
FIXED, UNMERGED at rebased tip e3ab1d1 on ci/kernel-hash-footprint; the branch adds the enumerator, generated manifest and --check gate. |
| 26 | seal-demo was fleet leg four and shipped the current wasm while six tracked text files still named the dead kernel. Before the repair, NOTICE, public/audit.js and public/seal-wasm.js carried the full a3790181... identity, while fixture provenance, its generator and the pathological-number test carried its short form; no tracked text named d7d81e27, but public/wasm/seal.wasm already hashed to d7d81e27.... |
CLOSED by pushed 2702b0a. All six references now name the live identity; fixtures were re-minted through scripts/regenerate-fixtures.cjs, and an independent rerun on pushed origin/main printed “fixtures regenerated” and left git diff empty. RUN seal-demo-leg4-local-2026-07-26 records 37/0 and old/current footprint 6/0 -> 0/6. |
| 27 | Merged main’s live Stage B differential would fail because CI never builds SealV2.EffectEnvelope. The workflow comment was already false: it said the live diff “stays #[ignore]d”, while rust/tests/envelope_v23_twin.rs has no ignore on live_lean_diff_over_shared_corpus. Neither lake build +Ffi:c.o.export nor the default-target lake build reaches SealV2.EffectEnvelope; the pinned package has 22 SealV2 source modules but the resulting tree had 9 oleans, with EffectEnvelope among the 13 missing. RUN twin-red-2026-07-26 on merged main 23c3c03 passed both frozen checks and failed only the live check with “SealV2/EffectEnvelope.olean … does not exist”, reproduced with Lake idle. |
FIXED, UNMERGED by explicit lake build SealV2.EffectEnvelope plus the corrected comment at f35368c on ci/build-effectenvelope. |
| 28 | A green build or rust-conformance job tick can mean only checkout plus a token-missing notice. In .github/workflows/ci.yml, every Lean build/test and Rust format/build/test/conformance step in those two jobs has if: SEAL_CI_READ_TOKEN != ''; with the token absent they skip deliberately. This is narrower than “only contract-freeze runs”: contract-freeze, cargo-audit and rust-sbom are ungated, and the always-running release-evidence job receives RELEASE_EVIDENCE_PRIVATE_TOKEN_CONFIGURED: false and is designed to make the overall run red. The misleading green is therefore at the two skipped job surfaces, not the release verdict. |
OPEN |
| 29 | seal-demo/public/audit.js excludes repository-pin identity from its own green light. allGood is exactly formatOk && shaMatch && reqMatch && bindingOk && signature_valid && kernel_replay_consistent; shaMatch correctly compares the live wasm hash with the hash inside the receipt, while ki.match compares that same live hash with the repo’s SEAL_WASM_SHA256, is surfaced only as kernel_identity.self_verified, and is absent from allGood. This is deliberate under the line-30 P-SELFAUDIT self-consistency claim and defensible—a kernel attesting to its own hash supplies no independent authority—but it means the demo’s green surface cannot catch pin drift. The six-file leg-four miss in row 26 is the observed consequence. |
OPEN |
TIER 2 — close the red suite
Section titled “TIER 2 — close the red suite”Suite is 105/5 after the guard-target merge. Three targets remain.
| # | Finding | Status |
|---|---|---|
| 6 | differential.rs and parser_boundary.rs assert a 0/1 classify contract. Classify now returns 2 (refuse) for duplicate object keys, duplicate method keys, oversized integers and a lone surrogate. The guards are correct; the tests encode the pre-fix contract. Fix WITH negative controls so refuse is asserted for the right inputs, not merely tolerated. |
CLOSED 2026-07-26. Merged via d573774, widened to 0/1/2 with refusals pinned; negative controls at 509a796. This row read OPEN for an unknown period after the fix landed. |
| 7 | The pinned seal.wasm predates the wire guards. three_way_agreement is red because native and model refuse unsafe-number cases while the pinned wasm passes them through or denies differently. Needs a repin. |
FIXED, UNMERGED f247c04 on chore/repin-wasm-row7, [[Ben]]-authorised 2026-07-26 01:32. Wasm d7d81e27 -> 70bee4b9. Three-way now 356/356; suite 114/0/2; ablation red reproduced and reverted. Merge still owed. |
TIER 3 — real defects with known fixes
Section titled “TIER 3 — real defects with known fixes”| # | Finding | Status |
|---|---|---|
| 8 | Interior NUL is claimed but untested. TCB.md and rust/src/lean.rs:37,111 claim the seam is interior-NUL safe. The only corpus entry (differential.rs:172) feeds \u0000 as a JSON ESCAPE, six characters on the wire. No test passes a literal 0x00 byte across the seam, which is the condition C-string truncation would exploit. Found by a blind GLM seat. |
CLOSED 24ade6d. rust/tests/nul_seam.rs distinguishes a full-length crossing from a truncated one by verdict; ablating to_lean_string to a strlen convention failed it with “assertion left == right failed, left: 0, right: 2” |
| 8b | This row itself contained a literal NUL byte until 2026-07-25. The sentence claiming the corpus feeds an ESCAPE rather than a raw byte contained a raw byte, so grep classified this entire findings ledger as a BINARY FILE and text tooling silently skipped it. Fixed by writing the escape as text. Recorded rather than quietly corrected, because a document that greps as binary is the same failure shape this ledger exists to track: an instrument that silently does not see something. |
CLOSED 2026-07-25 |
| 21 | Three distinct approval-signature failures collapse to one audit reason. In Ed25519TokenProvider::poll, a signature that is not valid hex, one that is well-formed hex but the wrong shape, and one that is well-formed and simply does not verify all record "bad_signature". An operator cannot distinguish a malformed client from a genuine failed verification. Same shape as row 18, in the approval path rather than the wire path. Pre-existing, NOT introduced by the 7a0235f extraction, but that extraction’s -> bool return makes it structurally harder to fix without changing the signature. |
OPEN |
| 9 | The shipped example config carries a signature nothing validates. config/trusted.example.json appears only in a schema gate; nothing verifies its signature. A user copying it cannot tell whether it is real. Either verify it somewhere or mark it explicitly illustrative. |
OPEN |
| 10 | production_startup_conformance.mjs and conformance_bridge.mjs still carry forbidden guarded targets. Found during the guard-target sweep, out of that brief’s file scope. |
LIKELY CLOSED 2026-07-26 via aa1d4dd/77b148b (“bind guarded targets to full arguments”); the named files were fixed on main. NOT semantically confirmed: nobody has audited that zero forbidden targets remain, which needs the conformance scripts run. Do not mark CLOSED until that runs. |
| 11 | The standalone seal binary still lacks the Unicode canonical-equivalence key guard that seal-host has. Needs the UnicodeBasic dependency in mcp-seal-dev. Recorded in the fix commit rather than silently left. |
OPEN |
| 12 | wireNumbersSafe measures parse cost, not cross-parser agreement. This row previously asked for an observed-safe exponent bound. That was the wrong remediation: the existing six-exponent-digit bound should remain as a DoS guard, while a separate agreement gate rejects literals that do not survive an IEEE-754 double round trip. Reproduced 2026-07-26: -1e9999, 1e999, 1e310 and 99999999999999999999 all return true from the live wireNumbersSafe; Node reads the first three as infinities and rounds the 20-digit integer to 100000000000000000000. |
SUPERSEDED BY ROW 34; the missing agreement control remains open there. |
| 24 | The 18 i_-class corpus divergences are CONSEQUENTIAL, not parser-view noise. Triaged by consequence 2026-07-26 (report ~/.mega-monkey/divergences-report.md); the earlier framing “parser-view divergence, not evidence of a mediation bypass” does not survive. Four are Rust Act / Lean Refuse (21 to 48 digit integers): Lean refuses before dispatch, audit, approval consumption or forwarding, so the deployed path fails closed. Fourteen are Rust NotAct / Lean Act: nine surrogate cases, 500 nested arrays via serde depth rejection, others. Rust’s serde rejects the line outright while Lean classifies it as Act. Digest verdict, verbatim: “no demonstrated host/kernel hash mismatch, but the fourteen Lean-act vectors leave approval bound to Lean’s semantic parse rather than to cross-parser agreement about the forwarded effect.” The approval target is computed ONLY by Lean from argsJson (Seal/Classify.lean:68, Seal/Hash.lean:41); Rust validates and transports the 64-hex value and never computes it, so two conflicting values cannot exist because only one exists. Cleared: arguments_sha256 and canonical_request_sha256 are receipt-only and omitted when serde cannot parse; request_sha256 over raw bytes survives; the V2.3 Rust effect projection fails closed (envelope_v23.rs:197). This is V3.1 stated precisely, and it names the experiment nobody has run: forward the exact bytes to each supported downstream MCP server and compare its extracted tool and arguments against Lean’s CanonicalAction. |
NEEDS BEN |
| 32 | Deploying flywheel-memory has no release rollback. Historical scripts/deploy-local.sh promised versioned releases, an atomic current symlink flip and symlink rollback while hardcoding absent /home/you/src/flywheel-memory and /home/you/flywheel/releases. The live user unit instead has WorkingDirectory=/home/you/src/flywheel-memory and runs packages/mcp-server/dist/index.js directly; /home/you/flywheel/releases and current are also absent. Recovery is checkout-last-good, rebuild, restart, with no ready previous release. The phantom script was deleted at flywheel-memory 29168a4; 12d49f9 documents the real build/verify/restart sequence and RUN flywheel-deploy-2026-07-26. |
OPEN |
| 34 | V3.1 now has a measured cross-parser disagreement and an accepted, unimplemented remediation. RUN v31run-2026-07-26 sent i_number_neg_int_huge_exp.json through the real approval/forward path: Lean signed external.json_corpus([-10^9999]) as an exact 10,000-digit integer while Node extracted external.json_corpus([-Infinity]). The untouched vector (92123944...), payload (2206dfa4...) and LF frame (a508b78a...) hashes independently recompute to the apparatus report, whose observer records the same frame hash. Node and Python independently parse [-1e9999] as negative infinity, confirming float coercion rather than a Node-only result. This is NOT a demonstrated unsafe act: the downstream application later rejected array-shaped arguments for an unrelated schema reason. Scope is one of 18 vectors; four are not approvable by Lean and the other 13 plus four of five observers remain untested. Apparatus is committed on seal-host d6cc012; remediation is ACCEPTED Option B in docs/NUMERIC-AGREEMENT.md (84325f4, 724d177): keep the cost gate and refuse before signing any numeric literal that does not survive a double round trip. |
OPEN |
| 35 | A false numeric receipt shipped on the public kernel, then was removed. At mcp-seal-dev bd03bf7, Seal/JsonUtil.lean:334-342 compared only the normalized, trailing-zero-stripped coefficient with maxSafeInteger and ignored parsed.exp10; RUN ledgerfold3-2026-07-27 built that public commit and printed (some true) for both 90071992547409910 and 999999999999999000, while Node’s exact binary64 integers are respectively 90071992547409904 and 999999999999998976 and Python preserves the wire integers. b83fdff constructs { coeff := coefficient, exp10 := parsed.exp10 } and checks exact binary64 equality (Seal/JsonUtil.lean:346-362). Independent run at that pushed commit: LITERALS_CHECKED=43, UNDER_REFUSALS=[], unchanged six-item OVER_REFUSALS, 0.1 and 1.5e3 ACCEPT, and lake build completed 423/423 jobs including v2_m4_axiom_check. |
CLOSED by pushed b83fdff |
| 36 | Nine separate surrogate denotations are still signed although downstream observers disagree. seal-host v31run/downstream-parser-agreement 5c90739 is unpushed and unavailable through GitHub, so the full five-observer matrix is UNVERIFIED INDEPENDENTLY. Saved Flywheel evidence evidence.nine-new-false-receipts-surrogate-class reports, verbatim, 9 REFUSED (eight numeric plus 500 nested arrays) and 9 FORWARDED where observers DISAGREE, all UTF-16-surrogate strings: the kernel signs ["�"]; GitHub, Patchright, Flywheel and the SQLite demo retain lone surrogate code units; Roundtable rejects with "Invalid JSON: lone leading surrogate in hex escape". The kernel/downstream shape is independently reproduced by RUN ledgerfold3-2026-07-27: Lean Json.parse prints ["�"], ["�"], ["��"] for \ud800, \udada, and inverted \udd1e\ud834, while Node and Python print code units d800, dada, and dd1e d834. Thus the reported nine combine value divergence with acceptance divergence; the named four-observer/Roundtable counts remain the unverified part. |
OPEN |
| 37 | The surrogate class is unrepresentable in the kernel’s value type, not merely mis-parsed. In the pinned Lean 4.28.0 core, Init/Prelude.lean:2794-2795 defines Nat.isValidChar to exclude 0xd800–0xdfff; Char carries valid : val.isValidChar at lines 2807-2811; and String is a sequence of Unicode scalar values backed by valid UTF-8 at lines 3468-3481. RUN ledgerfold3-2026-07-27 independently showed Node and Python retaining lone surrogate code units while Lean can produce only replacement Chars. No Lean parser work can make String denote a lone surrogate: the type excludes it. For this class the kernel cannot honestly sign a value denotation; it must refuse the input or bind only to bytes under an explicitly narrower claim. |
OPEN |
TIER 4 — harvest work that already exists
Section titled “TIER 4 — harvest work that already exists”Frisk branches before harvesting them; do not rewrite their work from scratch. Rows 13 and 14 are now resolved, leaving the decisions in rows 15 and 23.
| # | Finding | Status |
|---|---|---|
| 13 | feat/field-warrant (mcp-seal-dev, 46 behind / 3 ahead) carries the expiry, issuedAt-freshness, policy-version and delegation-membership gates. |
SUPERSEDED 2026-07-26; recommend branch deletion. Main contains 4f39f20 (ported SHOW suite) and 77380fe (negative-witness harness). Reproduced from Git objects: SealV2/EnvelopeCompleteness.lean is 135 lines on main vs 137 on the branch, Test/FieldWarrant.lean is 335 vs 221, and git diff main feat/field-warrant over those two files is 185 insertions / 297 deletions. Merging the branch would remove net test surface. |
| 14 | feat/envelope-stageB-twin carried the seal.effect/v2 encoder work and un-ignored the live differential after Ben ruled “host follows kernel to v2”. |
CLOSED 2026-07-26, merged into seal-host local main as 23c3c03 with Ben’s approval; the merge is not pushed (main is 61 commits ahead of origin/main). Harvest evidence: final suite 121/0/1, Lean build 16239 jobs, PINS.md:46 true, and ABLATION-RUN-STAGEB-LIVE-001 failed on the mutated golden-fable byte then passed after revert. A post-merge run did show one red: the live twin could not find SealV2/EffectEnvelope.olean. Row 27 reproduces that environmental build-coverage defect; it is not an encoder-merge defect. |
| 15 | feat/v2.1-principal: this row said 114 behind in seal-host. THE BRANCH NO LONGER EXISTS THERE, local or origin, as checked 2026-07-26. The mcp-seal-dev copy survives at origin, 53 behind / 1 ahead, so that half was accurate. Proposed: abandon the survivor. |
NEEDS BEN |
| 23 | feat/passthrough-perimeter: DO NOT MERGE. The branch’s valuable scope correction still stands: deployedAdapter becomes gatedSinkAdapter, honestly limited to two of nine transitions (P2 forward and P3 retry), excluding P1 and P4-P9. But its central perimeter theorem chain is not integration-ready. Applied to current main, a clean focused elaboration fails all three claimed router correspondences—classifyLine_refuse_iff, classifyLine_act_iff, classifyLine_passthrough_iff—because the branch predicates omit the live Seal.JsonUtil.wireKeysSafe, Host.UnicodeKeys.wireKeysSafe and Seal.JsonUtil.wireDigitsSafe gates; the failures introduce sorryAx, then 13 inline #guard_msgs pins reject the contaminated chain. Independent RUN ledgerfold2-k4-2026-07-26 reproduced the genuine compile red in 7.38 seconds and 784444 KiB RSS. The first perimcond verdict was not probative: its follow-up work order records a seven-hour build OOM-killed at the old 7G cap and every cargo target failing because libsealffi.so was absent. Probe sensitivity remains UNPROVEN. UNVERIFIED from surviving local artifacts: the supplied follow-up summary says baseline, mutated and post-revert builds all died before Test.PerimeterProbe; no independent RED or GREEN transcript was found. |
DO NOT MERGE |
TIER 5 — specification and honesty defects
Section titled “TIER 5 — specification and honesty defects”Real, none of them a live bypass.
| # | Finding | Status |
|---|---|---|
| 16 | ValidApproval is weaker than its name. It carries target, session, unconsumed, unexpired and signature validity, but NOT ttlWithinCap, NOT !nonceConsumed, and no equation approvalLiveFor ... = true. The type can be constructed without proving everything that made the approval live. Not a runtime bypass (the runtime goes through findApproval). |
OPEN |
| 17 | serializeTargetKey is not injective. It joins arbitrary strings with NUL separators, so tool="a\0b", action="c" collides with tool="a", action="b\0c". Fail-closed (extra replay rejection), so denial rather than approval transfer, but the injectivity claim is false. Fix with a structured ReplayTargetKey, not another framed string. |
OPEN |
| 18 | Every refusal reports “unsafe numeric literal” although the branch now covers pathological exponents, duplicate keys, Unicode-equivalent duplicate keys and excessive significant digits. The audit record needs the correct reason even if the wire response stays generic. | OPEN |
| 19 | METHOD.md section 4 says “a finding that is already documented is not a finding.” That doctrine is dangerous as worded and was mis-applied on 2026-07-25 to downgrade a real defect. Correct form: it is not a NEW finding, but it must still be assessed against the current claim and release threshold. |
OPEN |
| 20 | PINS.md and DECISIONS.md are hand-maintained and drift immediately. Load-bearing facts: declaration names, dependency SHAs, domain tags, field counts, test target names, whether each named test is actually reached. FIX RESHAPED 2026-07-26. This row previously proposed generating the markdown from machine-readable data. That is the wrong shape: it discards the prose and the reasoning, which is most of what these documents are for. The right shape is partial generation, taken from leCore (AnOversizedMooseWithSocks/leCore, MIT), which ships it: the prose stays hand-written and untouched, while the load-bearing TABLE inside it is regenerated and diffed against the live code, and CI fails naming the offending row rather than rewriting the document. Three companion mechanisms from the same repo, in descending order of value to us: (a) a meta-test cross-referencing the generator list against the CI gate list, so a gate with no generator or a generator with no gate is a test failure, which is the check-the-checker layer this project keeps rediscovering it needs; (b) one door, a single importable module holding the canonical generator list with an --outputs flag, so no workflow ever repeats the list and a missing generator fails loudly instead of being skipped (their recorded cause: six copy-pasted CI steps, one forgotten at close-out); (c) an import audit resolving every import against what is actually on disk via ast, catching imports that pass by accident, which is our own green-measuring-the-wrong-thing class found independently. NOT YET FRISKED: read against their source before building; the above is from their CI step comments. |
OPEN |
| 30 | A green default seal-host build does not compile the full kernel theorem surface it depends on for assurance. This is normal Lake reachability, not a compiler defect: default targets build only imported modules. At the manifest-pinned mcp-seal 6c74b61, 22 SealV2/*.lean modules exist but only 9 corresponding oleans were present after the normal build. The 13 absent modules were ClassifyTransport, EffectEnvelope, EnvelopeCompleteness, LifecycleTheorems, NonceLedger, ParserTheorems, PrincipalNonInfluence, ResponseNI, ResponseTransport, SerializationContainerLemmas, SerializationLemmas, SerializationTheorems and ValidationTheorems; DecideTheorems and TamperTheorems were among the nine that did build. The assurance map must say which theorem surfaces CI compiles rather than treating a green host build as evidence for all 22. |
OPEN |
| 31 | A security-sensitive lane brief falsely attributed permissive behavior to the frozen V2.3 corpus. The alleged corpus sentence—leftover v1 keys “are simply not consulted” because they are unsigned—does not exist in the current file, any local or remote ref, or any reflog-reachable or unreachable commit searched on 2026-07-26. The frozen corpus actually says killed fields are stripped and a vector carrying one is a corpus bug; EnvelopeV23 plus its three nested claims all use #[serde(deny_unknown_fields)], wire_view returns Malformed, and killed_field_in_wire_envelope_fails_closed covers the retired fields. The contract gate independently reports all seven reviewed digests green. The rejection behavior is real; the false claim was in the evidence chain, not the fixture. |
CORRECTED HERE |
| 33 | K4’s “EXACTLY” claim is false at the integration point. feat/passthrough-perimeter:CLAIMS.md says Host.classifyLine realizes refusedClass, inPerimeter and escapes exactly via three _iff proofs. Its predicates and proofs case-split only on wireNumbersSafe; current main’s classifier also refuses on byte-duplicate keys, Unicode-equivalent keys and excessive significant digits. RUN ledgerfold2-k4-2026-07-26 compiled the branch’s K4 module against current main in a disposable tree: all three named proofs failed with unsolved goals requiring precisely Seal.JsonUtil.wireKeysSafe, Host.UnicodeKeys.wireKeysSafe and Seal.JsonUtil.wireDigitsSafe, and their printed axiom footprints gained sorryAx. Main itself does not carry the K4 row or proofs; the failure is the branch-on-main integration truth. |
OPEN |
| 38 | The integer agreement rule is decided partly by spelling, not solely by magnitude or reader agreement. This is a coherence defect, not a safety defect. RUN ledgerfold3-2026-07-27 at public kernel b83fdff printed 100000000000000000 ACCEPT and 9007199254740992 REFUSE; Node and Python agree exactly on both, and both exceed 2^53-1. The operative difference is normalization: trailing zeroes move into exp10 before the coefficient check at Seal/JsonUtil.lean:346-362. Correction to the overnight warning: docs/NUMERIC-AGREEMENT.md no longer states a plain magnitude rule; current lines 94-147 already name this exact defect, its six preserved over-refusals, and the alternative of dropping the coefficient conjunct. The ledger, not that spec, was stale. |
NEEDS BEN on the rule choice |
| 39 | Ed25519 scalar-range rejection is tested, but its production ownership and dependency configuration remain implicit. The overnight claim that there was “no test anywhere” and that feature unification could change acceptance silently is false. seal-host main has ed25519-dalek = "3" with implicit defaults (rust/Cargo.toml:9) and calls plain .verify() (rust/src/envelope_v23.rs:281-286); dalek 3.0.0 selects Scalar::from_canonical_bytes unless legacy_compatibility is enabled (ed25519-dalek-3.0.0/src/signature.rs:68-90). But 7a0235f already pinned a 150-vector Wycheproof corpus: its SignatureMalleability note explicitly names failure to range-check S (rust/tests/corpora/Wycheproof/ed25519_test.json:32-35), and rust/tests/wycheproof_ed25519.rs:94,164-173 sends every invalid vector through the production helper and asserts rejection. RUN ledgerfold3-2026-07-27 passed 150/150 normally and, with ed25519-dalek/legacy_compatibility, failed exactly at tcId=63 ... flags=["SignatureMalleability"] ... seal=verified; the suite would signal the feature-unification change. The narrower open item is explicit ownership: exact pin, declared features, owned S < L check and distinct error class. Reported repair 44af185 on fix/own-scalar-range is UNVERIFIED because the unpushed commit is unavailable without entering the frozen tree; Flywheel evidence evidence.scalar-range-now-owned-44af185 says it adds those controls and two path tests. |
OPEN |
| 40 | A JavaScript approval renderer is a latent parser-agreement boundary. RUN ledgerfold3-2026-07-27 parsed wire integer 1234567890123456789 in Node and printed JSON.stringify=1234567890123456800, toFixed(0)=1234567890123456768, while Python retained 1234567890123456789: a JS renderer can show a human a different integer from the approved bytes. This is LATENT, NOT LIVE today. A read-only seal-host main clone contains only wasm-spike/browser_smoke.html and wasm-spike/verified/seal.js, neither an approval surface; the live approval UI is the terminal digest prompt "seal-host: approve target {target}? [y/N]" at rust/src/providers.rs:523-534. The defect becomes live when a GUI or demo renders decoded request values for approval; at that point the renderer must join the conformance corpus as another parser. |
OPEN |
| 41 | The contract freeze gate protects the envelope contract, not the authorization-record contract, while reading as though it protects the signed shape. Measured 2026-07-27 10:40 on disk in seal-host worktree /home/you/wt/rename at 7c83191. scripts/contract_freeze_gate.py:54-69 sets REQUIRED_FROZEN_FILES to seven envelope_v23 paths plus every tracked file under rust/tests/vectors. rust/src/authorization_decision.rs and docs/AUTHORIZATION-DECISION-SCHEMA.md are absent from it. Consequence, observed rather than reasoned: 7c83191 changed the record’s on-wire version discriminator from "seal_receipt": "v2" to "record_type" + "record_version", no verifier in the tree accepts the legacy key, stored artifacts under demo/out/ carrying "seal_receipt": "v2" no longer validate, and the gate said nothing. Ruled by [[Ben]] 2026-07-27 10:41: the four-leg record shape SHOULD enter the frozen set. |
RULED, NOT YET IMPLEMENTED |
| 42 | The freeze gate hashes whole files, so prose burns the human ceremony. Same run as row 41. python3 scripts/contract_freeze_gate.py exits 1 naming docs/EFFECT-ENVELOPE-V23.md, rust/src/envelope_v23.rs and rust/tests/envelope_v23.rs, and the entire diff of all three against main is commentary: two comment lines, three more comment lines, and one test-function rename. Not one wire byte moved. Taken with row 41 the pair is the serious shape: the second key, which exists precisely so an automated agent cannot approve its own contract change, is spent on comments while a real signed-shape change rides free. A ceremony performed for cosmetics becomes reflex, and reflex is the failure mode that key exists to prevent. This is [[green-measuring-the-wrong-thing]] wearing a red light instead of a green one. Ruled by [[Ben]] 2026-07-27 10:41: the gate should hash contract REGIONS rather than whole files. Evidence bar before this counts as done: a prose-only edit inside a frozen file must leave the gate green, AND a wire-byte edit in the same file must still turn it red. Without the second half the fix is indistinguishable from weakening the gate. |
CLOSED by seal-host f2f0b8e |
| 43 | LEGACY_CONTRACT_VIEWS widens the human-key surface from one table to two, and must not become permanent. Introduced by seal-host f2f0b8e while closing row 42, so the move to view-based hashing did not force a re-approval of all seven digests for a change that moved no contract bytes. Its own comment claims it “cannot name an alternative accepted output”, and that claim is true as written: the logic is if legacy is not None and digest == legacy: return REVIEWED_HASHES[relative], so the returned digest is always the human-approved one and the table’s values are used only in an equality test. The precise residual risk is different: it can name an alternative accepted INPUT. Any file content whose contract view digests to a legacy entry receives the approved answer, so editing a legacy value by hand to the view digest of a doctored file would pass that file. This is not a new class of hole, it is the same trust as REVIEWED_HASHES itself, which --refreeze also cannot write and a human edit can. But two hand-maintained approval tables are harder to reason about than one. ACTION: delete LEGACY_CONTRACT_VIEWS at the next real contract re-approval, when those entries become dead weight anyway, returning the human-key surface to a single table. Recorded so it does not quietly become permanent. |
OPEN |
What I would front-load if it were my call
Section titled “What I would front-load if it were my call”Tier 1, entirely, before anything else. Specifically item 1. Until a missing secret turns CI red, every green is unfalsifiable and we are grading our own homework. It is also the cheapest item on this page.
Then tier 2, because a red suite hides new regressions in the noise.
Then item 8 (interior NUL) out of order, ahead of the rest of tier 3, because it is a CLAIMED hardening property with no test, it was found from outside by a seat that knew nothing about our other findings, and it is small.
Tier 4 before tier 5: harvesting existing work beats writing new work. Rows 13 and 14 are now resolved; rows 15 and 23 still need decisions.
Tier 5 last, deliberately. All real, none urgent, and item 19 is the one I would do first within that tier because a wrong doctrine keeps generating wrong calls.