godel-kernel

What this badge asserts — and what it does not. Green means: on the head of the branch, CI fetched the pinned tla2tools.jar (BLAKE3-verified — a hash mismatch aborts), ran every (module, N) instance under the pinned JDK, and every instance reproduced its committed green/*.tlc-green record — identical distinct-state count AND identical invariant verdict. By design it asserts reproducibility fidelity — "the committed numbers are real and stable" — not invariant cleanliness — "the kernel is proved". It stays green only while every committed verdict reproduces; it would stay green even if a verdict were VIOLATED, as long as that VIOLATED reproduced bit-for-bit. (As it stands, all ten committed verdicts reproduce as PASS — see STATUS.md.) A badge that meant only "TLC exited 0" would be theatre (TLC exits 0 on a vacuous spec); this one turns red the day a guard edit silently changes the state space — even if TLC still "succeeds". (Demonstrated: see FINDINGS.md.)

The runnable TLA⁺ companion to the essay Taking Gödel Seriously. Where the paper argues that no model can prove its own constitution, this repo lets you run the mechanism the argument is about — and check, with a single command, the exact state counts the paper claims.

STATUS — invariant-clean on the machine-checkable subset. All four modules pass their formalisable load-bearing invariants empirically, state-by-state, under TLC across all ten instances (three attestor-graph modules swept over N ∈ {3, 5, 7}, plus the GovernanceGate singleton fixture); the reproducibility harness verifies them bit-for-bit. "Invariant-clean" here covers the invariants reducible to a predicate over the model state — A1–A4, A6, A11, FreshnessMonotone, plus the governance gate's GovernanceGateRespected (the witness→act wiring). The mycelial axiom's social / editorial obligations — A5 (vetting-gate), A7 (tempo monitoring), A8 (veto-cost publication), A9 (no-celebrity), A10 (dated absorption ceremony) — are predicates over the world, not the model; they are decreed out-of-model and are intentionally not encoded here. See STATUS.md.

One command

./reproduce.sh

It fetches the pinned tla2tools.jar by hash (aborting on mismatch), runs every (module, N) instance, recomputes each green/*.tlc-green proof record, and diffs it against the committed one. It exits non-zero on any divergence — a guard silently edited, a constant tightened, a distinct-state count that moved. That diff is the proof; a badge that only means "TLC exited 0" is theatre (TLC exits 0 on a vacuous spec).

./reproduce.sh --list      # the instance matrix (3 sweep modules × N∈{3,5,7} + 1 singleton)
./reproduce.sh --update    # regenerate green files after a reviewed spec change

Requirements: java (major pinned in pinned-tooling.env), b3sum (BLAKE3), and curl/wget (only if the jar is not already present; or set TLA2TOOLS_JAR=/path/to/tla2tools.jar).

The commit-time freshness gate

./reproduce.sh is the proof — but it re-runs every TLC instance (~minutes) and so, in practice, fires only in CI. That left a cheap invariant ungated at commit time: nothing guaranteed a committed green/*.tlc-green records the hash of the spec it sits next to. A specs/*.tla edited and committed without the matching ./reproduce.sh --update ships a green that describes the old spec — a reproducibility lie that survives until the next full CI run. That is exactly how a red badge once shipped.

tools/check-greens-fresh.sh closes it with hashing alone (no jar, no JDK, no TLC): for every instance it asserts blake3(committed spec/cfg/mc) equals the spec_blake3/cfg_blake3/mc_blake3 recorded in its green. It runs in two places — install once after cloning:

tools/install-hooks.sh           # core.hooksPath → tools/git-hooks (pre-commit)

After that, any commit touching specs/*.tla|*.cfg or green/*.tlc-green is gated locally in milliseconds; .github/workflows/greens-fresh.yml runs the same check on every push. It is a necessary condition (the green describes this spec), not the sufficient one (the count is that spec's count) — the latter still needs ./reproduce.sh. Deliberate bypass: git commit --no-verify.

What a passing run does and does not establish

A PASS verdict is a real, bounded theorem: for the specified finite instance (N ≤ 7, bounded horizon), the safety invariants hold on every reachable state of the model. It is not a proof of the essay's thesis. The kernel is machine-checkable, not machine-proved: it demonstrates that the design is internally consistent with the thesis on bounded models; it does not, and by its own construction cannot, prove that thesis from within.

That refusal is deliberate and load-bearing. Each module states a theorem without proof:

THEOREM ExternalObligation == ...
\* OBLIGATION_EXTERNAL -- NOT PROVED WITHIN THIS MODULE.
\* Discharged by witness <DID:w> attesting <hash> at <ISO-8601 t>.

This is the formal shadow of Gödel's second theorem: the spec declines to prove its own constitution from within. A future in-module discharge of ExternalObligation would be the mechanical falsifier of the kernel's honesty — the kernel is meant to be incomplete exactly where the essay says it must be.

Layout

specs/
  MycelialGate.tla       AttestorGraph.tla       WitnessFreshness.tla   doctrinal sweep modules
  GovernanceGate.tla     the public, runtime-decoupled honest-line anchor (singleton)
  MC_<Module>.tla        symmetry harness (named Permutations operator for SYMMETRY)
  <Module>_N{3,5,7}.cfg  one runnable config per N (sweep modules; no hand-edit step)
  GovernanceGate.cfg     the single fixed three-molecule fixture (m_g/m_o/m_x)
green/
  <Module>_N{3,5,7}.tlc-green   committed proof records (the diff target)
  GovernanceGate.tlc-green      the singleton's committed record
KERNEL.md              generated: clause → TLA⁺ → expected distinct-count
reproduce.sh           the verifier / single writer of the green files
pinned-tooling.env     the (version, jar-hash, java-major) reproducibility triple
FINDINGS.md            what the harness has caught (with evidence) — read this
tools/
  check-greens-fresh.sh  fast hash-only commit-time gate (greens describe specs)
  git-hooks/pre-commit   version-controlled hook calling the gate (staged index)
  install-hooks.sh       sets core.hooksPath → tools/git-hooks (run once)
.github/workflows/
  tlc.yml              CI: runs reproduce.sh per push → the badge above (the proof)
  greens-fresh.yml     CI: fast hash-freshness gate per push (necessary condition)

The modules are a screened, one-way projection of an internal source of truth; they are regenerated, never hand-edited (the code identifiers — the Mycelial, Attestor and Witness families — are exactly the paper's vocabulary).

Symmetry / counts

Each sweep instance is model-checked through MC_<Module>.tla, which declares AttestorPerms == Permutations(...); its distinct-state count is therefore a symmetry quotient — states counted up to attestor permutation. The singleton GovernanceGate carries no symmetry (its three molecules are distinct roles), so its count is exact. KERNEL.md labels each count and maps it to the clause it verifies.

Reproducibility, precisely

For a fixed (spec-hash, cfg-hash, tla2tools-version) triple, any third party obtains the identical distinct-state count and the identical invariant verdict.

states_generated and depth are recorded as informative; the distinct-state count and the verdict are the equality obligations reproduce.sh enforces.