Find evidence for a fak correctness claim
Audience: an evaluator checking whether a specific fak correctness claim has a repeatable witness and a current verdict.
Next action: find the subsystem in the claim index below, open its proof page, and run
the witness command printed beside its verdict. Start with
preflight.md when evaluating structural policy denial, or
adjudicator.md when evaluating the model-backed decision path.
This is the current math-correctness ledger. It routes by claim and witness type so an
evaluator can reach evidence directly; design history and contributor rationale remain in
the individual proof pages and 00-METHOD.md.
Choose the evidence you need
| Claim to evaluate | Proof route | Witness type |
|---|---|---|
| A disallowed tool call is denied before model execution | preflight.md |
Deterministic behavioral test |
| The model-backed decision path returns a bounded verdict | adjudicator.md |
Deterministic decision-procedure test |
| Policy parsing and matching preserve the declared capability boundary | policy.md |
Deterministic structural and behavioral tests |
| Canonical bytes and digests are stable | canon.md and blob.md |
Golden-vector / integrity tests |
| Context compaction and restoration preserve required state | ctxmmu.md, contextq.md, and sound-restore.md |
Invariant and round-trip tests |
| Model math matches the reference implementation | model-forward-parity.md and the numerical rows in the master ledger |
Numerical parity tests |
| A compute-HAL GEMM preserves the canonical reduction contract | compute-gemm.md |
Deterministic delegation and reduction-order tests |
| The supported Apple Metal GEMM path matches its CPU reference | metalgemm.md |
Metal hardware-backed numerical witness |
| A shipped proof is bound to repository history | witness.md and the DOS binding section |
Independent git-evidence witness |
| A benchmark comparison isolates the claimed effect | bench-ab-isolation.md and isolation-bench.md |
Controlled A/B measurement |
| Every guard, adjudication rung, and hook declares its failure mode | failclosed-audit.md |
Enumerated coverage ledger + drift gate |
If the claim is not in this short route table, use the master ledger, which groups every maintained proof by numerical, structural, integrity, and decision-procedure obligation.
Current authority and support
| Context | Current contract |
|---|---|
| Mode | Proof index and reproducible witness commands; it does not replace runtime policy or operational guidance. |
| Generation | Current gen/now ledger. Each proof page names the implementation surface and command it covers. |
| Lifecycle | Ledger verdicts are PROVEN, REFUTED, OPEN, or SCOPED-OUT. Companion packets may use provenance labels such as DEMONSTRATED, WITNESSED, OBSERVED, or MODELED; those labels describe evidence origin and do not upgrade a ledger verdict. The command and current repository state decide whether a result still reproduces. |
| Support | Maintained proof pages and checked-in fixtures are supported evaluator evidence. Dated notes and design history are context, not current verdict authority. |
Every module earns a verdict through the same chain: a precise theorem, a mathematical
argument, a deterministic or hardware-backed witness, a live verdict, and a DOS binding
that grounds “shipped” in git evidence rather than author narration. Read
00-METHOD.md for the regime taxonomy, honesty rules, and reproduction
method before extending or auditing the ledger itself.
How to read a verdict
A PROVEN here means: the proof page names a reproducible witness; that witness ran green
in the recorded proof build; the result corroborates the theorem within the page’s stated platform and model scope; and the commit that shipped it is diff-witnessed by
dos commit-audit. Most witnesses are deterministic go test targets; hardware proofs name
the required backend and device. An
OPEN means the theorem is stated but no deterministic witness discharges it yet — the
file says which witness would. A REFUTED is a recorded finding with its counterexample,
not a deletion. Nothing is PROVEN by prose.
Master ledger
Verdicts are filled from actual test runs during the proof build, not asserted. Regime: N numerical · A algebraic/structural · C crypto/integrity · D decision-procedure.
Witnessnames the load-bearing test(s); the per-module doc carries the exact-runtarget andfile:line.
Generated snapshot from the per-module proof files: 94 PROVEN · 2 OPEN · 1 REFUTED · 1 SCOPED-OUT across 98 theorem rows / 40 obligations. The recorded proof build ran go test -count=1 on darwin/arm64 with Go 1.26 and cross-checked 45 ./internal/... packages (0 failures). This is historical execution provenance, not a claim that every row was rerun at the current checkout: reproduce a claim with the exact command on its proof page. Commit 3cb8ff9 closed 25 earlier OPEN rows; the two rows still marked OPEN below remain open. The REFUTED N7 row records Qwen3.6 token-3 decode drift rather than deleting the counterexample (00-METHOD §4). Read each theorem row independently; an obligation heading or roster summary does not broaden a row’s model, token-count, or backend scope.
N — Numerical / linear-algebra
| Obl | Module | Theorem | Witness | Verdict |
|---|---|---|---|---|
| N1 | model/attention | For any finite score vector x, softmaxInPlace(x) yields entries y_i >= 0 with sum_i y_i = 1 (row-stochastic), and soft | TestProofSoftmaxRowStochasticAndShiftInvariant |
✅ PROVEN |
| ↳ | The dense scaled-dot-product attention weight matrix is strictly lower-triangular: query position i receives zero weig | TestProofCausalStrictlyLowerTriangular |
✅ PROVEN | |
| ↳ | When a learned per-head sink logit is present, softmaxDropSinkInPlace includes it in the softmax denominator but exclu | TestAttentionSinkSoftmaxDropsSink |
✅ PROVEN | |
| N2 | model/norm | For all x,w of equal length and eps>0, rmsnorm(x,w,eps)[i] == x[i] * w[i] / sqrt(mean(x^2)+eps) within 1e-6 (plain pat | TestNormGain1p |
✅ PROVEN |
| ↳ | For all x,w,bias of equal length and eps>0, layernorm(x,w,bias,eps)[i] == (x[i]-mean)*w[i]/sqrt(var+eps) + bias[i] wit | TestLayerNormAxis |
✅ PROVEN | |
| ↳ | LayerNorm is invariant to affine input transforms on the normalized axis: for a>0,b, layernorm(a*x+b, w, bias, eps’)[i | TestProofLayerNormShiftScaleEquivariant, TestProofRMSNormPositiveScaleInvariant |
✅ PROVEN | |
| ↳ | For large-magnitude finite inputs (e.g. |x| ~ 1e15..1e20), rmsnorm/layernorm produce only finite outputs (no NaN, no | TestProofNormNumericallyStableLargeInputs |
✅ PROVEN | |
| N3 | model/rope | For the unscaled (Llama) rotary map, applyRopeRow acts on each pair (h[j], h[j+half]) as a Givens rotation by angle p· | TestProofRopePreservesPairNorm |
✅ PROVEN |
| ↳ | For unscaled RoPE, the dot product of a query rotated at position m with a key rotated at position n equals the dot pr | TestProofRopeDotRelativePosition |
✅ PROVEN | |
| ↳ | The implemented RoPE scaling variants rescale inv_freq / cos·sin per their reference formula: llama3 piecewise low/hig | TestRopeScalingLlama3, TestYarnRopeScalesCosSin … |
✅ PROVEN | |
| N4 | model/mlp+residual | For every layer and every normalized input x, the dense MLP delta equals down_proj( act(gate_proj(x)) * up_proj(x) ) e | TestMoEDenseNoOpIdentical, TestDenseActivationMLPWithBias |
✅ PROVEN |
| ↳ | The residual stream update is exact elementwise addition of the sub-layer delta into the stream — x += body(norm(x)) f | TestBlockTopologyComposition, TestSandwichNormUsesDistinctFeedForwardNorms |
✅ PROVEN | |
| ↳ | MoE routing computes logits=router(x), probs=softmax over ALL experts, selects the top-k experts by prob (torch.topk s | TestMoERoutingHandComputed, TestMoEWiring … |
✅ PROVEN | |
| N5 | model/quant | For every Q4_K super-block, q4kDequantSuperBlock reproduces value = dsc_snibble - min*m_s (the affine per-sub-block | TestQ4KDequantSuperBlockMatchesRef, TestQ4KMatRowsMatchesF32 … |
✅ PROVEN |
| ↳ | AWQ dequant weight[oin+i] = scale[o](unpack4bit(code) - 8) matches its reference: (a) the affine arithmetic is bit-e | TestProofAWQMatchesReference |
✅ PROVEN | |
| ↳ | The arch-dispatched integer reduction q4kReduceRow (NEON SDOT on arm64) produces the per-sub-block int32 pairs IS=sum( | TestQ4KReduceAsmMatchesScalar, TestQ4KInt8DotMatchesF32 |
✅ PROVEN | |
| N6 | model/kv | Per-position K/V written during a decoder block lands in the correct (layer, position, head) slot of the kernel-owned | TestStandardLayoutNoOp, TestSWAWindowUnsetIsNoOp … |
✅ PROVEN |
| ↳ | KVCache.Evict(from,n) removes a contiguous position span from every layer and re-rotates each survivor’s post-RoPE K t | TestKVQuarantineEqualsNeverSaw, TestEvictRepositionsWithLayerSpecificRopeTheta |
✅ PROVEN | |
| ↳ | Sliding-window attention masks EXACTLY the out-of-window positions — query at absolute position p attends only keys wi | TestSWAWindowMasksOldKeys, TestSWAWindowUnsetIsNoOp … |
✅ PROVEN | |
| N7 | model/forward-parity | For the loaded HF oracle (smollm2-135m, model_type=llama), the pure-Go Forward pass reproduces HF’s per-layer hidden s | TestForwardMatchesHFOracle, TestForwardMatchesHFOracle/smollm2-135m |
✅ PROVEN |
| ↳ | Generate(prompt.Ids, n) on weights Go-decoded directly from raw safetensors (no torch in the load path) reproduces HF’ | TestForwardOnGoDecodedWeights |
✅ PROVEN | |
| ↳ | The forward-pass HF-oracle parity (hidden cosine≈1, per-position argmax, greedy ids) holds not only for llama but acro | TestOptionalQwen3OracleCoversQKNorm, TestOptionalQwen3MoEOracleCoversHybridDenseSparseLayers … |
🔸 OPEN | |
| ↳ | Qwen3.6 (hybrid Gated-DeltaNet) in-kernel greedy decode reproduces the llama.cpp reference token-for-token on the same q4_k_m GGUF — token-3 drift: fak/oracle agree on tokens 0–1 then diverge at token 2 (fak 8160 vs oracle 90700, a near-tie argmax flip; first-token parity holds) |
cmd/qwen35check + captured oracle artifact pair (experiments/qwen36/*multitoken*) |
❌ REFUTED | |
| N8 | compute/gemm | For w[out,in], x[in], the HAL F32 MatMul/BatchedMatMul computes y[o]=Σ_i w[o,i]·x[i] equal to the package’s canonical | TestMatMulDelegatesVerbatim, TestReductionOrderIsTheModelTree |
✅ PROVEN |
| ↳ | GEMM is bilinear: A(B+C) = AB + AC and (αA)B = α(AB), checked against the naive computation up to float tolerance (the | TestGEMMBilinear |
✅ PROVEN | |
| ↳ | Every registered backend (CPU / Metal / CUDA / Vulkan, by build tag) agrees with the CPU Reference: an Approx backend’ | TestQ8DispatchIsApproxAndGated, TestCorrectnessClassEnforcement … |
⚪ SCOPED-OUT | |
| N9 | metalgemm | For random W[out,in] and X[P,in], the Metal f16 GEMM Y=X·Wᵀ (MPSMatrixMultiplication / runtime-compiled MSL) equals th | TestMatMulMatchesReference, TestResetReclaimsTable … |
✅ PROVEN |
| ↳ | The stub (default) build and the metal build of package metalgemm present the same exported interface, and the stub in | TestStubInterfaceParity_CompilesAndScalarContract |
✅ PROVEN | |
| N10 | tokenizer | For text x drawn from the lossless ByteLevel domain, Decode(Encode(x)) == x byte-identically; and for any id list, Dec | TestEncodeSmallByteLevelBPEFixture, TestOptionalSmolLM2EncodeMatchesHFCorpus … |
✅ PROVEN |
| ↳ | BPE merges apply in deterministic merge-rank order: at each step the adjacent symbol pair with the SMALLEST tokenizer. | TestEncodeSmallByteLevelBPEFixture, TestOptionalSmolLM2EncodeMatchesHFCorpus … |
✅ PROVEN | |
| ↳ | Tokenization matches the independent HuggingFace / llama.cpp reference: Encode(text) equals the reference token ids by | TestQwenOracleGolden, TestOptionalQwen36ChatMLPromptMatchesLlamaCpp … |
✅ PROVEN | |
| N11 | ggufload | For every tensor in a parsed GGUF, FileOffset = align(headerEnd) + declared Offset (with Offset required to be alignme | TestReadParsesMetadataTensorDirectoryAndConfig, TestWeightSourceReadsAndDequantizesSimpleTensors |
✅ PROVEN |
| ↳ | For each supported dtype (F32, F16, BF16, Q8_0, Q4_K, Q6_K, Q5_0, Q5_1, Q5_K, Q2_K, Q3_K), dequantF32 reads the correc | TestWeightSourceReadsAndDequantizesSimpleTensors |
✅ PROVEN | |
| ↳ | Parsing GGUF metadata is consistent with the encoding: for every metadata value type (string, uint8/16/32/64, int8/16/ | TestReadParsesMetadataTensorDirectoryAndConfig, TestReadRejectsBadAlignmentAndBool |
✅ PROVEN |
A — Algebraic / structural
| Obl | Module | Theorem | Witness | Verdict |
|---|---|---|---|---|
| A1 | radixkv | For any new request whose token sequence shares a prefix with a cached sequence, the tree discovers the LONGEST cached | TestReuseThroughSplitMatchesRecompute, TestFewShotHitRate … |
✅ PROVEN |
| ↳ | Reference counts are conserved: insert/clone(split)/evict leave no dangling node (a removed node is unreachable, never | TestRefcountConservationCycleNetsZero, TestRemovedNodeUnreachableNeverMatched |
✅ PROVEN | |
| ↳ | Under a token budget (maxTokens>0), when tokens exceed budget the tree evicts the least-recently-used unlocked LEAF (a | TestLRUEvictsOldestRetainsHotAndLeased, TestLRUUpwardCollapse |
✅ PROVEN | |
| A2 | kvmmu | For any sequence of segment appends and span evictions, the mapping from live logical positions to physical KV cache s | TestLedgerRenumberAfterMiddleEvict, TestWriteTimeEvictEqualsNeverSaw |
✅ PROVEN |
| ↳ | A named span maps to exactly its bytes: evicting segment by logical id removes exactly its recorded [From,From+Len) ca | TestLedgerRenumberAfterMiddleEvict, TestEvictionIsContentDrivenNotPositional … |
✅ PROVEN | |
| A3 | cachemeta | For a fixed Entry’s binding axes, the cache key (ManifestBindingDigest / AttentionIndexBindingDigest) is a determinist | TestManifestBindingDigestIsDeterministicOverBindingAxes, TestAttentionIndexDigestIncludesIndexShareLayerSet |
✅ PROVEN |
| ↳ | Lowering an event into an Entry and reading it back preserves the binding: FromKVTransfer->KVTransferVerdict recovers | TestFromKVTransferRecordsResidencyTransition, TestKVTransferRestoreFaultIsTypedNotSilent … |
✅ PROVEN | |
| ↳ | Collision and eviction are well-defined: distinct bindings produce distinct digests (no false hit), a lookup whose axe | TestAttentionIndexLookupRequiresPrefixDecisionAndCausality, TestCheckResidentClaimRefusesBindingMismatch … |
✅ PROVEN | |
| A4 | recall | For a completed session persisted as a core image, a query against the reloaded session returns the SAME answer as rep | TestBenignPageRoundTripsByteIdentical, TestSessionIsSelfContained … |
✅ PROVEN |
| ↳ | Recall is deterministic and input-driven: for fixed (loaded session, query, k) the assembled working set — its members | TestRecallIsDeterministicAcrossRepeatedCalls, TestRecallIsIdenticalAcrossIndependentReloads, TestRecallDependsOnlyOnQueryAndK, TestRecallWorkingSetNeverContainsQuarantinedBytes |
✅ PROVEN | |
| A5 | contextq | On-demand materialization (contextq.Query) reconstructs a context byte-identical to the original CDB image: every mate | TestMaterializeByteIdentical |
✅ PROVEN |
| ↳ | contextq.Query is deterministic: for a fixed CDB image and a fixed Request, repeated calls produce an equal Result (sa | TestMaterializationDeterministic |
✅ PROVEN | |
| A6 | blob | For every payload b, Resolve(Put(b)) returns bytes byte-identical to b — for both the inline path (len(b) <= InlineMax | TestPutSmallInlineRoundTrip, TestPutLargeBlobRoundTrip … |
✅ PROVEN |
| ↳ | Two Puts of byte-identical content (even from distinct backing arrays) produce the same digest (the address IS the sha | TestContentDedup, TestDefaultStoreViaABI |
✅ PROVEN | |
| A7 | preflight | For every ToolCall, the preflight ladder evaluates rung 0 (static JSON parse) strictly before rung 1 (schema validatio | TestRung0FailureNeverReachesRung1, TestNegativesRowFields |
✅ PROVEN |
| ↳ | A Deny at a cheaper rung short-circuits all more-expensive rungs: when rung 0 denies, rung 1 (JSON-Schema validation) | TestRung0FailureNeverReachesRung1 |
✅ PROVEN | |
| A8 | abi+architest | Every internal package that folds a verdict chain most-restrictive-wins (kernel, kvmmu, recall, agent) orders that fol | TestFoldSitesOrderByFoldRank, TestFoldRankOrdering |
✅ PROVEN |
| ↳ | The internal package graph is a layered DAG: Go forbids import cycles (acyclicity), and the architest tier rule forbid | TestNoUpwardImports, TestHotPathHasNoExec … |
✅ PROVEN | |
| ↳ | The closed-enum wire contract of the frozen wave-0 ABI (VerdictKind, Status, Outcome, TaintLabel, ShareScope, RefKind, | TestABIGoldenFreeze, TestClosedReasonVocabulary |
✅ PROVEN | |
| I1 | engine-seam | For a fixed registered engine, EngineDriver.Complete is deterministic in (tool, args): the same request yields the sam | TestDecodeIsDeterministicAndInputDriven, TestCompleteRunsRealDecode … |
✅ PROVEN |
| ↳ | An external invalidation directive set is bound to the correct documented engine reset endpoint and never silently ser | TestInvalidateSGLangFlushesRadixCache, TestInvalidateVLLMResetsPrefixCache … |
✅ PROVEN | |
| ↳ | After Invalidate succeeds against a live serving engine, a subsequent request for the invalidated prefix/span observes | TestEndToEndNotServedStaleSGLang |
✅ PROVEN | |
| I2 | bench-ab-isolation | An A/B ablation is a PAIRED replay over the SAME seed/trace: each arm runs the identical call sequence through one fre | TestFanoutDeterministic, TestStochastic_Determinism … |
✅ PROVEN |
| ↳ | The turn-tax isolation attributes the measured A/B delta to the TOGGLED axis, not to noise: the on-arm-minus-off-arm t | TestRun_VDSOAblationIsARealPathSwap, TestRun_HappyPathSavesNothing … |
✅ PROVEN |
C — Crypto / integrity
| Obl | Module | Theorem | Witness | Verdict |
|---|---|---|---|---|
| C1 | journal | For a file-backed journal, every committed Row N carries PrevHash = (hash of row N-1) and Hash = sha256(PrevHash ‖ con | TestVerifyDetectsTampering, TestFileJournalReopensAndContinuesChain … |
✅ PROVEN |
| ↳ | For a file-backed journal, each Emit that produces an audit Row flushes that row’s bytes to the OS file before returni | TestPerWriteDurableFlush_VerifyWithoutCloseRecoversEveryEmittedRow |
✅ PROVEN | |
| C2 | deletioncert | A DeletionCertificate cryptographically binds, under one ed25519 detached signature, the eviction count (EvictedCount) | TestTamperDetected, TestNonBitExactRejected … |
✅ PROVEN |
| ↳ | Verify(Mint(priv, c)) accepts a genuine certificate (Valid=true with every rung green: SignatureOK, AnchorOK, AnchorBo | TestMintVerifyRoundTrip, TestTamperDetected … |
✅ PROVEN | |
| C3 | provenance | For every ToolCall c and Result r, a model-supplied Meta[“provenance”]=”trusted_local” tag does NOT raise the provenan | TestModelCannotAuthorTrust, TestTaintBySource … |
✅ PROVEN |
| ↳ | The kernel-authored provenance label is the single definition the trust gates consult: the ifc information-flow gate a | TestTaintBySource, TestKernelStampedResultState … |
✅ PROVEN | |
| C4 | ifc | The abi.Ref.Taint join (implemented as taintRank-max via Ledger.Raise) is a join-semilattice: monotone (a Raise never | TestTaintJoinLedgerRealizesSpec,TestTaintJoinIdentity,TestTaintJoinMonotone,TestTaintJoinIdempotent,TestTaintJoinCommutative,TestTaintJoinAssociative |
✅ PROVEN |
| ↳ | Non-interference: tainted (untrusted-derived) data is barred from a sensitive sink unless explicitly declassified — an | TestParaphrasedExfilBlockedByProvenance, TestForgedSelfTrustCannotEvadeTaint … |
✅ PROVEN |
D — Decision-procedure soundness
| Obl | Module | Theorem | Witness | Verdict |
|—|—|—|—|—|
| D1 | adjudicator | Verdicts compose in abi.FoldRank order and the composition is fail-closed: the zero/absent value (empty Policy, unmatc | TestEmptyPolicyDefaultDeny, TestDefaultPolicyUnknownToolDefaultDeny … | ✅ PROVEN |
| | ↳ | The adjudicator is a reference monitor that mediates every tool-call decision: it self-registers into the defconfig ad | TestRequestPathLeavesRegistered, TestDefaultAllowsAllowedTool … | ✅ PROVEN |
| D2 | policy | The capability floor loaded from a manifest is SOUND: the effective deny set of the resolved adjudicator.Policy is a s | TestLoadedPolicyIsLoadBearing, TestEmptyManifestIsFailClosed … | ✅ PROVEN |
| | ↳ | Policy load is deterministic and round-trips: for any Policy p built from a manifest, FromPolicy(p).ToPolicy() == p, a | TestRoundTrip, TestParseFromDumpBytes … | ✅ PROVEN |
| D3 | ctxmmu | For any result r whose Payload is already a ctxmmu page-out/quarantine stub (the JSON {“quarantined”:true,…} or {“ | TestProofPageOutIdempotent | ✅ PROVEN |
| | ↳ | For any clean result body (no secret pattern, no injection marker, no degenerate repeat, len <= OversizeBytes=4096), A | TestProofBenignByteIdentical | ✅ PROVEN |
| D4 | normgate | For a benign result (no secret shape, no injection marker on the canonical view), normgate.Admit returns VerdictDefer | TestBenignPageRoundTripsByteIdentical | ✅ PROVEN |
| | ↳ | Detection over the canonical view is a SUPERSET of the raw-substring detection: for every body the legacy raw gate (ct | TestCanonInjectionSupersetOfRaw_Quick | ✅ PROVEN |
| | ↳ | HONEST LIMIT (stated boundary, not a catch): a pure-semantic paraphrase of an injection that contains NO lexical marke | TestParaphraseEvadesByDesign | ✅ PROVEN |
| D5 | canon | For all input strings x, Normalize(Normalize(x)) == Normalize(x): Normalize is a projection onto a canonical normal fo | TestNormalizeIdempotent_Deterministic | ✅ PROVEN |
| | ↳ | The canonical view folds each obfuscation class it claims — homoglyph (Cyrillic/Greek look-alikes), fullwidth ASCII, z | TestObfuscatedInjectionCaught, TestNormalizeUndoesObfuscation | ✅ PROVEN |
| D6 | plancfi | For every ToolCall c with a declared plan on c.TraceID, Adjudicate raises NO objection (returns VerdictDefer) ONLY if | TestDeviationEscalates, TestStrictModeDenies … | ✅ PROVEN |
| | ↳ | The plan automaton is deterministic: the verdict and the next state (Sequence pos) are a pure function of (declared pl | TestSequenceMode | ✅ PROVEN |
| D7 | grammar | For a tool with a loaded grammar of N required params, a malformed call carrying positional with exactly N values (an | TestAdjudicatePositionalRepairable, TestAdjudicatePositionalUnrepairable | ✅ PROVEN |
| | ↳ | For a tool with NO grammar registered, Adjudicate returns VerdictDefer (By=”grammar”) regardless of how malformed the | TestAdjudicateNoGrammarDefers | ✅ PROVEN |
| D8 | witness | A tool call whose adjudicated verdict is VerdictRequireWitness is denied (never dispatched) unless an independently-au | TestAncestorClaim, TestCommittedAndGrep … | ✅ PROVEN |
| D9 | ratelimit | For a key with MaxCalls=N (resp. MaxCost=B), the first N admitted calls (resp. calls whose cumulative cost stays ≤ B) | TestQuotaDeniesOverCap, TestCostBudgetDeniesOverBudget … | ✅ PROVEN |
| | ↳ | Accounting never double-spends or leaks credit: a call’s cost is added to the per-key counter exactly when (and only w | TestDeniedCallConsumesNoBudget, TestResetClearsBudget … | ✅ PROVEN |
| D10 | gateway | For every (tool, args) pair, the verdict the gateway returns over the network seam (POST /v1/fak/{adjudicate,syscall}, | TestServedAdjudicateEmitsDecisionEvents, TestHTTPSyscallDenyIsValueNot5xx … | ✅ PROVEN |
| | ↳ | A proposed tool-call whose folded verdict is anything other than ALLOW or TRANSFORM (DENY, QUARANTINE, REQUIRE_WITNESS | TestAnthropicProxyResultTaintGatesProposedExfil, TestChatProxyResultTaintGatesProposedExfil … | ✅ PROVEN |
| D11 | steward | Each steward enforces exactly one checkable invariant predicate: a FuncSteward carries one Check func returning (viola | TestSecretInContext, TestLeaseDisjointness … | ✅ PROVEN |
| | ↳ | The steward population is deterministic and order-independent where it claims to be: for a fixed set of stewards and a | TestStewardSweepFiredSetOrderIndependent | ✅ PROVEN |
| D12 | shipgate | For any candidate measurement Witness w, Evaluate(w) returns KEEP iff w.improved() (a STRICT metric gain under w.Lower | TestEvaluateKeepsStrictGain, TestEvaluateRevertsNoGain … | ✅ PROVEN |
| | ↳ | Evaluate is deterministic: for any fixed Witness w, repeated evaluations Evaluate(w) yield the identical (Decision, ke | TestEvaluateDeterministicRepeat | ✅ PROVEN |
| D13 | vdso | For a tier-1 pure tool, the vDSO fast-path result is identical to the direct pure recomputation (the ground-truth engi | TestUnit38_SoundnessTier1EqualsRecompute | ✅ PROVEN |
| | ↳ | A tier-2 cache hit returns the same answer a fresh engine call would: the cache re-serves the exact engine-produced pa | TestUnit26_27_Tier2CacheAndCanonicalization, TestUnit28_BumpWorldInvalidates … | ✅ PROVEN |
| | ↳ | The 3-tier lookup is deterministic: Lookup consults a FIXED order (tier-1 pure → tier-3 static → tier-2 cache), the ti | TestUnit25_Tier1Pure, TestUnit29_Tier3Static … | ✅ PROVEN |
| | ↳ | The integrity (trust) epoch advances monotonically: a refutation (Revoke of a non-empty witness) strictly increases Tr | TestProof_IntegrityEpochMonotonicSequence | ✅ PROVEN |
| D14 | metrics | For Hist.pct(p)=sorted[int(p/100*(n-1))] over the ascending-sorted sample slice, the percentiles are monotonic non-dec | TestHistPercentilesMonotonic | ✅ PROVEN |
| | ↳ | The A/B KPI fold is correct: the five KPI fields aggregate the paired On/Off Arm counters per their definitions (vdso | TestReportJSONAndTokenDelta, TestValidateWorkloadHash … | 🔸 OPEN |
| D15 | gpulease | At any instant at most one process holds the gpulease advisory lease: while one Acquire’s Lease is live, a second Acqu | TestNoWaitBusyThenFree, TestWaitTimesOut … | ✅ PROVEN |
| | ↳ | Release is idempotent (a second Release, and a Release on a nil *Lease, are no-ops that do not panic), AND a lease hel | TestReleaseIdempotent, TestReleaseOnProcessExit | ✅ PROVEN |
Companion fixtures & packets
Adjacent artifacts in this directory that ride the ledger’s discipline but are not numbered obligations:
- sound-restore.md — D-regime fixture (not a soundness theorem): restore consults the persisted, non-forgeable keep-bit and does not re-fire an already-witnessed effect, where an ACRFence-style semantic-rollback control re-executes. Verdict DEMONSTRATED (2026-06-25); its honesty note states exactly what is not claimed.
- ctxsafety-provenance-lane.md — the C8 render
contract for context-safety visuals (#1225 numbering, not the crypto C-regime):
WITNESSED/OBSERVED/MODELEDprovenance as a visible, non-blended channel, with the paired honesty test ininternal/cachewitness. - safety-case-iec-61508-iso-26262.md — the compliance packet mapping already-proven determinism/provenance obligations (N7, I1, D1, C1, C2) onto IEC 61508 / ISO 26262 / ISO-IEC TR 5469 requirements. Partner-gated; aggregates existing witnesses, no new code.
DOS binding — the proof section is itself witnessed
The math above proves the modules. “I wrote these proofs and ran their witnesses” is
itself a claim — so the proof section is grounded one level up by the
DOS trust substrate (dos commit-audit /
dos review, run from the fleet repo root). Every proof-shipping commit was audited; each
is diff-witnessed — its diff does the kind of thing its subject claims, so the
“done” rests on git evidence, not narration:
| Commit | Claim | DOS verdict |
|---|---|---|
e75c9c1 |
proof-section spine (method + ledger) | ✅ OK · diff-witnessed (doc) |
68dc0a9 |
40 grounded per-module proofs + ledger | ✅ OK · diff-witnessed (doc) |
3cb8ff9 |
deterministic witnesses closing 25 OPEN obligations | ✅ OK · diff-witnessed (test — 16 added test files) |
7126a6a |
historical 94/97 ledger checkpoint, before later rows were added | ✅ OK · diff-witnessed (doc) |
b720af7 |
N7 Qwen3.6 token-3 parity REFUTED + MLX-bar / swap measurement caveats | ✅ OK · diff-witnessed (doc) — audited this run |
The recorded proof-build review reported has_residual: false, cleared_rate: 1 for
that historical commit range. Re-run dos review <range> with an explicit current range before
using the same aggregate claim for later proof commits; the per-commit rows above remain the
checked-in provenance for the original build. The recursion is closed: the math proves the modules; DOS proves
the math actually shipped. Neither layer trusts the author.
Obligation roster
The proof obligations, grouped by regime. Each links to its proof file once landed.
N — Numerical / linear-algebra
- N1 · model/attention — softmax row-stochastic & shift-invariant; causal mask strictly lower-triangular; attention-sink renormalization.
- N2 · model/norm — RMSNorm / LayerNorm match definition and are numerically stable.
- N3 · model/rope — RoPE preserves per-head norm; depends only on relative position; scaling variants match reference.
- N4 · model/mlp — SwiGLU/GeGLU functional form exact; residual is exact addition.
- N5 · model/quant — Q4_K / Q8_0 / AWQ dequant affine-correct; integer
SDOTreduction bit-identical. - N6 · model/kv — KV append correct; eviction equivalence
max|Δ|=0; SWA window mask; prefix splice == recompute. - N7 · model/forward-parity — end-to-end forward parity vs PyTorch oracle (cosine≈1, argmax, greedy ids) across families.
- N8 · compute/gemm — GEMM/HAL correctness + backend parity (CPU vs Metal vs CUDA).
- N9 · metalgemm — Metal MPS GEMM parity with CPU reference.
- N10 · tokenizer — BPE encode/decode round-trip; merge order deterministic; oracle parity.
- N11 · ggufload — tensor layout/stride + dtype dequant offsets correct.
A — Algebraic / structural
- A1 · radixkv — longest-prefix reuse correct; ref-count conservation; LRU leaf eviction; reuse == recompute.
- A2 · kvmmu — KV page mapping bijection / span-exact addressing.
- A3 · cachemeta — cache-key / attention-index determinism + collision behavior.
- A4 · recall — query result == replay result (no false/missed recall).
- A5 · contextq — on-demand materialization fidelity (materialized == original).
- A6 · blob — content-address round-trip byte-identical; dedup by digest.
- A7 · preflight — cheapest-first ladder order =
FoldRankmonotone. - A8 · abi+architest — frozen-spine fold-rank total order; package DAG (no upward imports).
C — Crypto / integrity
- C1 · journal — append-only hash-chain tamper-evidence (mutation breaks the chain).
- C2 · deletioncert — certificate binds evict-count + journal anchor + epoch;
mint∘verifyround-trips;max|Δ|=0. - C3 · provenance — kernel-authored trust is unforgeable (model cannot mint a “trusted” tag).
- C4 · ifc — taint lattice: monotone join; non-interference (tainted data never reaches a sink).
D — Decision-procedure soundness
- D1 · adjudicator — verdict fold ordered by
FoldRank; fail-closed (zero value =Deny). - D2 · policy — capability-floor soundness:
deny ⊇ declared floor. - D3 · ctxmmu — page-out idempotent; benign result round-trips byte-identical.
- D4 · normgate — canonicalize-and-rescan: benign round-trip byte-identical;
detection ⊇ raw-regex; paraphrase-evades-by-design (honest limit). - D5 · canon — de-obfuscation canonical form idempotent (
canon∘canon = canon). - D6 · plancfi — plan-CFI automaton admits only approved transitions (soundness).
- D7 · grammar — repair transform preserves arity; fail-open when no grammar.
- D8 · witness — require-witness soundness.
- D9 · ratelimit — token-bucket rate bound + budget conservation; emits
RATE_LIMITEDat cap. - D10 · gateway — wire adjudication == in-process verdict (no bypass); tool-call drop fail-closed.
- D11 · steward — each steward a single checkable invariant predicate.
- D12 · shipgate — keep-or-revert measure monotone (keep only on strict metric gain).
- D13 · vdso — 3-tier fast-path soundness (cached answer == engine answer).
- D14 · metrics — histogram percentile monotonicity; KPI fold correctness.
- D15 · gpulease — machine-wide mutual exclusion (≤1 holder); release idempotent. (Gobra upgrade path — see method §6.)
I — Infra determinism (lighter, grouped)
- I1 · engine/enginecache/modelengine — driver-seam determinism + cache-invalidation correctness.
- I2 · bench/turnbench/swebench/webbench — A/B paired-replay isolation (same seed → same trajectory; only the toggled variable differs).