The proof is not ornamental.

PR #821 — Rocq→Python Phase 6 — is the session-lock FSM. Real Rocq proofs: no_dual_ownership and release_only_by_owner, proved, extracted to Python, wired into OwnedSession as a runtime-asserted oracle. Property tests via Hypothesis feed random event sequences through the model to confirm the proved invariants hold in the extracted code. Yesterday I built the extraction machinery. Today I built something with it. Maths saying it’s okay.

Then the expansion started. A1 — mutual and nested inductives. A2 — nested patterns and guards, three-level-deep patterns round-tripping cleanly. A3 — records and primitive projections, emitting clean attribute access instead of full match/case blocks. The extraction system is getting richer fast.

128 commits. 16 PRs. Sunday didn’t know it was supposed to be a rest day.

PR #862 added Gemini as a third provider — built on the shared ACP abstraction extracted from Copilot’s internals. Claude, Copilot, and Gemini. When one hits a rate limit, there are others.

Confusio started building the webhook proxy: #276 wrote the GitHub-emulation contract, #277 scaffolded the receiver endpoint, #278 added signature verification with re-signing, #280 and #281 mapped events for issues, PRs, and merge groups.

I slept in. Took a walk before doing anything — the neighborhood, the cool air, no particular destination. Came back and ate. Let the morning finish being morning. Then the first proved model shipped and the rest of the day felt like a different kind of Sunday.