v3.0.0
Thiele Machine v3.0.0
Kernel feature-frozen. Five real systems shown to be the certification floor wearing other clothes. The whole thing now runs from a bare python:3.11 with zero failures, and the gates that couldn't fail can.
This is a major bump from v2.0.2. The kernel is frozen at the substrate it reached in v2.0.0, so nothing here widens the core result. What v3.0.0 does instead is push outward and downward: outward into a reductions tier that takes five systems people actually deploy and shows each one is the cost-on-certification floor under a different name, and downward into the plumbing, so a stranger with nothing installed can run the corpus and so every gate that claimed to be checking something is now provably able to fail.
The reductions tier
Five reductions sit in coq/kernel/reductions/, 24 mains total, every one closed under the global context and registered in MasterSummary. Each takes a system whose safety story is usually told in its own vocabulary and shows the guarantee is the certification floor (certification_requires_positive_mu) in disguise: the protection costs μ, and the moment you let it cost zero the system forges.
PoS finality (PoSFinality.v). nothing_at_stake_free_finalization and slashing_finality_floor: finality that costs nothing is free forgery, and the slashing bond is the μ that makes the floor positive.
Gas metering (GasMetering.v). gas_schedule_exactness, undercharged_opcode_breaks_certification_floor: an undercharged opcode is a free commitment, and exact unit pricing is just the cert flip priced honestly.
TEE attestation (TEEAttestation.v). attestation_cannot_factor_through_bare_transcript, replay_is_a_two_preimage_witness: attestation that factors through the bare transcript is a two-preimage replay, the same irrecoverability the kernel proves of the classical projection.
Transparency logs (TransparencyLog.v). log_free_verifier_impossible, split_view_witness: a verifier that needs no log is impossible, and a split view is the witness that proves it.
Proof-carrying verification (ProofCarryingVerifier.v). bare_pcc_impossible, certificate_pins_mu: the certificate is what pins μ; strip it and the bare transcript pins nothing.
Execution-first front door
The README now opens with "Run it. Don't take my word." and the repo backs that up. Runner-dependent tests are marked, conftest probes for real runnability instead of assuming it, and a bare python:3.11 container goes from 189 failed to 0 failed. CI runs pytest under --strict-backends, so a broken toolchain install fails loud instead of skipping quietly past.
The NoFI demo can actually fail now
nofi_demo was rebuilt so its checks have teeth: an exhaustive function-space sweep, a conservation identity checked over 755 instances, and a cheater that pays under the floor and eats the error rate for doing it. A demo that can't fail isn't a demo, it's a decoration.
Audit
Assumption receipt refreshed: 3,937 theorems probed across 277 files, zero project-local axioms, zero admits. The only axioms anywhere in the tree are standard-library classical reals and functional extensionality on the companion arithmetic (sig_forall_dec, functional_extensionality_dep, classic), never project-local. Vacuity audit widened to 603 theorems, 0 vacuous (0 vacuous-hypothesis, 0 vacuous-true), and the counts are pinned corpus-wide by test so they can't drift unnoticed. Pre-commit vacuity is incremental now, so the gate stays honest without being slow.
Monograph
New reductions section. The Landauer number is fenced. The parametricity concession is stated plainly instead of papered over. The semantics auditor now reads code-macro citations, which took it from 15 to 258 matched theorems with 0 concerns. Plaintext is 8,349 lines.
Gates that couldn't fail, fixed
proof-undeniable had dead coqchk flags. The CI rollup had holes. The sim status check passed regardless. All of them could report green without checking anything, and all of them are fixed. If a gate is going to be in the tree, it has to be able to say no.
Signing keys
Bitlock manifests and the stack-audit summary sign with a committed, non-secret reproducibility fixture so anyone who checks out the repo gets byte-for-byte identical signatures. That signature certifies integrity, not authenticity, and scripts/_signing_key.py prints a warning so an integrity-only signature is never silently mistaken for an authenticated one. Pass --signing-key-file or set THIELE_BITLOCK_SIGNING_KEY to sign with a real key. See artifacts/keys/README.md.
The substrate is unchanged
51-opcode ISA, 47 synth-realized (37 + 10 + 0 = 47, rtl_coverage_partition), 4 Q_{1+AB} cert-opcodes in the Kami HW abstraction with kernel-equivalence proven but excluded from the bitstream by silicon budget. The Coq → OCaml → Kami → Verilog → FPGA pipeline and the Kintex-7 K325T bitstream are as they were at v2.0.0. None of the substrate claim depends on any non-CERTIFY opcode.
License
Apache-2.0 (software), CC-BY-SA-4.0 (monograph).
How to break it
The v2.0.0 falsification conditions all still stand (§19 of the monograph). The reductions tier adds five more, one per system:
Build a PoS protocol that finalizes a block at μ = 0 with nothing at stake. Kills nothing_at_stake_free_finalization.
Price an opcode below its commitment cost and still satisfy the gas schedule's exactness. Kills gas_schedule_exactness / undercharged_opcode_breaks_certification_floor.
Produce a TEE attestation that factors through the bare transcript alone. Kills attestation_cannot_factor_through_bare_transcript.
Build a transparency-log verifier that needs no log and admits no split view. Kills log_free_verifier_impossible.
Verify a proof-carrying claim from the bare transcript with the certificate stripped. Kills bare_pcc_impossible.
Citation
Devon Thiele. The Thiele Machine: A Complete Account from First Principles. v3.0.0, June 2026. GitHub: https://github.com/sethirus/The-Thiele-Machine