diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 03becaa..f1bde3d 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -27,7 +27,7 @@ cargo test
 ## Key Design Decisions
 
 - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)
-- MPL-2.0 license
+- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/
 - RSR (Rhodium Standard Repository) template
 - Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml
index a82f178..1f45960 100644
--- a/.github/workflows/rhodibot.yml
+++ b/.github/workflows/rhodibot.yml
@@ -4,7 +4,7 @@
 # Reads root-hygiene rules and auto-fixes what it can:
 #   - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots)
 #   - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml)
-#   - Fix SPDX headers (AGPL → PMPL in dotfiles)
+#   - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles)
 #   - Create missing required files (SECURITY.md, CONTRIBUTING.md)
 #   - Report unfixable issues as PR comments
 #
@@ -87,7 +87,7 @@ jobs:
           for dotfile in .gitignore .gitattributes .editorconfig; do
             if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then
               sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile"
-              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)"
+              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)"
               CHANGED=true
             fi
           done
diff --git a/.gitignore b/.gitignore
index 4b77703..875c66e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -116,3 +116,8 @@ deps/
 .cache/
 build/
 dist/
+
+# Idris2 proof build artifacts
+**/build/
+*.ttc
+*.ttm
diff --git a/.machine_readable/compliance/reuse/dep5 b/.machine_readable/compliance/reuse/dep5
index 49aaed6..bead9ed 100644
--- a/.machine_readable/compliance/reuse/dep5
+++ b/.machine_readable/compliance/reuse/dep5
@@ -52,3 +52,10 @@ License: MPL-2.0
 Files: cliff.toml
 Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
 License: MPL-2.0
+
+# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0).
+# Last-match-wins in the Debian copyright format, so this overrides the
+# `Files: *` default above for prose docs.
+Files: *.adoc *.md docs/* docs/**/*
+Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
+License: CC-BY-SA-4.0
diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml
index f2a4f95..731ffca 100644
--- a/.machine_readable/contractiles/trust/Trustfile.a2ml
+++ b/.machine_readable/contractiles/trust/Trustfile.a2ml
@@ -34,7 +34,7 @@ is traceable.
 
 ### license-content
 - description: LICENSE contains expected identifier
-- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE
+- run: grep -q 'MPL-2.0' LICENSE
 - severity: warning
 
 ## Container Security
diff --git a/Cargo.toml b/Cargo.toml
index ac6a1f1..97442fd 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,7 +5,7 @@ version = "0.1.0"
 edition = "2024"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 description = "Add formal type safety (10 levels, dependent/linear/session types) to any query language — SQL, GraphQL, Cypher, SPARQL, VCL"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/typedqliser"
 keywords = ["type-safety", "sql", "graphql", "formal-verification", "query"]
 categories = ["command-line-utilities", "database"]
diff --git a/LICENSE b/LICENSE
index 14e2f77..2a8b960 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 
diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc
index 36ef406..9069ad3 100644
--- a/QUICKSTART-MAINTAINER.adoc
+++ b/QUICKSTART-MAINTAINER.adoc
@@ -106,7 +106,7 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}`
 
 == Security Notes
 
-* License: MPL-2.0 (Palimpsest License)
+* License: MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 * All dependencies SHA-pinned
 * `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[]
 * OpenSSF Scorecard: see badge in README
diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml
index 883179e..7a4a97e 100644
--- a/contractiles/trust/Trustfile.a2ml
+++ b/contractiles/trust/Trustfile.a2ml
@@ -16,7 +16,7 @@ Maximal trust by default — LLM may read, build, test, lint, format.
 
 ### license-content
 - description: LICENSE contains expected SPDX identifier
-- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE
+- run: grep -q 'SPDX\|MPL-2.0' LICENSE
 - severity: critical
 
 ### no-secrets-committed
diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc
index 014b21c..8faf3bb 100644
--- a/docs/RSR_OUTLINE.adoc
+++ b/docs/RSR_OUTLINE.adoc
@@ -1,6 +1,6 @@
 = RSR Template Repository
 
-image:[Palimpsest-MPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"]
+image:https://img.shields.io/badge/license-MPL--2.0-blue[MPL-2.0,link="LICENSES/MPL-2.0.txt"] image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue[CC-BY-SA-4.0,link="LICENSES/CC-BY-SA-4.0.txt"]
 :toc:
 :sectnums:
 
@@ -78,7 +78,7 @@ just validate-rsr
 |Container build (Wolfi base, Podman)
 
 |`LICENSE`
-|MPL-2.0 (Palimpsest MPL)
+|MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 
 |`EXHIBIT-A-ETHICAL-USE.txt`
 |Ethical use guidelines (LICENSE Exhibit A)
diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc
index 2af3297..4be8d44 100644
--- a/docs/STATE-VISUALIZER.adoc
+++ b/docs/STATE-VISUALIZER.adoc
@@ -87,7 +87,7 @@ CONTAINER ECOSYSTEM (Phase 2)
 
 REPO INFRASTRUCTURE
   .machine_readable/                ██████████ 100%    STATE/META/ECOSYSTEM active
-  Governance & License              ██████████ 100%    PMPL & Ethical use verified
+  Governance & License              ██████████ 100%    MPL-2.0 & Ethical use verified
   Development Shells (Nix/Guix)     ██████████ 100%    Reproducible env stable
 
 ─────────────────────────────────────────────────────────────────────────────
diff --git a/src/interface/abi/Typedqliser/ABI/Foreign.idr b/src/interface/abi/Typedqliser/ABI/Foreign.idr
new file mode 100644
index 0000000..e3acb5d
--- /dev/null
+++ b/src/interface/abi/Typedqliser/ABI/Foreign.idr
@@ -0,0 +1,76 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Foreign Function Interface declarations for TypedQLiser.
+|||
+||| C-compatible entry points implemented in the Zig FFI layer
+||| (src/interface/ffi/src/main.zig). Each safe wrapper maps the raw C result
+||| code back to the `Result` type from the ABI.
+
+module Typedqliser.ABI.Foreign
+
+import Typedqliser.ABI.Types
+import Typedqliser.ABI.Layout
+
+%default total
+
+||| Initialise the TypedQLiser proof engine; returns a context pointer.
+export
+%foreign "C:typedqliser_init,libtypedqliser"
+prim__init : PrimIO Bits64
+
+export
+init : IO (Maybe Handle)
+init = do
+  ptr <- primIO prim__init
+  pure (createHandle ptr)
+
+||| Release the proof engine context.
+export
+%foreign "C:typedqliser_free,libtypedqliser"
+prim__free : Bits64 -> PrimIO ()
+
+export
+free : Handle -> IO ()
+free h = primIO (prim__free (handlePtr h))
+
+||| Check a query (null-terminated C string) against a schema, up to the
+||| requested level. Returns a C result code.
+export
+%foreign "C:typedqliser_check_query,libtypedqliser"
+prim__checkQuery : Bits64 -> String -> Bits32 -> PrimIO Bits32
+
+export
+checkQuery : Handle -> (query : String) -> (level : Bits32) -> IO (Either Result ())
+checkQuery h query level = do
+  rc <- primIO (prim__checkQuery (handlePtr h) query level)
+  pure $ case rc of
+    0 => Right ()
+    2 => Left InvalidQuery
+    3 => Left SchemaError
+    _ => Left Error
+
+||| Highest safety level the last checked query achieved (0 if none).
+export
+%foreign "C:typedqliser_certificate_level,libtypedqliser"
+prim__certificateLevel : Bits64 -> PrimIO Bits32
+
+export
+certificateLevel : Handle -> IO Nat
+certificateLevel h = do
+  n <- primIO (prim__certificateLevel (handlePtr h))
+  pure (cast n)
+
+||| Library version string.
+export
+%foreign "C:typedqliser_version,libtypedqliser"
+prim__version : PrimIO Bits64
+
+export
+version : IO String
+version = do
+  ptr <- primIO prim__version
+  pure (prim__getString ptr)
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
diff --git a/src/interface/abi/Typedqliser/ABI/Layout.idr b/src/interface/abi/Typedqliser/ABI/Layout.idr
new file mode 100644
index 0000000..a421aad
--- /dev/null
+++ b/src/interface/abi/Typedqliser/ABI/Layout.idr
@@ -0,0 +1,122 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Memory-layout proofs for the TypedQLiser ABI.
+|||
+||| The proof certificate descriptor crosses the Zig/C FFI boundary; this module
+||| pins its field layout and proves it is C-ABI aligned.
+
+module Typedqliser.ABI.Layout
+
+import Typedqliser.ABI.Types
+import Data.Vect
+import Data.So
+import Data.Nat
+import Decidable.Equality
+
+%default total
+
+public export
+paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
+paddingFor offset alignment =
+  if offset `mod` alignment == 0
+    then 0
+    else minus alignment (offset `mod` alignment)
+
+public export
+alignUp : (size : Nat) -> (alignment : Nat) -> Nat
+alignUp size alignment = size + paddingFor size alignment
+
+||| `m = k * n` — n divides m.
+public export
+data Divides : Nat -> Nat -> Type where
+  DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
+
+||| Sound divisibility decision: returns a real witness when n divides m.
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z _ = Nothing
+decDivides (S k) m =
+  let q = m `div` (S k) in
+  case decEq m (q * (S k)) of
+    Yes prf => Just (DivideBy q prf)
+    No _ => Nothing
+
+public export
+record Field where
+  constructor MkField
+  name : String
+  offset : Nat
+  size : Nat
+  alignment : Nat
+
+public export
+record StructLayout where
+  constructor MkStructLayout
+  fields : Vect k Field
+  totalSize : Nat
+  alignment : Nat
+  {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
+  {auto 0 aligned : Divides alignment totalSize}
+
+||| The proof-certificate descriptor as it crosses the FFI (40 bytes, 8-aligned).
+public export
+certificateDescLayout : StructLayout
+certificateDescLayout =
+  MkStructLayout
+    [ MkField "query_hash_ptr" 0 8 8
+    , MkField "schema_ver_ptr" 8 8 8
+    , MkField "max_level" 16 4 4
+    , MkField "num_proofs" 20 4 4
+    , MkField "proofs_ptr" 24 8 8
+    , MkField "result_code" 32 4 4
+    , MkField "padding" 36 4 4
+    ]
+    40
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}
+
+||| Every field offset in a layout is correctly aligned.
+public export
+data FieldsAligned : Vect len Field -> Type where
+  NoFields : FieldsAligned []
+  ConsField :
+    (f : Field) ->
+    (rest : Vect len Field) ->
+    Divides f.alignment f.offset ->
+    FieldsAligned rest ->
+    FieldsAligned (f :: rest)
+
+||| Decide field alignment, building a real witness from per-field divisibility.
+public export
+decFieldsAligned : (fs : Vect len Field) -> Maybe (FieldsAligned fs)
+decFieldsAligned [] = Just NoFields
+decFieldsAligned (f :: fs) =
+  case decDivides f.alignment f.offset of
+    Nothing => Nothing
+    Just dvd => case decFieldsAligned fs of
+                  Nothing => Nothing
+                  Just rest => Just (ConsField f fs dvd rest)
+
+public export
+data CABICompliant : StructLayout -> Type where
+  CABIOk : (layout : StructLayout) -> FieldsAligned layout.fields -> CABICompliant layout
+
+||| Verify a layout against the C-ABI alignment rules; real proof or error.
+public export
+checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
+checkCABI layout =
+  case decFieldsAligned layout.fields of
+    Just prf => Right (CABIOk layout prf)
+    Nothing => Left "Field offsets are not correctly aligned for the C ABI"
+
+||| Decide whether a field lies within a struct's byte bounds (honest Maybe;
+||| the property is false for an arbitrary field, so it is decided not asserted).
+public export
+offsetInBounds : (layout : StructLayout) -> (f : Field) ->
+                 Maybe (So (f.offset + f.size <= layout.totalSize))
+offsetInBounds layout f =
+  case choose (f.offset + f.size <= layout.totalSize) of
+    Left ok => Just ok
+    Right _ => Nothing
diff --git a/src/interface/abi/Typedqliser/ABI/Proofs.idr b/src/interface/abi/Typedqliser/ABI/Proofs.idr
new file mode 100644
index 0000000..19d9592
--- /dev/null
+++ b/src/interface/abi/Typedqliser/ABI/Proofs.idr
@@ -0,0 +1,92 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked proofs over the TypedQLiser ABI.
+|||
+||| These are propositional statements the Idris2 type checker must discharge at
+||| compile time — not runtime tests. If the certificate descriptor were
+||| misaligned, a level ordinal wrong, the status encoding off, or a "complete"
+||| certificate admitted a non-Proven level, this module would fail to typecheck.
+
+module Typedqliser.ABI.Proofs
+
+import Typedqliser.ABI.Types
+import Typedqliser.ABI.Layout
+import Data.So
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- The certificate descriptor is provably C-ABI compliant.
+--------------------------------------------------------------------------------
+
+||| Every field offset in the certificate descriptor divides its alignment:
+||| 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4.
+export
+certificateDescCompliant : CABICompliant Layout.certificateDescLayout
+certificateDescCompliant =
+  CABIOk Layout.certificateDescLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 9 Refl)
+     NoFields)))))))
+
+--------------------------------------------------------------------------------
+-- Level ordinals + cumulative ordering.
+--------------------------------------------------------------------------------
+
+||| ParseSafe is level 1 (the floor).
+export
+parseSafeIsOne : levelNat ParseSafe = 1
+parseSafeIsOne = Refl
+
+||| LinearSafe is level 10 (the ceiling).
+export
+linearSafeIsTen : levelNat LinearSafe = 10
+linearSafeIsTen = Refl
+
+||| Cumulativity is reflected in the ordering: the top level dominates every
+||| other. A query at LinearSafe has therefore discharged InjectionFree.
+export
+linearDominatesInjectionFree : So (levelDominates LinearSafe InjectionFree)
+linearDominatesInjectionFree = Oh
+
+||| The ordering is *not* symmetric: InjectionFree does not dominate LinearSafe.
+export
+injectionFreeBelowLinear : So (not (levelDominates InjectionFree LinearSafe))
+injectionFreeBelowLinear = Oh
+
+--------------------------------------------------------------------------------
+-- Proof-status encoding the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+export
+provenIsZero : statusToInt Proven = 0
+provenIsZero = Refl
+
+export
+timeoutIsThree : statusToInt Timeout = 3
+timeoutIsThree = Refl
+
+--------------------------------------------------------------------------------
+-- Certificate completeness (non-vacuous).
+--------------------------------------------------------------------------------
+
+||| A certificate whose ten levels are all Proven is complete. The obligation is
+||| real: see `incompleteRejected` for the negative side.
+export
+tenAllProven : CertifiedComplete (replicate 10 Proven)
+tenAllProven = Complete Oh
+
+||| A certificate with one Refuted level is NOT all-proven — witnessing that
+||| `CertifiedComplete`'s obligation `So (allProven v)` is not vacuously true
+||| (there is no `Complete` for this vector).
+export
+incompleteNotAllProven :
+  So (not (allProven [Proven, Proven, Refuted, Proven]))
+incompleteNotAllProven = Oh
diff --git a/src/interface/abi/Typedqliser/ABI/Types.idr b/src/interface/abi/Typedqliser/ABI/Types.idr
new file mode 100644
index 0000000..b7c19fc
--- /dev/null
+++ b/src/interface/abi/Typedqliser/ABI/Types.idr
@@ -0,0 +1,174 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| ABI Type Definitions for TypedQLiser.
+|||
+||| Models the ten cumulative type-safety levels a query may achieve, the
+||| per-level proof status, and the proof certificate that crosses the FFI
+||| boundary. The levels are cumulative: a query certified at level N has
+||| satisfied the obligations of every level 1..N.
+
+module Typedqliser.ABI.Types
+
+import Data.Bits
+import Data.So
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Platform
+--------------------------------------------------------------------------------
+
+public export
+data Platform = Linux | Windows | MacOS | BSD | WASM
+
+||| Default build platform (overridden by the codegen/build layer).
+public export
+thisPlatform : Platform
+thisPlatform = Linux
+
+--------------------------------------------------------------------------------
+-- The ten type-safety levels
+--------------------------------------------------------------------------------
+
+||| The ten cumulative type-safety levels (see src/abi/mod.rs).
+public export
+data SafetyLevel : Type where
+  ParseSafe     : SafetyLevel  -- 1: total parser produces Right ast
+  SchemaBound   : SafetyLevel  -- 2: all references resolve in the schema
+  TypeCompat    : SafetyLevel  -- 3: operand types compatible
+  NullSafe      : SafetyLevel  -- 4: nullable paths explicitly handled
+  InjectionFree : SafetyLevel  -- 5: no string interpolation in structure
+  ResultTyped   : SafetyLevel  -- 6: return type statically known
+  CardinalSafe  : SafetyLevel  -- 7: result cardinality bounded
+  EffectTracked : SafetyLevel  -- 8: side-effects declared and verified
+  TemporalSafe  : SafetyLevel  -- 9: time-dependent predicates valid
+  LinearSafe    : SafetyLevel  -- 10: resources consumed exactly once
+
+||| The 1-based ordinal of a level. This is the cumulative ordering: a query
+||| at level `levelNat l` has discharged every obligation with a smaller ordinal.
+public export
+levelNat : SafetyLevel -> Nat
+levelNat ParseSafe     = 1
+levelNat SchemaBound   = 2
+levelNat TypeCompat    = 3
+levelNat NullSafe      = 4
+levelNat InjectionFree = 5
+levelNat ResultTyped   = 6
+levelNat CardinalSafe  = 7
+levelNat EffectTracked = 8
+levelNat TemporalSafe  = 9
+levelNat LinearSafe    = 10
+
+public export
+Eq SafetyLevel where
+  a == b = levelNat a == levelNat b
+
+||| `a` is at least as strong as `b` when its ordinal dominates. Cumulativity
+||| means achieving `a` entails every level `b` with `levelDominates a b`.
+public export
+levelDominates : SafetyLevel -> SafetyLevel -> Bool
+levelDominates a b = levelNat b <= levelNat a
+
+--------------------------------------------------------------------------------
+-- Per-level proof status
+--------------------------------------------------------------------------------
+
+public export
+data ProofStatus = Proven | Refuted | Skipped | Timeout
+
+public export
+Eq ProofStatus where
+  Proven  == Proven  = True
+  Refuted == Refuted = True
+  Skipped == Skipped = True
+  Timeout == Timeout = True
+  _       == _       = False
+
+||| C encoding for the proof status (must match the Zig FFI).
+public export
+statusToInt : ProofStatus -> Bits32
+statusToInt Proven  = 0
+statusToInt Refuted = 1
+statusToInt Skipped = 2
+statusToInt Timeout = 3
+
+--------------------------------------------------------------------------------
+-- FFI result codes
+--------------------------------------------------------------------------------
+
+public export
+data Result : Type where
+  Ok           : Result
+  Error        : Result
+  InvalidQuery : Result
+  SchemaError  : Result
+  NullPointer  : Result
+
+public export
+resultToInt : Result -> Bits32
+resultToInt Ok           = 0
+resultToInt Error        = 1
+resultToInt InvalidQuery = 2
+resultToInt SchemaError  = 3
+resultToInt NullPointer  = 4
+
+--------------------------------------------------------------------------------
+-- Opaque handle
+--------------------------------------------------------------------------------
+
+public export
+data Handle : Type where
+  MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
+
+||| Safely build a handle; a null pointer yields Nothing. `choose` supplies the
+||| real `So (ptr /= 0)` witness for the non-null branch.
+public export
+createHandle : Bits64 -> Maybe Handle
+createHandle ptr =
+  case choose (ptr /= 0) of
+    Left ok => Just (MkHandle ptr {nonNull = ok})
+    Right _ => Nothing
+
+public export
+handlePtr : Handle -> Bits64
+handlePtr (MkHandle ptr) = ptr
+
+--------------------------------------------------------------------------------
+-- Proof certificate
+--------------------------------------------------------------------------------
+
+||| One level's proof outcome.
+public export
+record LevelProof where
+  constructor MkLevelProof
+  level  : SafetyLevel
+  status : ProofStatus
+
+||| A certificate: the highest level reached, and the per-level outcomes.
+public export
+record ProofCertificate (n : Nat) where
+  constructor MkProofCertificate
+  maxLevel : SafetyLevel
+  proofs   : Vect n ProofStatus
+
+||| Decidable predicate: every level in the vector was Proven.
+public export
+allProven : Vect n ProofStatus -> Bool
+allProven v = all (== Proven) v
+
+||| Proof that a certificate is *complete*: every one of its `n` levels is
+||| `Proven`. A single `Refuted`/`Skipped`/`Timeout` makes this uninhabited —
+||| the obligation `So (allProven v)` is genuine, not a free assertion.
+public export
+data CertifiedComplete : Vect n ProofStatus -> Type where
+  Complete : {v : Vect n ProofStatus} -> So (allProven v) -> CertifiedComplete v
+
+||| Decide certificate completeness, returning a real proof or Nothing.
+public export
+checkComplete : (v : Vect n ProofStatus) -> Maybe (CertifiedComplete v)
+checkComplete v =
+  case choose (allProven v) of
+    Left ok => Just (Complete ok)
+    Right _ => Nothing
diff --git a/src/interface/abi/typedqliser-abi.ipkg b/src/interface/abi/typedqliser-abi.ipkg
new file mode 100644
index 0000000..47afffd
--- /dev/null
+++ b/src/interface/abi/typedqliser-abi.ipkg
@@ -0,0 +1,11 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Idris2 package for the TypedQLiser ABI formal proofs.
+-- Build/check with:  idris2 --build typedqliser-abi.ipkg   (from src/interface/abi/)
+package typedqliser-abi
+
+sourcedir = "."
+
+modules = Typedqliser.ABI.Types
+        , Typedqliser.ABI.Layout
+        , Typedqliser.ABI.Foreign
+        , Typedqliser.ABI.Proofs