diff --git a/API-CONVENTIONS.md b/API-CONVENTIONS.md
index 61b379d0e3..24de631435 100644
--- a/API-CONVENTIONS.md
+++ b/API-CONVENTIONS.md
@@ -18,6 +18,8 @@ All pointers to non-empty buffers are assumed to be valid and non-NULL, and ever
 
 The exception is a pointer paired with a length: it may be NULL when that length is `0` — for example, the message `m` when `mlen == 0`, or `ctx` when `ctxlen == 0`. Such cases are called out in the per-function documentation.
 
+Buffers passed to the same function must not overlap.
+
 ## Output buffers on error
 
 When a function returns an error, each caller-owned output buffer is left either unchanged or fully zeroized. An output buffer is never left holding partially computed or otherwise stale data that could be mistaken for a valid result.
diff --git a/README.md b/README.md
index f916a13cc7..bb37e0b95e 100644
--- a/README.md
+++ b/README.md
@@ -56,7 +56,7 @@ mldsa-native is used in
 
 ## Formal Verification
 
-We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mldsa/src/*](mldsa) and [mldsa/src/fips202/*](mldsa/src/fips202) involved in running mldsa-native with its C backend. See [proofs/cbmc](proofs/cbmc) for details.
+We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mldsa/src/*](mldsa) and [mldsa/src/fips202/*](mldsa/src/fips202), except for the Armv8.1-M backend and the debug code. See [proofs/cbmc](proofs/cbmc) for details.
 
 All AArch64 and x86_64 assembly, and the RV32IM arithmetic backend, are
 proved functionally correct and memory-safe at the object-code level using
@@ -81,7 +81,8 @@ pointwise-multiplication assembly; see its [README](proofs/isabelle/neon_ntt/REA
 
 All assembly in mldsa-native is constant-time in the sense that it is free of secret-dependent control flow, memory access,
 and instructions that are commonly variable-time, thwarting most timing side channels. C code is hardened against compiler-introduced
-timing side channels through suitable barriers and constant-time patterns.
+timing side channels through suitable barriers and constant-time patterns. The C code assumes constant-time 32x32->32 and 32x32->64 multiplication,
+which some targets do not provide, e.g., cores without a hardware multiplier or with early-terminating multiply instructions.
 
 Absence of secret-dependent branches, memory-access patterns and variable-latency instructions is also tested using `valgrind`
 with various combinations of compilers and compilation options.
diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index d42095c87c..837078b153 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -26,7 +26,9 @@
  * # API conventions
  *
  * Conventions shared by all functions below (return values, pointer validity,
- * output buffers on error) are documented in API-CONVENTIONS.md.
+ * buffer overlap, output buffers on error) are documented in
+ * API-CONVENTIONS.md. In particular, buffers passed to the same function must
+ * not overlap.
  *
  * # Multi-level builds
  *