diff --git a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean
index 190bc1d12d..55285f4638 100644
--- a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean
+++ b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean
@@ -25,8 +25,17 @@ finite-control machines with strict polynomial bounds and independent fair coins
 conventions, `Randomized.StrictPPT`, `Randomized.Negligible` and `Randomized.Indistinguishable`,
 are the shared foundations displayed in the appendix.
 The definitions and theorem statements below specify the claim; Lean checks their proofs through
-`CryptographyBridge`. The audit allows only the listed foundational program, interpretation and
-machine modules across the implementation boundary, without importing a security definition.
+`CryptographyBridge`. Besides the shared foundations, the audit allows only the following eight
+foundational program, interpretation and machine modules across the implementation boundary,
+without importing a security definition:
+* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels
+  have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as
+  a typed program), `Probabilistic` (one fresh fair coin per live instruction) and
+  `Probabilistic.Oracle` (fair-coin runs with external oracle calls);
+* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only
+  randomness is uniform choice from a finite range), `Oracle` (private coins beside external
+  calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful
+  randomized oracle).
 
 ## References
 
diff --git a/abstracts/ComplexityAbstracts/ShamirAbstract.lean b/abstracts/ComplexityAbstracts/ShamirAbstract.lean
index 91a0f288f9..53f2caf7d2 100644
--- a/abstracts/ComplexityAbstracts/ShamirAbstract.lean
+++ b/abstracts/ComplexityAbstracts/ShamirAbstract.lean
@@ -24,8 +24,16 @@ bounds and correctness apply to encoded instances. The explicit foundational mod
 distinguishes finite-uniform requests in program syntax from their efficient fair-coin realization.
 
 The definitions and theorem statement below specify the claim. Lean checks the bridge, and the
-audit permits only the seven listed foundational program and machine modules, with no
-complexity-class or headline-result allowance.
+audit permits only the following eight foundational program and machine modules, with no
+complexity-class or headline-result allowance:
+* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels
+  have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as
+  a typed program), `Probabilistic` (one fresh fair coin per live instruction) and
+  `Probabilistic.Oracle` (fair-coin runs with external oracle calls);
+* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only
+  randomness is uniform choice from a finite range), `Oracle` (private coins beside external
+  calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful
+  randomized oracle).
 
 ## References
 
diff --git a/abstracts/ComplexityAbstracts/TodaAbstract.lean b/abstracts/ComplexityAbstracts/TodaAbstract.lean
index 21c5570ca7..d57d93675e 100644
--- a/abstracts/ComplexityAbstracts/TodaAbstract.lean
+++ b/abstracts/ComplexityAbstracts/TodaAbstract.lean
@@ -27,9 +27,17 @@ extension of valid bit answers to words outside the query encoding's image. The
 is deterministic. Its resource bound is expressed by exact realization on a clocked fair-coin
 machine; the same interaction interface also supports randomized programs.
 
-The definitions and theorem statement below specify the claim. Lean checks the bridge, and the
-audit permits only the listed foundational program and machine modules, with no complexity-class
-or Toda-theorem allowance.
+The definitions and theorem statement below specify the claim. Lean checks the bridge, and
+besides the shared foundations the audit permits only the following eight foundational program and
+machine modules, with no complexity-class or Toda-theorem allowance:
+* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels
+  have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as
+  a typed program), `Probabilistic` (one fresh fair coin per live instruction) and
+  `Probabilistic.Oracle` (fair-coin runs with external oracle calls);
+* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only
+  randomness is uniform choice from a finite range), `Oracle` (private coins beside external
+  calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful
+  randomized oracle).
 
 ## References