diff --git a/README.md b/README.md
index 29de976..e2d43ca 100644
--- a/README.md
+++ b/README.md
@@ -23,6 +23,13 @@ statements; this repository exists to do it properly.)
 
 ## Layer status
 
+> **Construction note (2026-07-02):** the field layer is mid-build. PROVEN and
+> compiled: PPallas (primality), Denote (Montgomery denotation), HelperSpecs
+> (adc/sbb/mac), SubNegSpec (sub/neg). DRAFTED, awaiting compilation:
+> AddSpec, ConstSpecs, ReduceSpec (Montgomery reduction), MulSpec. Not yet
+> written: SquareSpec, InvertSpec, FieldMain (the certificate), check.sh.
+> This note is removed when `verification/check.sh` goes green end-to-end.
+
 | Layer | Certificate | Status | Axioms of certificate |
 |-------|-------------|--------|-----------------------|
 | Field 𝔽_p (Montgomery) | `fieldImplementation` | ⏳ in progress | — |
diff --git a/verification/lean-guard b/verification/lean-guard
index 256ef42..10a0af3 100755
--- a/verification/lean-guard
+++ b/verification/lean-guard
@@ -106,7 +106,7 @@ if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null;
     # --scope runs the command as a child of THIS shell (env inherited),
     # merely placing it in a fresh cgroup with the hard caps below.
     systemd-run --user --scope --quiet \
-        -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \
+        -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
         -- taskset -c "$CORES" \
            timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
            lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"