diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json
index 2cbb2e1..cdc7aca 100644
--- a/verification/PROVENANCE.json
+++ b/verification/PROVENANCE.json
@@ -3,7 +3,7 @@
   "parameter_set": "SLH-DSA-SHA2-128s",
   "source": {
     "repo": "github.com/saymrwulf/fips205-source",
-    "head": "c945821bf964a78bed3ba920ad5aa021083e6237",
+    "head": "a3ce8e8644fe302019ed7ae271912333f1476de4",
     "upstream_base": "integritychain/fips205 @ 30bac08580aa61f653e5436d1bbacb5ffac446c4",
     "upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit; then NIST ACVP SHA2-128s sigVer vectors + an expanded differential bridge (TEST-ONLY: no verify-path function changed, and re-running extract.sh against this commit reproduces the TWO Aeneas-generated model files (Types.lean, Funs.lean) byte-identically; the two *External.lean files are hand-maintained and are NOT regenerated by extraction \u2014 they are separately byte-pinned in model_integrity_sha256 and were unchanged by this commit)",
     "cargo_lock": "committed",
@@ -50,7 +50,7 @@
     "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
     "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
     "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
-    "extract.sh": "2829b863301e1e6677376dd2c948673341e934c81dd55a19ff764f563ff22665"
+    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9"
   },
   "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
 }
diff --git a/verification/extract.sh b/verification/extract.sh
index a3114e4..397c02e 100755
--- a/verification/extract.sh
+++ b/verification/extract.sh
@@ -33,7 +33,7 @@ CRATE="${1:-$HOME/GitClone/FormalVerification/sources/fips205-source}"
 
 # The pinned source commit this repo's model + proofs were verified against.
 # Keep in lockstep with verification/PROVENANCE.json and the README snapshot.
-EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-c945821bf964a78bed3ba920ad5aa021083e6237}"
+EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-a3ce8e8644fe302019ed7ae271912333f1476de4}"
 
 # ── Provenance guard: refuse a wrong or dirty source tree (fail-closed) ──────
 [ -d "$CRATE/.git" ] || { echo "ERROR: '$CRATE' is not a git checkout of fips205-source." >&2; exit 2; }