gale v0.8.0

What's Changed

• ci: actually run the Lean proofs — 136 theorems that no workflow ever compiled (#286) by @avrabe in #288
• docs(T4): commit the synth-wcet-v1 fixture, and measure v0 identity churn for scry by @avrabe in #293
• proofs(T3): gale's side of the supply obligation — the bridge lemma, machine-checked by @avrabe in #292
• proofs(T3): discharge SupplyGuarantee for gust's static frame at ≤½ utilisation by @avrabe in #295
• ci(lean): adopt the rules_lean platform fix, drop the workaround and the stale patch by @avrabe in #296
• chore(deps): bump pulseengine/rivet from 0.32.0 to 0.34.0 by @dependabot[bot] in #299
• chore(deps): bump syn from 3.0.3 to 3.0.4 in /tools/verus-strip by @dependabot[bot] in #300
• proofs+docs(T3): discharge SupplyGuarantee UNCONDITIONALLY, and record it — status stays proposed by @avrabe in #297
• chore(toolchain): pin varve layer 2026.08.4 — adopted only after proving it changes nothing by @avrabe in #298
• proofs(T3): derive Θ_eff from a real frame window, and machine-check the raw-budget unsoundness by @avrabe in #301
• feat(drv): pwm-thin imports gust:hal instead of raw env — the worked example for #302 by @avrabe in #303
• proofs(T3): Θ_eff is additive over disjoint windows — k windows cost k ticks by @avrabe in #304
• feat(drv): the last four thin drivers import gust:hal — REQ-DRV-COMPONENT-001 is 13 of 13 by @avrabe in #305
• feat(ci): VER-DRV-COMPONENT-001 gate — the half that makes 13 of 13 stick by @avrabe in #306
• fix(drv): re-pin the driver symbol contract, and gate the object axis so it cannot drift again (#307) by @avrabe in #308
• docs(T2): 51% → 64% — the matcher was guessing theorem names, in three ways by @avrabe in #309
• fix(ci): pin the cross-arch gate and wire it — my "RISC-V is red" finding was a stale binary by @avrabe in #310
• feat(gust:os): implement world app-timer — the periodic-loop shape jess asked for, and fix the world that could not work by @avrabe in #311
• fix(varve): pin the layer by digest — the rolling channel republished 2026.08.4 by @avrabe in #312
• fix(drv): gate the PROVIDERS enumeration against reality by @avrabe in #314
• fix(drv): the cross-arch gate was green because it could not see the defect by @avrabe in #316
• docs(plan): record the real blocking structure — neither v0.7.1 nor v0.7.2 is cuttable by @avrabe in #315
• docs(dma): re-verify the DMA evidence — Kani 6/6 holds, the committed object is 41 synth releases stale by @avrabe in #317
• find(oci): record why the Zephyr primitives cannot travel the OCI path by @avrabe in #318
• ci(gate): make the cross-arch gate REQUIRABLE — path filter moves off the trigger by @avrabe in #319
• ci(#289): retry + pipefail the apt.llvm.org installs — one of them is in release.yml by @avrabe in #320
• ci(#289): retry + scoped pipefail the remaining 16 rustup installs by @avrabe in #321
• find(oci): correct FIND-BYOOS-009 — the need is a LINKING gap, not a packaging one by @avrabe in #322
• ci(#324): fire the two kill-criteria that existed as code and ran nowhere by @avrabe in #325
• fuzz: gate coverage notes behind cfg(fuzzing) (#326) by @avrabe in #328
• docs(rv32): synth 0.61.0 refuses instead of shipping unlinkable objects by @avrabe in #329
• docs(pin): record that rustc is not pinned, and four objects have drifted by @avrabe in #330
• chore(varve): adopt 2026.09.0, and check the assumption its synth demands by @avrabe in #331
• chore(deps): bump pulseengine/rivet from 0.34.0 to 0.35.0 by @dependabot[bot] in #332
• docs(pin): correct the drift diagnosis — rustc is ruled out, sources moved by @avrabe in #334
• ci: gate that a committed object is not older than its sources (#334) by @avrabe in #335
• ci: extend the freshness gate from 4 committed objects to 20 by @avrabe in #336
• fix(ci): trigger compliance on the tag push, not the suppressed release event (#333) by @avrabe in #337
• ci: make the verification gates requirable (#294) by @avrabe in #338
• find(spar): record the spar→WIT gap as an observed incident, not a prediction by @avrabe in #339
• fix(ci): a required gate must not depend on undefined YAML semantics by @avrabe in #340
• ci: gate that a required context can actually report (#294, #340) by @avrabe in #341
• ci: require the new gate, and stop compliance overstating what "Cuttable" means by @avrabe in #343
• find(v0.5.0): the recorded blocker closed seven weeks ago — the real one had no tracker by @avrabe in #344
• feat(v0.7.1): split REQ-DRV-COMPONENT-001, and verify the half that is done by @avrabe in #345
• feat(v0.7.1): gate VER-DRV-GRAPH-001 — no raw env import in the composed graph by @avrabe in #346
• record: synth scoped the MPU blocker; the graph sweep landed but the dma-own call did not by @avrabe in #347
• feat(v0.5.0): CI-gate the MPU enforcement oracle, and make its control mechanical by @avrabe in #349
• feat: track the security-containment gap, and the MPU-primitive shipping ask by @avrabe in #350
• feat(v0.5.0): make the security-containment gap executable instead of prose by @avrabe in #351
• silicon(v0.5.0): unprivileged execution blocks the PPB escape — measured on the G474RE by @avrabe in #352
• feat(model): MPU presence is a declared target property, measured on both boards by @avrabe in #353
• silicon + evidence: run the MPU oracle on the G474RE, and correct what gale claimed about Renode by @avrabe in #354
• ci: require the two gates I built today and then did not require by @avrabe in #355
• feat(bench): claim the shared probe before touching it (#356) by @avrabe in #357
• fix(renode): gale's STM32F100 platform modelled an MPU the part does not have by @avrabe in #358
• chore(varve): bump to layer 2026.09.1, and correct two things the bump exposed by @avrabe in #359
• chore(bench): pin with-device v0.7.2, adopt --require-claim, stop inventing device names by @avrabe in #360
• find(v0.5.0): multi-tenancy is blocked by page-granular region sizing, not by RAM by @avrabe in #361
• feat(v0.5.0): REQ-OS-MPU-001's kill-criterion executes and holds, with a negative control by @avrabe in #362
• fix(rivet): drop release.require coverage — cuttability answers the evidentiary question now by @avrabe in #363
• feat: reproducible two-tenant runner — varve base, announced overrides by @avrabe in #364
• fix(bench): resolve with-device through varve — it is in the layer now by @avrabe in #366
• fix(gates): the WCET gate announced green while its comparison was exempt from set -e by @avrabe in #369
• fix(ci): 28 retry loops could not report failure — an install "succeeded" installing nothing by @avrabe in #370
• chore(deps): bump syn from 3.0.4 to 3.0.5 in /tools/verus-strip by @dependabot[bot] in #372
• fix(rivet): a resolved finding is release-ready — v0.7.0 was one artifact from cuttable by @avrabe in #367
• fix(varve): move to the rotated root and the new registry (gale#365) by @avrabe in #371
• chore(deps): bump pulseengine/rivet from 0.35.0 to 0.36.0 by @dependabot[bot] in #373
• fix(fv): 74 Rocq theorems are stated and not proven, and CI could not tell by @avrabe in #375
• release(v0.8.0): "Prove It" — notes for the tri-track theorem and the tickless timer by @avrabe in #376

Full Changelog: v0.7.0...v0.8.0