---
version: 0.28.0
date: 2026-06-20
headline: "Dedicated math-proof section: every sub-module gets a theorem + a deterministic witness; 94/97 PROVEN, DOS-grounded."
themes: ["proofs", "ctxmmu", "dgx", "gcp-bench", "architest", "agent"]
highlights:
  - "proofs: new fak/docs/proofs/ — 40 sub-module obligations, 98 theorems, each with a deterministic witness"
  - "proofs: 94 PROVEN / 2 OPEN / 1 REFUTED / 1 SCOPED-OUT, verified by a real go test ./internal/... pass"
  - "proofs: 16 new stdlib witness tests close 25 previously-unwitnessed properties (softmax, RoPE, GEMM, taint lattice, …)"
  - "proofs: REFUTED finding — Qwen3.6-27B hybrid-GDN greedy decode diverges from the llama.cpp oracle at token 3"
  - "proofs: every proof commit is DOS diff-witnessed; dos review reports zero residual"
  - "ctxmmu: classifyDurability stamps Verdict.Meta[\"durability\"] on the write-time gate"
  - "dgx: pure-Go Slack control-bridge RPC driver + base64 file transport"
---

**TL;DR** — This release adds a **dedicated math-proof section** (`docs/proofs/`) that states, for every fak sub-module, the theorem it must satisfy to be "math correct," gives the proof, and binds it to a **deterministic witness** — a test the toolchain re-runs — never to an author's say-so. Of 98 theorems, **94 are `PROVEN`** against a real `go test` pass, 2 are honestly `OPEN`, 1 is `SCOPED-OUT`, and **1 is `REFUTED`** — a real correctness gap the section caught (Qwen3.6 hybrid-GDN decode parity). The section is itself grounded in DOS (`dos commit-audit` / `dos review`), closing the recursion: the math proves the modules, DOS proves the math shipped. CI on `master` is currently red independent of this work (it predates the v0.27.0 cut); this release is cut on a verified-green local suite (`go build`/`go vet`/`go test ./internal/...` all green) per fleet's local-green release law.

> Current status: the GPU-server Slack control bridge described below was later removed
> from the public tree and belongs in `fak-private`; public `fak` keeps only scrubbed
> evidence/runbooks. See [`docs/dgx-slack-boundary.md`](../dgx-slack-boundary.md).

## Proofs — the dedicated math-proof section (headline)

- **What changed** — a new `docs/proofs/` section proves the mathematical correctness of every sub-module, with a verdict that is earned by a deterministic test, not asserted.
  - *Why:* the repo already *thought* in proof terms (`...RoundTripBitExact`, `TestVDSOSoundness`, `max|Δ|=0`, "FROZEN Taint lattice"), but nothing formalized each claim, bound it to a witness, and refused to call it correct on self-report.
  - *How:* `00-METHOD.md` fixes the discipline — four correctness regimes (numerical / algebraic / crypto / decision-procedure), the deterministic-witness taxonomy (oracle parity · metamorphic relations · bit-identity · round-trip · property · structural · crypto), the `PROVEN/REFUTED/OPEN/SCOPED-OUT` vocabulary + honesty rule, and the SOTA tooling survey (Gobra deductive-verifier frontier scoped-out with rationale; metamorphic-testing literature; stdlib `testing/quick`; PyTorch oracle export). `README.md` is the per-theorem master ledger; one `<module>.md` per obligation carries the theorem, proof with `file:line`, witness command, and live verdict.
- **What it proves** — **94 PROVEN · 2 OPEN · 1 REFUTED · 1 SCOPED-OUT** across **98 theorems / 40 obligations**, every verdict from an actual `go test -count=1` run cross-checked by an independent full `./internal/...` pass (45 packages green, 0 failures).
  - *How (closures):* 16 new zero-dependency witness tests (`internal/<pkg>/proofs_witness_test.go`, commit `3cb8ff9`) close 25 previously-OPEN properties — softmax row-stochasticity + shift-invariance, dense attention causality, LayerNorm affine-equivariance + RMSNorm scale-invariance, numerical stability to `|x|~1e20`, RoPE pair-norm preservation + relative-position dot, AWQ dequant bit-exactness, GEMM bilinearity, `canon` idempotence, the IFC taint join-semilattice, radix ref-count conservation + LRU eviction, and a dozen round-trip / determinism / mutual-exclusion invariants.
  - *The REFUTED finding (the section earning its keep):* N7 Theorem 3 — fak's in-kernel **greedy decode of Qwen3.6-27B (hybrid Gated-DeltaNet) diverges from the llama.cpp oracle at token 3**. First token is parity-exact (logit 28.30 = oracle 28.30); the third flips a near-tie argmax (`8160 "Here"` 23.18 vs the oracle's `90700 "Thinking"`), the signature of accumulated f32 drift in the GDN recurrent scan / int8-SDOT decode / attention accumulation order. fak is **forward-parity-PROVEN on llama but not yet at greedy-continuation parity on this arch** — recorded with its committed counterexample (`fak/experiments/qwen36/native-gguf-q8-multitoken-parity-20260619.json`), not deleted (00-METHOD §4).
  - *Honest residual:* the 2 OPEN (forward-pass cross-arch parity, A/B KPI fold) need absent oracle/HF fixtures; the 1 SCOPED-OUT (cross-backend GEMM agreement) needs other-backend builds. A vacuous pass would be dishonest, so they stay labelled.
- **Trust grounding** — every proof-shipping commit (`e75c9c1`, `68dc0a9`, `3cb8ff9`, `7126a6a`) is DOS `diff-witnessed`; `dos review` over the range reports `has_residual: false`, `cleared_rate: 1`. Companion to `SUBSYSTEM-CHECKS.md`: that proves a boundary is alive, this proves the math it computes is correct.

## ctxmmu — durability classification on the write-time gate

- **What changed** — the context-MMU stamps a durability class onto its verdict.
  - *How:* `classifyDurability` sets `Verdict.Meta["durability"]` on the write-time (post-tool) gate, so downstream consumers can read the context-MMU's durability decision off the verdict envelope.

## dgx — pure-Go Slack control bridge

- **What changed** — a Slack control-bridge RPC driver lands in pure Go.
  - *How:* the bridge RPC driver (`fak/internal/dgxbridge/rpc.go`, `slack.go`) plus a working transport with base64 file delivery and an env probe; `internal/dgxbridge` is declared at the architest foundation tier.

## gcp-bench — automated quota requests

- **What changed** — the GCP benchmark path can file its own capacity requests.
  - *How:* B200 quota-increase requests via the Cloud Quotas API, so a Blackwell benchmark run can request the GPUs it needs without a manual console step.

## agent — sampler invariant pinning

- **What changed** — the in-kernel sampler's top-k truncation gains an invariant test.
  - *How:* `internal/agent/inkernel_topk_test.go` pins per-request TopK truncation invariants on the in-kernel sampler.
