diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index 9ffec84..fc54a36 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -37,7 +37,7 @@ ____
 
 **Evidence**: `examples/02-multi-module.twasm` demonstrates: Module A exports a `region Entity` with fields (pos_x, pos_y, hp); Module B imports the same region and defines typed load/store operations. `src/abi/Proofs.idr` proves field offset and alignment agreement.
 
-**Caveat**: Schema agreement proof is _type-level_ (compile-time). Does NOT verify that actual Rust/ReScript compiled code respects field layout — correspondence is manual. Runtime behavior depends on correct field packing across compilers.
+**Caveat**: Schema agreement proof is _type-level_ (compile-time). Does NOT verify that actual Rust/AffineScript compiled code respects field layout — correspondence is manual. Runtime behavior depends on correct field packing across compilers.
 
 === Claim 3: "Checked L1-L10 Proof Core — All 10 Levels Integrated"
 
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
index eb362fe..21ee9b4 100644
--- a/PROOF-NEEDS.md
+++ b/PROOF-NEEDS.md
@@ -502,7 +502,7 @@ operationally but does not prove the monotonicity as a theorem.
    (P2.1, P2.2), Levels monotonicity (P3.2). Cleanup session.
 
 After each session: run `idris2 --check` on every file in
-`typed-wasm.ipkg`, run `panic-attack assail` on the Rust/ReScript
+`typed-wasm.ipkg`, run `panic-attack assail` on the Rust/AffineScript
 adjacent code (no new unsafe code should land), update this file's
 inventory table, commit.