diff --git a/README.adoc b/README.adoc
index aad0968a..e7ef02d0 100644
--- a/README.adoc
+++ b/README.adoc
@@ -107,6 +107,27 @@ Run the coherence tests:
 node --test mcp-bridge/tests/
 ----
 
+== Formal verification
+
+BoJ's ABI safety layer is written in Idris2 with the proof obligations
+audited in `PROOF-NEEDS.md`. Headline posture (as of 2026-05-18 audit):
+
+* *All P1/P2 obligations closed.* `SafePromptInjection`, `SafeCORS`,
+  `SafeAPIKey`, `SafeWebSocket`, `SafeHTTP`, `Federation`, `Catalogue`,
+  `CartridgeDispatch` (BJ1), `CredentialIsolation` (BJ2),
+  `APIContractCoverage` (BJ3) — all carry constructive proofs.
+* *Five remaining `believe_me` invocations*, all isolated in
+  `src/abi/Boj/SafetyLemmas.idr`, all class (J) — *principled
+  assumptions*, not unproven debt. They axiomatise the soundness of
+  Idris2 0.8.0's opaque `Char`/`String` primitives (`prim__eqChar`,
+  `prim__strToCharList`, `prim__strAppend`, `prim__strSubstr`) which
+  have no in-language induction principle. The only reduction path is
+  external backend-assurance evidence (Chez/BEAM extraction or
+  property-test harness), not constructive in-language proof.
+* *No unproven obligations remain in the audited surface.* The full
+  per-site rationale and the in-progress cross-cartridge composition
+  question are tracked in `PROOF-NEEDS.md` and `docs/decisions/`.
+
 == License
 
 PMPL-1.0-or-later
diff --git a/src/abi/Boj/SafetyLemmas.idr b/src/abi/Boj/SafetyLemmas.idr
index cfaca09a..c13a707c 100644
--- a/src/abi/Boj/SafetyLemmas.idr
+++ b/src/abi/Boj/SafetyLemmas.idr
@@ -6,12 +6,20 @@
 ||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection,
 ||| SafeAPIKey, and Safety modules.
 |||
-||| Three axiomatic believe_me primitives are declared here:
-|||   charEqSound  — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
-|||   charEqSym    — symmetry of prim__eqChar (x == y = y == x)
-|||   unpackLength — prim__strToCharList preserves length
+||| Five axiomatic believe_me primitives are declared here. Each is
+||| class (J) — genuinely unavoidable in Idris2 0.8.0 because `Char`
+||| and `String` are opaque primitive types whose operations are
+||| foreign functions with no constructors and no in-language induction
+||| principle. They are documented as principled assumptions, not
+||| unproven debt; see PROOF-NEEDS.md for the per-site audit.
 |||
-||| All other proofs are constructive.
+|||   charEqSound       — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
+|||   charEqSym         — symmetry of prim__eqChar (x == y = y == x)
+|||   unpackLength      — prim__strToCharList preserves length
+|||   appendLengthSum   — prim__strAppend: length (s ++ t) = length s + length t
+|||   substrLengthBound — prim__strSubstr: result no longer than the requested count
+|||
+||| All other proofs in this module are constructive.
 module Boj.SafetyLemmas
 
 import Data.List
@@ -215,12 +223,12 @@ unpackLength _ = believe_me ()
 ||| Idris2 type level. Established by semantics of all supported backends.
 %unsafe
 export
-appendLengthSum : (s t : String) -> length (s ++ t) = length s + length t
+appendLengthSum : (s, t : String) -> length (s ++ t) = length s + length t
 appendLengthSum _ _ = believe_me ()
 
 ||| Substring of a string has length at most the requested count.
 ||| Axiomatic: prim__strSubstr semantics — result is never longer than `len`.
 %unsafe
 export
-substrLengthBound : (s : String) -> (start len : Nat) -> LTE (length (substr start len s)) len
+substrLengthBound : (s : String) -> (start, len : Nat) -> LTE (length (substr start len s)) len
 substrLengthBound _ _ _ = believe_me ()