diff --git a/proven.ipkg b/proven.ipkg
index 40402c1a..212c1feb 100644
--- a/proven.ipkg
+++ b/proven.ipkg
@@ -238,6 +238,7 @@ modules = Proven
         , Proven.SafeCORS
         , Proven.SafeCORS.Proofs
         , Proven.SafeAPIKey
+        , Proven.SafeAPIKey.Proofs
         , Proven.SafeWebSocket
         -- Security hardening modules (v1.2.0)
         , Proven.SafeCSRF
diff --git a/src/Proven/SafeAPIKey.idr b/src/Proven/SafeAPIKey.idr
index a171cd8d..b3ca8f1f 100644
--- a/src/Proven/SafeAPIKey.idr
+++ b/src/Proven/SafeAPIKey.idr
@@ -84,9 +84,17 @@ record APIKey where
 ||| Postulate: length check for key construction
 keyLengthOk : (s : String) -> {auto 0 _ : So (length s >= MinKeyLength)} -> So (length s >= MinKeyLength)
 
-||| Attempt to create an APIKey from a raw string
+||| Attempt to create an APIKey from a raw string.
+|||
+||| The empty-string fast-path is explicit so the proof
+||| `emptyKeyRejected` (in `Proofs.idr`) discharges by `Refl` without
+||| relying on the `prim__strLength`/`>=` FFI primitives to reduce at
+||| type-check time. Behaviour is identical to a single `with`-clause
+||| definition — empty strings fail the length check either way.
+||| See hyperpolymath/proven#95.
 public export
 mkAPIKey : String -> Maybe APIKey
+mkAPIKey ""  = Nothing
 mkAPIKey s with (choose (length s >= MinKeyLength))
   mkAPIKey s | Left prf  = Just (MkAPIKey s (detectFormat s) prf)
   mkAPIKey s | Right _   = Nothing
diff --git a/src/Proven/SafeAPIKey/Proofs.idr b/src/Proven/SafeAPIKey/Proofs.idr
index 90779049..ed471a45 100644
--- a/src/Proven/SafeAPIKey/Proofs.idr
+++ b/src/Proven/SafeAPIKey/Proofs.idr
@@ -71,10 +71,21 @@ emptyFormatUnknown = Refl
 --------------------------------------------------------------------------------
 
 ||| fullMask never exposes any key characters.
-||| The output is "[REDACTED:N chars]" which contains no key material.
+|||
+||| The original formulation asked for `isPrefixOf "[REDACTED:"`
+||| (fullMask key) = True`, but Idris2 0.8.0 cannot reduce the
+||| `isPrefixOf` call through the `unpack`/`++` String-FFI chain when
+||| the right operand is universally quantified. Splitting the
+||| guarantee in two delivers the same safety property by structural
+||| equality (which `Refl` discharges) plus a derived prefix-lemma
+||| that any consumer can apply locally — see #95 for the bridge
+||| approach.
+|||
+||| The output is "[REDACTED:N chars]" — opaque length, no key bytes.
 public export
-fullMaskFormat : (key : APIKey) -> isPrefixOf "[REDACTED:" (fullMask key) = True
-fullMaskFormat key = Refl
+fullMaskStructure : (key : APIKey) ->
+                    fullMask key = "[REDACTED:" ++ show (length key.raw) ++ " chars]"
+fullMaskStructure _ = Refl
 
 --------------------------------------------------------------------------------
 -- Format Matching Properties