diff --git a/README.md b/README.md
index 5d35697..854b18d 100644
--- a/README.md
+++ b/README.md
@@ -27,8 +27,8 @@ in this repository.
 |-------|-------------|--------|-----------------------|
 | Field 𝔽_p          | `fieldImplementation`    | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Group law (Edwards) | `edwardsImplementation`  | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
-| Scalar mod ℓ        | `scalarImplementation`   | 🔨 foundation | denotation + L=ℓ proven; add/sub/mul in progress |
-| Signature (EdDSA)   | `verifyEquation`          | ⏳ in progress | — |
+| Scalar mod ℓ        | `scalarImplementation` (planned; `L_val` proven)   | 🔨 foundation | denotation + L=ℓ proven; add/sub/mul in progress |
+| Signature (EdDSA)   | `verifyEquation` (planned)          | ⏳ planned | — |
 
 Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
 This table is updated only when `verification/check.sh` passes for the layer.
diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh
index dc49996..e63c3bc 100755
--- a/verification/check-scalar.sh
+++ b/verification/check-scalar.sh
@@ -21,5 +21,21 @@ lake env bash -c "
   cd '$HERE'
   for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
 " || { echo FAIL; exit 1; }
+echo "=== Phase 3: axiom audit (kernel-level) ==="
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -uo pipefail
+  export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
+  cd '$HERE'
+  AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
+  { echo 'import Proofs.ScalarDenote'; echo '#print axioms ScalarProofs.L_val'; } > \"\$AUD\"
+  OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
+  echo \"\$OUT\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
+  echo \"\$OUT\" | grep -qF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || {
+    echo 'AXIOM AUDIT FAILED: L_val not clean'; exit 1; }
+" || { echo FAIL; exit 1; }
+echo "  L_val axiom-clean"
+
 echo ""
 echo "SCALAR FOUNDATION: gen compiles; denotation + group-order constant (L = ℓ) proven."
diff --git a/verification/check.sh b/verification/check.sh
index caf3ebb..36aedfe 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -20,7 +20,7 @@ source ~/aeneas-toolchain/env.sh
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
 TIMEOUT="${LEAN_TIMEOUT:-300}"
-export LEAN_MEM_MB="${LEAN_MEM_MB:-6144}"
+export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"  # 8192: ReduceSpec exceeds 6144 (coherence pass 2)
 CORES="${LEAN_MAX_CORES:-0-3}"
 
 # Layer manifests (extended as the pyramid grows; ORDER = import order).
@@ -110,6 +110,7 @@ lake env bash -c "
   for f in Proofs/*.lean; do
     b=\$(basename \"\$f\" .lean)
     [ \"\$b\" = AxiomCheck ] && continue
+    case \"\$b\" in Scalar*) continue;; esac  # scalar layer: checked by check-scalar.sh (coherence pass 2)
     case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac
   done
 "
@@ -125,12 +126,12 @@ lake env bash -c "
   set -euo pipefail
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
   cd '$HERE'
-  AUD=\$(mktemp /tmp/audit-XXXX.lean)
+  AUD=\$(mktemp '$HERE/.audit-XXXX.lean')
   {
     for i in ${AUDIT_IMPORTS[*]}; do echo \"import \$i\"; done
     for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done
   } > \"\$AUD\"
-  OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -M \${LEAN_MEM_MB:-4096} \"\$AUD\" 2>&1)
+  OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
   rm -f \"\$AUD\"
   N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true)