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 73f5db0..d9013fb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,6 +16,11 @@ Thumbs.db
 /_build/
 /build/
 /dist/
+
+# Idris2 proof build artifacts (any nested build/ dir + TTC output)
+**/build/
+*.ttc
+*.ttm
 /out/
 
 # Dependencies
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 d078d13..abf79b4 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 = "Meta-framework that generates new -iser projects from a target language interop description"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/iseriser"
 keywords = ["meta-framework", "code-generation", "language-interop", "scaffolding"]
 categories = ["command-line-utilities", "development-tools"]
diff --git a/Justfile b/Justfile
index d7888d1..c71d2f8 100644
--- a/Justfile
+++ b/Justfile
@@ -14,6 +14,11 @@ build:
 test:
     cargo test
 
+# Type-check the Idris2 ABI formal proofs (requires idris2 >= 0.7.0)
+proofs:
+    cd src/interface/abi && idris2 --build iseriser-abi.ipkg
+    @echo "Idris2 ABI proofs type-check cleanly"
+
 # Run clippy lints
 lint:
     cargo clippy -- -D warnings
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 2c4bd84..f343852 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/README.md b/README.md
index 3eac4f4..51267dd 100644
--- a/README.md
+++ b/README.md
@@ -3,8 +3,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
-[![License: MPL-2.0](https://img.shields.io/badge/license-PMPL--1.0--or--later-blue)](LICENSE) ![Palimpsest
-Covenant](https://img.shields.io/badge/Palimpsest-Covenant-purple) ![29
+[![License: MPL-2.0](https://img.shields.io/badge/license-MPL--2.0-blue)](LICENSE) [![Docs: CC-BY-SA-4.0](https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue)](LICENSES/CC-BY-SA-4.0.txt) ![29
 repos](https://img.shields.io/badge/-iser_family-29_repos-brightgreen)
 ![Idris2 ABI](https://img.shields.io/badge/ABI-Idris2-red) ![Zig
 FFI](https://img.shields.io/badge/FFI-Zig-orange)
@@ -303,9 +302,7 @@ Hypatia neurosymbolic scanning.
 
 # License
 
-SPDX-License-Identifier: `MPL-2.0`
+Code is licensed under `MPL-2.0`; documentation under `CC-BY-SA-4.0`.
+Full licence texts are in [`LICENSES/`](LICENSES/).
 
 Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-
-Licensed under the [Palimpsest
-License](https://github.com/hyperpolymath/palimpsest-license).
diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml
index 1df8ae5..b30c962 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/Foreign.idr b/src/interface/abi/Iseriser/ABI/Foreign.idr
similarity index 100%
rename from src/interface/abi/Foreign.idr
rename to src/interface/abi/Iseriser/ABI/Foreign.idr
diff --git a/src/interface/abi/Iseriser/ABI/Layout.idr b/src/interface/abi/Iseriser/ABI/Layout.idr
new file mode 100644
index 0000000..37805cc
--- /dev/null
+++ b/src/interface/abi/Iseriser/ABI/Layout.idr
@@ -0,0 +1,215 @@
+-- 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 Iseriser
+
+module Iseriser.ABI.Layout
+
+import Iseriser.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
+
+||| Proof that alignment divides aligned size: `m = k * n`.
+public export
+data Divides : Nat -> Nat -> Type where
+  DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
+
+||| Sound decision procedure for divisibility. Returns a genuine
+||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
+||| Division by zero is undecidable here and yields Nothing.
+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
+
+||| Sound divisibility check for an aligned size. The general theorem
+||| "alignUp size align is always divisible by align" needs div/mod lemmas
+||| from Data.Nat and is tracked as residual proof work; here we *decide* it
+||| via `decDivides`, which returns a genuine witness when it holds. For the
+||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`).
+||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot
+||| typecheck for symbolic inputs.)
+public export
+alignUpDivides : (size : Nat) -> (align : Nat) ->
+                 Maybe (Divides align (alignUp size align))
+alignUpDivides size align = decDivides align (alignUp size align)
+
+public export
+record Field where
+  constructor MkField
+  name : String
+  offset : Nat
+  size : Nat
+  alignment : Nat
+
+public export
+nextFieldOffset : Field -> Nat
+nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
+
+public export
+record StructLayout where
+  constructor MkStructLayout
+  fields : Vect n Field
+  totalSize : Nat
+  alignment : Nat
+  {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
+  {auto 0 aligned : Divides alignment totalSize}
+
+public export
+calcStructSize : Vect k Field -> Nat -> Nat
+calcStructSize [] align = 0
+calcStructSize (f :: fs) align =
+  let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
+      lastSize = foldr (\field, _ => field.size) f.size fs
+   in alignUp (lastOffset + lastSize) align
+
+||| C-compatible layout for the language model data passed through FFI.
+public export
+languageModelDataLayout : StructLayout
+languageModelDataLayout =
+  MkStructLayout
+    [ MkField "name_ptr" 0 8 8
+    , MkField "name_len" 8 4 4
+    , MkField "num_features" 12 4 4
+    , MkField "features_ptr" 16 8 8
+    , MkField "target" 24 4 4
+    , MkField "padding" 28 4 4
+    ]
+    32
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
+
+||| C-compatible layout for template data passed to the expansion engine.
+public export
+templateDataLayout : StructLayout
+templateDataLayout =
+  MkStructLayout
+    [ MkField "template_ptr" 0 8 8
+    , MkField "template_len" 8 4 4
+    , MkField "padding1" 12 4 4
+    , MkField "output_ptr" 16 8 8
+    , MkField "output_len" 24 4 4
+    , MkField "is_lang_spec" 28 4 4
+    ]
+    32
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
+
+||| C-compatible layout for the generation context handle.
+public export
+generationContextLayout : StructLayout
+generationContextLayout =
+  MkStructLayout
+    [ MkField "model_ptr" 0 8 8
+    , MkField "templates_ptr" 8 8 8
+    , MkField "num_templates" 16 4 4
+    , MkField "artifacts_count" 20 4 4
+    , MkField "output_dir_ptr" 24 8 8
+    , MkField "output_dir_len" 32 4 4
+    , MkField "initialized" 36 4 4
+    , MkField "error_code" 40 4 4
+    , MkField "padding" 44 4 4
+    ]
+    48
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 6 Refl}
+
+||| Proof that every field offset in a layout is correctly aligned.
+public export
+data FieldsAligned : Vect k Field -> Type where
+  NoFields : FieldsAligned []
+  ConsField :
+    (f : Field) ->
+    (rest : Vect k Field) ->
+    Divides f.alignment f.offset ->
+    FieldsAligned rest ->
+    FieldsAligned (f :: rest)
+
+||| Decide field alignment for every field, building a real `FieldsAligned`
+||| witness from per-field divisibility proofs.
+public export
+decFieldsAligned : (fs : Vect k 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)
+
+||| Proof that a struct layout follows C ABI alignment rules.
+public export
+data CABICompliant : StructLayout -> Type where
+  CABIOk :
+    (layout : StructLayout) ->
+    FieldsAligned layout.fields ->
+    CABICompliant layout
+
+||| Verify a layout against the C ABI alignment rules, returning a genuine
+||| `CABICompliant` proof (built from real per-field divisibility witnesses)
+||| or an error when some field offset is misaligned.
+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"
+
+||| Verify that all iseriser layouts are C-ABI compliant. This now fails
+||| (Left) if any concrete layout is misaligned, rather than asserting it.
+public export
+verifyAllLayouts : Either String ()
+verifyAllLayouts = do
+  _ <- checkCABI languageModelDataLayout
+  _ <- checkCABI templateDataLayout
+  _ <- checkCABI generationContextLayout
+  Right ()
+
+||| All 64-bit platforms (Linux, Windows, MacOS, BSD) use 8-byte pointers and
+||| 4-byte ints, so the LanguageModelData layout is identical across them.
+public export
+verifyLanguageModelPortability : Either String ()
+verifyLanguageModelPortability = Right ()
+
+||| Look up a field's offset by name in a layout.
+public export
+fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
+fieldOffset layout name =
+  case findIndex (\f => f.name == name) layout.fields of
+    Just idx => Just (finToNat idx, index idx layout.fields)
+    Nothing => Nothing
+
+||| Decide whether a field lies within a struct's byte bounds, returning a
+||| genuine proof when `offset + size <= totalSize`. The previous signature
+||| asserted this for *every* field unconditionally, which is false (a field
+||| need not belong to the layout); this honest version decides it.
+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/Iseriser/ABI/Proofs.idr b/src/interface/abi/Iseriser/ABI/Proofs.idr
new file mode 100644
index 0000000..b8db7ff
--- /dev/null
+++ b/src/interface/abi/Iseriser/ABI/Proofs.idr
@@ -0,0 +1,101 @@
+-- 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 iseriser ABI.
+|||
+||| These are not runtime tests — they are propositional statements the Idris2
+||| type checker must discharge at compile time. If any concrete ABI layout
+||| were misaligned, the result-code encoding wrong, or a decision procedure
+||| mis-defined, this module would fail to typecheck and the proof build would
+||| go red.
+|||
+||| The C-ABI compliance witnesses are built directly from per-field
+||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`).
+||| Multiplication reduces during type checking, so these are fully verified
+||| by the compiler; we avoid routing them through `Nat` division, which is a
+||| primitive that does not reduce at the type level.
+
+module Iseriser.ABI.Proofs
+
+import Iseriser.ABI.Types
+import Iseriser.ABI.Layout
+import Data.So
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- The concrete FFI struct layouts are provably C-ABI compliant.
+--------------------------------------------------------------------------------
+
+||| Every field offset in the LanguageModelData layout divides its alignment:
+||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
+export
+languageModelDataCompliant : CABICompliant Layout.languageModelDataLayout
+languageModelDataCompliant =
+  CABIOk languageModelDataLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+     NoFields))))))
+
+||| Every field offset in the TemplateData layout is aligned:
+||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
+export
+templateDataCompliant : CABICompliant Layout.templateDataLayout
+templateDataCompliant =
+  CABIOk templateDataLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+     NoFields))))))
+
+||| Every field offset in the GenerationContext layout is aligned:
+||| 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4, 40|4, 44|4.
+export
+generationContextCompliant : CABICompliant Layout.generationContextLayout
+generationContextCompliant =
+  CABIOk generationContextLayout
+    (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)
+    (ConsField _ _ (DivideBy 10 Refl)
+    (ConsField _ _ (DivideBy 11 Refl)
+     NoFields)))))))))
+
+--------------------------------------------------------------------------------
+-- Result-code round-trip: the encoding the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+export
+nullPointerIsFive : resultToInt NullPointer = 5
+nullPointerIsFive = Refl
+
+--------------------------------------------------------------------------------
+-- Generation completeness: the full required set is accepted; a short set isn't.
+--------------------------------------------------------------------------------
+
+||| The complete set of seven categories is recognised as complete.
+export
+fullSetComplete : So (allCategoriesPresent Types.requiredCategories)
+fullSetComplete = Oh
+
+||| A set missing RSRGovernance is correctly rejected as incomplete.
+export
+shortSetIncomplete : So (not (allCategoriesPresent
+  [CargoToml, RustSource, Idris2ABI, ZigFFI, CIWorkflows, Documentation]))
+shortSetIncomplete = Oh
diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Iseriser/ABI/Types.idr
similarity index 63%
rename from src/interface/abi/Types.idr
rename to src/interface/abi/Iseriser/ABI/Types.idr
index eecdf5c..408624f 100644
--- a/src/interface/abi/Types.idr
+++ b/src/interface/abi/Iseriser/ABI/Types.idr
@@ -15,6 +15,8 @@ module Iseriser.ABI.Types
 import Data.Bits
 import Data.So
 import Data.Vect
+import Data.String
+import Decidable.Equality
 
 %default total
 
@@ -26,12 +28,12 @@ import Data.Vect
 public export
 data Platform = Linux | Windows | MacOS | BSD | WASM
 
-||| Compile-time platform detection
+||| The platform this build targets. Defaults to Linux; the Rust/Zig build
+||| layer overrides this via the codegen target selection. (Previously a
+||| `%runElab` stub that required ElabReflection and did not compile.)
 public export
 thisPlatform : Platform
-thisPlatform =
-  %runElab do
-    pure Linux  -- Default, override with compiler flags
+thisPlatform = Linux
 
 --------------------------------------------------------------------------------
 -- Language Model Types
@@ -134,14 +136,32 @@ record GeneratedArtifact where
   ||| Size in bytes of the rendered content
   sizeBytes : Nat
 
-||| Proof that a generated artifact has all placeholders resolved.
-||| No `{{` or `}}` sequences remain in the content.
+||| Decidable predicate: the rendered content carries no unresolved
+||| Handlebars placeholder markers (`{{` opening or `}}` closing).
+public export
+noUnresolvedMarkers : GeneratedArtifact -> Bool
+noUnresolvedMarkers art =
+  not (isInfixOf "{{" art.content) && not (isInfixOf "}}" art.content)
+
+||| Proof that a generated artifact has all placeholders resolved: the
+||| content contains no `{{` or `}}` markers. This is a genuine obligation —
+||| `Resolved` cannot be constructed while template delimiters remain.
+||| (Previously `Resolved` carried no proof and was inhabited by anything.)
 public export
 data FullyResolved : GeneratedArtifact -> Type where
   Resolved : {art : GeneratedArtifact} ->
-    -- In a real implementation, this would search for unresolved markers
+    So (noUnresolvedMarkers art) ->
     FullyResolved art
 
+||| Decide whether an artifact is fully resolved, returning a real proof
+||| when it is and Nothing when unresolved markers remain.
+public export
+checkResolved : (art : GeneratedArtifact) -> Maybe (FullyResolved art)
+checkResolved art =
+  case choose (noUnresolvedMarkers art) of
+    Left ok => Just (Resolved ok)
+    Right _ => Nothing
+
 --------------------------------------------------------------------------------
 -- Result Codes
 --------------------------------------------------------------------------------
@@ -172,7 +192,9 @@ resultToInt TemplateError = 3
 resultToInt OutputError = 4
 resultToInt NullPointer = 5
 
-||| Results are decidably equal
+||| Results are decidably equal. The off-diagonal cases discharge the
+||| disequality explicitly; the previous `decEq _ _ = No absurd` did not
+||| compile (no `Uninhabited (x = y)` instance exists for these).
 public export
 DecEq Result where
   decEq Ok Ok = Yes Refl
@@ -181,7 +203,36 @@ DecEq Result where
   decEq TemplateError TemplateError = Yes Refl
   decEq OutputError OutputError = Yes Refl
   decEq NullPointer NullPointer = Yes Refl
-  decEq _ _ = No absurd
+  decEq Ok Error = No (\case Refl impossible)
+  decEq Ok InvalidLanguage = No (\case Refl impossible)
+  decEq Ok TemplateError = No (\case Refl impossible)
+  decEq Ok OutputError = No (\case Refl impossible)
+  decEq Ok NullPointer = No (\case Refl impossible)
+  decEq Error Ok = No (\case Refl impossible)
+  decEq Error InvalidLanguage = No (\case Refl impossible)
+  decEq Error TemplateError = No (\case Refl impossible)
+  decEq Error OutputError = No (\case Refl impossible)
+  decEq Error NullPointer = No (\case Refl impossible)
+  decEq InvalidLanguage Ok = No (\case Refl impossible)
+  decEq InvalidLanguage Error = No (\case Refl impossible)
+  decEq InvalidLanguage TemplateError = No (\case Refl impossible)
+  decEq InvalidLanguage OutputError = No (\case Refl impossible)
+  decEq InvalidLanguage NullPointer = No (\case Refl impossible)
+  decEq TemplateError Ok = No (\case Refl impossible)
+  decEq TemplateError Error = No (\case Refl impossible)
+  decEq TemplateError InvalidLanguage = No (\case Refl impossible)
+  decEq TemplateError OutputError = No (\case Refl impossible)
+  decEq TemplateError NullPointer = No (\case Refl impossible)
+  decEq OutputError Ok = No (\case Refl impossible)
+  decEq OutputError Error = No (\case Refl impossible)
+  decEq OutputError InvalidLanguage = No (\case Refl impossible)
+  decEq OutputError TemplateError = No (\case Refl impossible)
+  decEq OutputError NullPointer = No (\case Refl impossible)
+  decEq NullPointer Ok = No (\case Refl impossible)
+  decEq NullPointer Error = No (\case Refl impossible)
+  decEq NullPointer InvalidLanguage = No (\case Refl impossible)
+  decEq NullPointer TemplateError = No (\case Refl impossible)
+  decEq NullPointer OutputError = No (\case Refl impossible)
 
 --------------------------------------------------------------------------------
 -- Opaque Handles
@@ -193,11 +244,15 @@ public export
 data Handle : Type where
   MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
 
-||| Safely create a handle from a pointer value
+||| Safely create a handle from a pointer value. Uses `choose` to obtain a
+||| real `So (ptr /= 0)` witness for the non-null branch. (Previously
+||| `Just (MkHandle ptr)` left the `auto` proof unsolved and did not compile.)
 public export
 createHandle : Bits64 -> Maybe Handle
-createHandle 0 = Nothing
-createHandle ptr = Just (MkHandle ptr)
+createHandle ptr =
+  case choose (ptr /= 0) of
+    Left ok => Just (MkHandle ptr {nonNull = ok})
+    Right _ => Nothing
 
 ||| Extract pointer value from handle
 public export
@@ -250,14 +305,49 @@ data ArtifactCategory : Type where
   Documentation : ArtifactCategory
   RSRGovernance : ArtifactCategory
 
+||| Artifact categories are decidably equal — needed for membership checks.
+public export
+Eq ArtifactCategory where
+  CargoToml     == CargoToml     = True
+  RustSource    == RustSource    = True
+  Idris2ABI     == Idris2ABI     = True
+  ZigFFI        == ZigFFI        = True
+  CIWorkflows   == CIWorkflows   = True
+  Documentation == Documentation = True
+  RSRGovernance == RSRGovernance = True
+  _             == _             = False
+
+||| The seven categories every generated -iser repo must contain.
+public export
+requiredCategories : List ArtifactCategory
+requiredCategories =
+  [ CargoToml, RustSource, Idris2ABI, ZigFFI
+  , CIWorkflows, Documentation, RSRGovernance ]
+
+||| Decidable predicate: every required category appears in `cats`.
+public export
+allCategoriesPresent : List ArtifactCategory -> Bool
+allCategoriesPresent cats = all (\c => elem c cats) requiredCategories
+
 ||| Proof that a generation produced all required artifact categories.
+||| `AllCategoriesPresent` now carries a genuine obligation: each of the
+||| seven `requiredCategories` must be a member of the produced list.
+||| (Previously the constructor proved nothing.)
 public export
 data GenerationComplete : List ArtifactCategory -> Type where
-  AllCategoriesPresent :
-    (cats : List ArtifactCategory) ->
-    -- In a real implementation, this would check membership of all 7 categories
+  AllCategoriesPresent : {cats : List ArtifactCategory} ->
+    So (allCategoriesPresent cats) ->
     GenerationComplete cats
 
+||| Decide generation completeness, returning a real proof when all seven
+||| categories are present and Nothing when any is missing.
+public export
+checkComplete : (cats : List ArtifactCategory) -> Maybe (GenerationComplete cats)
+checkComplete cats =
+  case choose (allCategoriesPresent cats) of
+    Left ok => Just (AllCategoriesPresent ok)
+    Right _ => Nothing
+
 --------------------------------------------------------------------------------
 -- Verification
 --------------------------------------------------------------------------------
@@ -279,7 +369,6 @@ namespace Verify
   verifyArtifacts : List GeneratedArtifact -> Either String ()
   verifyArtifacts [] = Right ()
   verifyArtifacts (a :: as) =
-    -- Check that artifact path and content are non-empty
     if length (outputPath a) == 0
       then Left "Artifact has empty output path"
       else verifyArtifacts as
diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Layout.idr
deleted file mode 100644
index 1c9f390..0000000
--- a/src/interface/abi/Layout.idr
+++ /dev/null
@@ -1,240 +0,0 @@
--- 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 Iseriser
-|||
-||| This module provides formal proofs about memory layout for the data
-||| structures that flow through the iseriser generation pipeline.
-|||
-||| Key structures: LanguageModelData (the parsed language description),
-||| TemplateData (the expanded template before writing), and
-||| GenerationContext (the state held during a generation run).
-
-module Iseriser.ABI.Layout
-
-import Iseriser.ABI.Types
-import Data.Vect
-import Data.So
-
-%default total
-
---------------------------------------------------------------------------------
--- Alignment Utilities
---------------------------------------------------------------------------------
-
-||| Calculate padding needed for alignment
-public export
-paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
-paddingFor offset alignment =
-  if offset `mod` alignment == 0
-    then 0
-    else alignment - (offset `mod` alignment)
-
-||| Round up to next alignment boundary
-public export
-alignUp : (size : Nat) -> (alignment : Nat) -> Nat
-alignUp size alignment =
-  size + paddingFor size alignment
-
-||| Proof that alignment divides aligned size
-public export
-data Divides : Nat -> Nat -> Type where
-  DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
-
-||| Proof that alignUp produces aligned result
-public export
-alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
-alignUpCorrect size align prf =
-  DivideBy ((size + paddingFor size align) `div` align) Refl
-
---------------------------------------------------------------------------------
--- Struct Field Layout
---------------------------------------------------------------------------------
-
-||| A field in a C-compatible struct with its offset and size
-public export
-record Field where
-  constructor MkField
-  name : String
-  offset : Nat
-  size : Nat
-  alignment : Nat
-
-||| Calculate the offset of the next field after this one
-public export
-nextFieldOffset : Field -> Nat
-nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
-
-||| A struct layout is a vector of fields with correctness proofs
-public export
-record StructLayout where
-  constructor MkStructLayout
-  fields : Vect n Field
-  totalSize : Nat
-  alignment : Nat
-  {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
-  {auto 0 aligned : Divides alignment totalSize}
-
-||| Calculate total struct size including padding
-public export
-calcStructSize : Vect n Field -> Nat -> Nat
-calcStructSize [] align = 0
-calcStructSize (f :: fs) align =
-  let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
-      lastSize = foldr (\field, _ => field.size) f.size fs
-   in alignUp (lastOffset + lastSize) align
-
---------------------------------------------------------------------------------
--- LanguageModelData Layout
---------------------------------------------------------------------------------
-
-||| C-compatible layout for the language model data passed through FFI.
-||| This struct is what the Zig FFI receives when a generation is requested.
-|||
-||| Fields:
-|||   name_ptr:    pointer to language name string (8 bytes, offset 0)
-|||   name_len:    length of language name (4 bytes, offset 8)
-|||   num_features: count of type system features (4 bytes, offset 12)
-|||   features_ptr: pointer to features array (8 bytes, offset 16)
-|||   target:      compilation target enum (4 bytes, offset 24)
-|||   padding:     alignment padding (4 bytes, offset 28)
-public export
-languageModelDataLayout : StructLayout
-languageModelDataLayout =
-  MkStructLayout
-    [ MkField "name_ptr" 0 8 8        -- Pointer to name string
-    , MkField "name_len" 8 4 4        -- Length of name
-    , MkField "num_features" 12 4 4   -- Feature count
-    , MkField "features_ptr" 16 8 8   -- Pointer to features array
-    , MkField "target" 24 4 4         -- CompilationTarget enum value
-    , MkField "padding" 28 4 4        -- Alignment padding to 32 bytes
-    ]
-    32   -- Total size: 32 bytes
-    8    -- Alignment: 8 bytes (pointer-aligned)
-
---------------------------------------------------------------------------------
--- TemplateData Layout
---------------------------------------------------------------------------------
-
-||| C-compatible layout for template data passed to the expansion engine.
-|||
-||| Fields:
-|||   template_ptr:  pointer to template content (8 bytes, offset 0)
-|||   template_len:  length of template content (4 bytes, offset 8)
-|||   output_ptr:    pointer to output path string (8 bytes, offset 16)
-|||   output_len:    length of output path (4 bytes, offset 24)
-|||   is_lang_spec:  boolean: language-specific template (4 bytes, offset 28)
-public export
-templateDataLayout : StructLayout
-templateDataLayout =
-  MkStructLayout
-    [ MkField "template_ptr" 0 8 8    -- Pointer to template content
-    , MkField "template_len" 8 4 4    -- Template content length
-    , MkField "padding1" 12 4 4       -- Alignment padding
-    , MkField "output_ptr" 16 8 8     -- Pointer to output path
-    , MkField "output_len" 24 4 4     -- Output path length
-    , MkField "is_lang_spec" 28 4 4   -- Language-specific flag (0 or 1)
-    ]
-    32   -- Total size: 32 bytes
-    8    -- Alignment: 8 bytes
-
---------------------------------------------------------------------------------
--- GenerationContext Layout
---------------------------------------------------------------------------------
-
-||| C-compatible layout for the generation context handle.
-||| This is the internal state held by the Zig FFI during generation.
-|||
-||| Fields:
-|||   model_ptr:      pointer to parsed LanguageModelData (8 bytes, offset 0)
-|||   templates_ptr:  pointer to template array (8 bytes, offset 8)
-|||   num_templates:  count of templates (4 bytes, offset 16)
-|||   artifacts_count: number of artifacts generated so far (4 bytes, offset 20)
-|||   output_dir_ptr: pointer to output directory path (8 bytes, offset 24)
-|||   output_dir_len: length of output directory path (4 bytes, offset 32)
-|||   initialized:    whether context is ready (4 bytes, offset 36)
-|||   error_code:     last error code (4 bytes, offset 40)
-|||   padding:        alignment padding (4 bytes, offset 44)
-public export
-generationContextLayout : StructLayout
-generationContextLayout =
-  MkStructLayout
-    [ MkField "model_ptr" 0 8 8         -- Pointer to language model
-    , MkField "templates_ptr" 8 8 8      -- Pointer to template array
-    , MkField "num_templates" 16 4 4     -- Template count
-    , MkField "artifacts_count" 20 4 4   -- Generated artifact count
-    , MkField "output_dir_ptr" 24 8 8    -- Output directory path
-    , MkField "output_dir_len" 32 4 4    -- Output directory path length
-    , MkField "initialized" 36 4 4       -- Initialization flag
-    , MkField "error_code" 40 4 4        -- Last error code
-    , MkField "padding" 44 4 4           -- Alignment padding
-    ]
-    48   -- Total size: 48 bytes
-    8    -- Alignment: 8 bytes
-
---------------------------------------------------------------------------------
--- C ABI Compliance
---------------------------------------------------------------------------------
-
-||| Proof that a struct layout follows C ABI rules
-public export
-data CABICompliant : StructLayout -> Type where
-  CABIOk :
-    (layout : StructLayout) ->
-    FieldsAligned layout.fields ->
-    CABICompliant layout
-
-||| Proof that field offsets are correctly aligned
-public export
-data FieldsAligned : Vect n Field -> Type where
-  NoFields : FieldsAligned []
-  ConsField :
-    (f : Field) ->
-    (rest : Vect n Field) ->
-    Divides f.alignment f.offset ->
-    FieldsAligned rest ->
-    FieldsAligned (f :: rest)
-
-||| Verify layout follows C ABI
-public export
-checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
-checkCABI layout =
-  Right (CABIOk layout ?fieldsAlignedProof)
-
---------------------------------------------------------------------------------
--- Platform-Specific Layout Verification
---------------------------------------------------------------------------------
-
-||| Verify that LanguageModelData has the same layout on all 64-bit platforms
-public export
-verifyLanguageModelPortability : Either String ()
-verifyLanguageModelPortability =
-  -- All 64-bit platforms use 8-byte pointers and 4-byte ints,
-  -- so the layout is identical on Linux, Windows, MacOS, BSD
-  Right ()
-
-||| Verify that all iseriser layouts are self-consistent
-public export
-verifyAllLayouts : Either String ()
-verifyAllLayouts = do
-  _ <- checkCABI languageModelDataLayout
-  _ <- checkCABI templateDataLayout
-  _ <- checkCABI generationContextLayout
-  Right ()
-
---------------------------------------------------------------------------------
--- Field Offset Queries
---------------------------------------------------------------------------------
-
-||| Look up a field's offset by name in a layout
-public export
-fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field)
-fieldOffset layout name =
-  case findIndex (\f => f.name == name) layout.fields of
-    Just idx => Just (finToNat idx ** index idx layout.fields)
-    Nothing => Nothing
-
-||| Proof that a field offset is within struct bounds
-public export
-offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
-offsetInBounds layout f = ?offsetInBoundsProof
diff --git a/src/interface/abi/iseriser-abi.ipkg b/src/interface/abi/iseriser-abi.ipkg
new file mode 100644
index 0000000..4304c93
--- /dev/null
+++ b/src/interface/abi/iseriser-abi.ipkg
@@ -0,0 +1,11 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Idris2 package for the iseriser ABI formal proofs.
+-- Build/check with:  idris2 --build iseriser-abi.ipkg   (from src/interface/abi/)
+package iseriser-abi
+
+sourcedir = "."
+
+modules = Iseriser.ABI.Types
+        , Iseriser.ABI.Layout
+        , Iseriser.ABI.Foreign
+        , Iseriser.ABI.Proofs
diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc
index 1ae324d..1041ac7 100644
--- a/verification/proofs/README.adoc
+++ b/verification/proofs/README.adoc
@@ -1 +1,52 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = Proofs Unit
+:toc:
+
+The iseriser formal proofs live with the ABI they constrain, under
+`src/interface/abi/Iseriser/ABI/`, and are built as a single Idris2 package.
+
+== What is proven
+
+`Types.idr`::
+  Core ABI types plus genuine proof obligations: `FullyResolved` (no `{{`/`}}`
+  markers remain in rendered content), `GenerationComplete` (all seven required
+  artifact categories present), and a total `DecEq Result`.
+
+`Layout.idr`::
+  C-ABI struct layouts with a sound `decDivides` divisibility decision
+  procedure, `decFieldsAligned`, and `checkCABI`. The three concrete FFI
+  layouts (`languageModelDataLayout`, `templateDataLayout`,
+  `generationContextLayout`) carry explicit alignment witnesses.
+
+`Proofs.idr`::
+  Machine-checked theorems (not runtime tests). The type checker must discharge
+  them at compile time:
+  * `languageModelDataCompliant`, `templateDataCompliant`,
+    `generationContextCompliant` — each concrete struct layout is provably
+    C-ABI aligned (built from per-field `offset = k * alignment` witnesses).
+  * `okIsZero`, `nullPointerIsFive` — the `Result` → C-int encoding the Zig FFI
+    depends on.
+  * `fullSetComplete`, `shortSetIncomplete` — completeness predicate accepts the
+    full category set and rejects a short one.
+
+== Running the proofs
+
+[source,sh]
+----
+just proofs
+# or directly:
+cd src/interface/abi && idris2 --build iseriser-abi.ipkg
+----
+
+Requires Idris2 >= 0.7.0. A clean build means every theorem above is verified;
+any regression (a misaligned offset, a wrong result code, a broken decision
+procedure) turns the build red.
+
+== Residual proof work
+
+* The general theorem "`alignUp size align` is always divisible by `align`" is
+  currently *decided* (`alignUpDivides`, via `decDivides`) rather than proven for
+  all inputs; a closed proof needs the `Data.Nat` div/mod lemmas. The concrete
+  layouts that matter are proven outright, so this is a generality gap, not a
+  soundness gap.