diff --git a/build/channels.scm b/build/channels.scm
index 54ac61a..9441973 100644
--- a/build/channels.scm
+++ b/build/channels.scm
@@ -5,12 +5,18 @@
 ;;   guix time-machine -C channels.scm -- shell -m manifest.scm
 ;;
 ;; Refresh it (after re-verifying) with: just toolchain-refresh
-;; Canon pin, verified 2026-09-30 (docker.io/metacall/guix, guix describe).
+;; Re-pinned for this repository on 2026-11-10 (re-anchoring plan WO 1.4, owner
+;; ruling 2026-11-10): from ae77aeb (canon pin of 2026-09-30) to 8edb9da, a
+;; commit the Guix build farm evaluated, because at ae77aeb Guix had no
+;; substitute for itself and each CI run compiled Guix first. The prover
+;; versions are the same at both: Agda 2.7.0.1, Rocq 8.18.0, Lean 4.29.0.
+;; PROVISIONING-STANDARD: channels.scm is re-pinned per repository, and is
+;; checked for a 40-hex commit pin, not byte-compared with the canon.
 (list (channel
        (name 'guix)
        (url "https://codeberg.org/guix/guix.git")
        (branch "master")
-       (commit "ae77aeb9543de2661d739104bc4d3803d8c6f38b")
+       (commit "8edb9da7052607f17f09007933275b43978fcf9d")
        (introduction
         (make-channel-introduction
          "9edb3f66fd807b096b48283debdcddccfea34bad"
diff --git a/verification/proofs/lean4/lean-toolchain b/verification/proofs/lean4/lean-toolchain
index d0eb99f..14791d7 100644
--- a/verification/proofs/lean4/lean-toolchain
+++ b/verification/proofs/lean4/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.29.0