diff --git a/.gitignore b/.gitignore
index 73f5db0..f4cfd5c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/
diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Dafniser/ABI/Foreign.idr
similarity index 100%
rename from src/interface/abi/Foreign.idr
rename to src/interface/abi/Dafniser/ABI/Foreign.idr
diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Dafniser/ABI/Layout.idr
similarity index 72%
rename from src/interface/abi/Layout.idr
rename to src/interface/abi/Dafniser/ABI/Layout.idr
index 83ca9f5..f644c07 100644
--- a/src/interface/abi/Layout.idr
+++ b/src/interface/abi/Dafniser/ABI/Layout.idr
@@ -18,6 +18,8 @@ module Dafniser.ABI.Layout
 import Dafniser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -31,24 +33,39 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
 paddingFor offset alignment =
   if offset `mod` alignment == 0
     then 0
-    else alignment - (offset `mod` alignment)
+    else minus alignment (offset `mod` 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
 
+||| Sound decision procedure: does `n` divide `m`?
+||| For n = S j, compute the quotient q = m `div` (S j) and check that
+||| m = q * (S j) holds on the nose.  Returns a real `Divides` witness, or
+||| Nothing when the candidate quotient does not check out (or when n = 0).
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z _ = Nothing
+decDivides (S j) m =
+  let q = m `div` (S j) in
+  case decEq m (q * (S j)) of
+    Yes prf => Just (DivideBy q prf)
+    No _ => Nothing
+
 ||| Round up to next alignment boundary
 public export
 alignUp : (size : Nat) -> (alignment : Nat) -> Nat
 alignUp size alignment =
   size + paddingFor size alignment
 
-||| Proof that alignUp produces aligned result
+||| Decide whether `alignUp size align` is a multiple of `align`.
+||| A universally-quantified claim here would need a full division lemma; we
+||| instead produce the real `Divides` witness by computation via `decDivides`
+||| (returns Nothing only in the degenerate `align = 0` case).
 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
+decAlignUp : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
+decAlignUp size align = decDivides align (alignUp size align)
 
 --------------------------------------------------------------------------------
 -- Struct Field Layout
@@ -80,7 +97,7 @@ record StructLayout where
 
 ||| Calculate total struct size with padding
 public export
-calcStructSize : Vect n Field -> Nat -> Nat
+calcStructSize : Vect k Field -> Nat -> Nat
 calcStructSize [] align = 0
 calcStructSize (f :: fs) align =
   let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -89,23 +106,26 @@ calcStructSize (f :: fs) align =
 
 ||| Proof that field offsets are correctly aligned
 public export
-data FieldsAligned : Vect n Field -> Type where
+data FieldsAligned : Vect k Field -> Type where
   NoFields : FieldsAligned []
   ConsField :
     (f : Field) ->
-    (rest : Vect n Field) ->
+    (rest : Vect k Field) ->
     Divides f.alignment f.offset ->
     FieldsAligned rest ->
     FieldsAligned (f :: rest)
 
 ||| Verify a struct layout is valid
 public export
-verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
+verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
 verifyLayout fields align =
-  let size = calcStructSize fields align
-   in case decSo (size >= sum (map (\f => f.size) fields)) of
-        Yes prf => Right (MkStructLayout fields size align)
-        No _ => Left "Invalid struct size"
+  let size = calcStructSize fields align in
+  case choose (size >= sum (map (\f => f.size) fields)) of
+    Right _ => Left "Invalid struct size"
+    Left szOk =>
+      case decDivides align size of
+        Nothing => Left "Total size is not a multiple of the alignment"
+        Just dvd => Right (MkStructLayout fields size align {sizeCorrect = szOk} {aligned = dvd})
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -136,11 +156,27 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
+||| Sound decision procedure over a whole field vector: are all field
+||| offsets divisible by their declared alignment?  Builds the real
+||| FieldsAligned witness when it succeeds.
+public export
+decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
+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)
+
 ||| Check if layout follows C ABI
 public export
 checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
 checkCABI layout =
-  Right (CABIOk layout ?fieldsAlignedProof)
+  case decFieldsAligned layout.fields of
+    Just prf => Right (CABIOk layout prf)
+    Nothing => Left "Struct fields are not correctly aligned for the C ABI"
 
 --------------------------------------------------------------------------------
 -- Dafniser-Specific Layouts
@@ -159,6 +195,8 @@ preconditionLayout =
     ]
     24  -- Total size: 24 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}
 
 ||| Layout for the Postcondition record (identical to Precondition).
 public export
@@ -171,6 +209,8 @@ postconditionLayout =
     ]
     24
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}
 
 ||| Layout for the LoopInvariant record.
 ||| Fields: functionName (ptr), loopIndex (u64), expression (ptr), description (ptr)
@@ -185,6 +225,8 @@ loopInvariantLayout =
     ]
     32  -- Total size: 32 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
 
 ||| Layout for the GhostVariable record.
 ||| Fields: name (ptr), dafnyType (ptr), initialiser (ptr), scope (ptr)
@@ -199,6 +241,8 @@ ghostVariableLayout =
     ]
     32
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
 
 ||| Layout for the Lemma record.
 ||| Fields: name (ptr), requires (ptr to list), ensures (ptr to list),
@@ -215,6 +259,8 @@ lemmaLayout =
     ]
     40
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}
 
 ||| Layout for the VerificationResult tagged union.
 ||| Tag (u32) + padding + payload (function name ptr + detail ptr/u64)
@@ -230,6 +276,8 @@ verificationResultLayout =
     ]
     32
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
 
 ||| Layout for the SpecTree top-level record.
 ||| Fields: moduleName (ptr), target (u32), functions (ptr to list),
@@ -247,6 +295,8 @@ specTreeLayout =
     ]
     40
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
@@ -260,7 +310,13 @@ fieldOffset layout name =
     Just idx => Just (finToNat idx ** index idx layout.fields)
     Nothing => Nothing
 
-||| Proof that field offset is within struct bounds
+||| Decide whether a field offset is within struct bounds.
+||| A universally-quantified `So (...)` return type would be unsound (it is
+||| false in general — a field may overflow the declared total size), so this
+||| returns a `Maybe` witness produced by `choose`.
 public export
-offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
-offsetInBounds layout f = ?offsetInBoundsProof
+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/Dafniser/ABI/Proofs.idr b/src/interface/abi/Dafniser/ABI/Proofs.idr
new file mode 100644
index 0000000..db80ab3
--- /dev/null
+++ b/src/interface/abi/Dafniser/ABI/Proofs.idr
@@ -0,0 +1,126 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked ABI theorems for Dafniser.
+|||
+||| Every concrete `StructLayout` declared in `Dafniser.ABI.Layout` is shown
+||| to be C-ABI-compliant: each field's offset is an exact multiple of its
+||| declared alignment.  The witnesses are built DIRECTLY (one `DivideBy k Refl`
+||| per field, where `offset = k * alignment`) because multiplication reduces
+||| during typechecking whereas division does not — so we never route these
+||| through the `decFieldsAligned` decision procedure.
+|||
+||| We also pin the FFI result-code encoding.
+
+module Dafniser.ABI.Proofs
+
+import Dafniser.ABI.Types
+import Dafniser.ABI.Layout
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- C-ABI compliance of every concrete layout
+--------------------------------------------------------------------------------
+
+||| Precondition layout: offsets 0, 8, 16 are 0*8, 1*8, 2*8.
+export
+preconditionCompliant : CABICompliant Layout.preconditionLayout
+preconditionCompliant =
+  CABIOk Layout.preconditionLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+     NoFields)))
+
+||| Postcondition layout: identical shape to Precondition.
+export
+postconditionCompliant : CABICompliant Layout.postconditionLayout
+postconditionCompliant =
+  CABIOk Layout.postconditionLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+     NoFields)))
+
+||| LoopInvariant layout: offsets 0, 8, 16, 24 over alignment 8.
+export
+loopInvariantCompliant : CABICompliant Layout.loopInvariantLayout
+loopInvariantCompliant =
+  CABIOk Layout.loopInvariantLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+     NoFields))))
+
+||| GhostVariable layout: offsets 0, 8, 16, 24 over alignment 8.
+export
+ghostVariableCompliant : CABICompliant Layout.ghostVariableLayout
+ghostVariableCompliant =
+  CABIOk Layout.ghostVariableLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+     NoFields))))
+
+||| Lemma layout: offsets 0, 8, 16, 24, 32 over alignment 8.
+export
+lemmaCompliant : CABICompliant Layout.lemmaLayout
+lemmaCompliant =
+  CABIOk Layout.lemmaLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+     NoFields)))))
+
+||| VerificationResult layout: tag(0,align4)=0*4, _pad(4,align4)=1*4,
+||| functionName(8,align8)=1*8, detail(16,align8)=2*8, witness(24,align8)=3*8.
+export
+verificationResultCompliant : CABICompliant Layout.verificationResultLayout
+verificationResultCompliant =
+  CABIOk Layout.verificationResultLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+     NoFields)))))
+
+||| SpecTree layout: moduleName(0,a8)=0*8, target(8,a4)=2*4, _pad(12,a4)=3*4,
+||| functions(16,a8)=2*8, moduleGhosts(24,a8)=3*8, moduleLemmas(32,a8)=4*8.
+export
+specTreeCompliant : CABICompliant Layout.specTreeLayout
+specTreeCompliant =
+  CABIOk Layout.specTreeLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+     NoFields))))))
+
+--------------------------------------------------------------------------------
+-- Result-code encoding
+--------------------------------------------------------------------------------
+
+||| The success code is zero, as the C ABI expects.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The error codes are pairwise distinct from success: Error encodes to 1.
+export
+errorIsOne : resultToInt Error = 1
+errorIsOne = Refl
+
+||| The five result codes are encoded as the contiguous range 0..4.
+||| NullPointer is the largest, encoding to 4.
+export
+nullPointerIsFour : resultToInt NullPointer = 4
+nullPointerIsFour = Refl
diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Dafniser/ABI/Types.idr
similarity index 73%
rename from src/interface/abi/Types.idr
rename to src/interface/abi/Dafniser/ABI/Types.idr
index 90db4f9..9357828 100644
--- a/src/interface/abi/Types.idr
+++ b/src/interface/abi/Dafniser/ABI/Types.idr
@@ -20,6 +20,7 @@ module Dafniser.ABI.Types
 import Data.Bits
 import Data.So
 import Data.Vect
+import Decidable.Equality
 
 %default total
 
@@ -35,10 +36,7 @@ data Platform = Linux | Windows | MacOS | BSD | WASM
 ||| This will be set during compilation based on target
 public export
 thisPlatform : Platform
-thisPlatform =
-  %runElab do
-    -- Platform detection logic
-    pure Linux  -- Default, override with compiler flags
+thisPlatform = Linux  -- Default; override with compiler flags / build config
 
 --------------------------------------------------------------------------------
 -- Core Result Types
@@ -76,7 +74,26 @@ DecEq Result where
   decEq InvalidParam InvalidParam = Yes Refl
   decEq OutOfMemory OutOfMemory = Yes Refl
   decEq NullPointer NullPointer = Yes Refl
-  decEq _ _ = No absurd
+  decEq Ok Error = No (\case Refl impossible)
+  decEq Ok InvalidParam = No (\case Refl impossible)
+  decEq Ok OutOfMemory = No (\case Refl impossible)
+  decEq Ok NullPointer = No (\case Refl impossible)
+  decEq Error Ok = No (\case Refl impossible)
+  decEq Error InvalidParam = No (\case Refl impossible)
+  decEq Error OutOfMemory = No (\case Refl impossible)
+  decEq Error NullPointer = No (\case Refl impossible)
+  decEq InvalidParam Ok = No (\case Refl impossible)
+  decEq InvalidParam Error = No (\case Refl impossible)
+  decEq InvalidParam OutOfMemory = No (\case Refl impossible)
+  decEq InvalidParam NullPointer = No (\case Refl impossible)
+  decEq OutOfMemory Ok = No (\case Refl impossible)
+  decEq OutOfMemory Error = No (\case Refl impossible)
+  decEq OutOfMemory InvalidParam = No (\case Refl impossible)
+  decEq OutOfMemory NullPointer = No (\case Refl impossible)
+  decEq NullPointer Ok = No (\case Refl impossible)
+  decEq NullPointer Error = No (\case Refl impossible)
+  decEq NullPointer InvalidParam = No (\case Refl impossible)
+  decEq NullPointer OutOfMemory = No (\case Refl impossible)
 
 --------------------------------------------------------------------------------
 -- Opaque Handles
@@ -92,8 +109,10 @@ data Handle : Type where
 ||| Returns Nothing if pointer is null
 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
@@ -229,7 +248,26 @@ DecEq DafnyTarget where
   decEq Go Go = Yes Refl
   decEq Python Python = Yes Refl
   decEq JavaScript JavaScript = Yes Refl
-  decEq _ _ = No absurd
+  decEq CSharp Java = No (\case Refl impossible)
+  decEq CSharp Go = No (\case Refl impossible)
+  decEq CSharp Python = No (\case Refl impossible)
+  decEq CSharp JavaScript = No (\case Refl impossible)
+  decEq Java CSharp = No (\case Refl impossible)
+  decEq Java Go = No (\case Refl impossible)
+  decEq Java Python = No (\case Refl impossible)
+  decEq Java JavaScript = No (\case Refl impossible)
+  decEq Go CSharp = No (\case Refl impossible)
+  decEq Go Java = No (\case Refl impossible)
+  decEq Go Python = No (\case Refl impossible)
+  decEq Go JavaScript = No (\case Refl impossible)
+  decEq Python CSharp = No (\case Refl impossible)
+  decEq Python Java = No (\case Refl impossible)
+  decEq Python Go = No (\case Refl impossible)
+  decEq Python JavaScript = No (\case Refl impossible)
+  decEq JavaScript CSharp = No (\case Refl impossible)
+  decEq JavaScript Java = No (\case Refl impossible)
+  decEq JavaScript Go = No (\case Refl impossible)
+  decEq JavaScript Python = No (\case Refl impossible)
 
 --------------------------------------------------------------------------------
 -- Specification Tree
@@ -245,7 +283,7 @@ record FunctionSpec where
   ||| Return type (Dafny syntax)
   returnType : String
   ||| Parameter names and types (Dafny syntax)
-  parameters : List (String, String)
+  params : List (String, String)
   ||| Preconditions (`requires` clauses)
   preconditions : List Precondition
   ||| Postconditions (`ensures` clauses)
@@ -306,44 +344,59 @@ ptrSize MacOS = 64
 ptrSize BSD = 64
 ptrSize WASM = 32
 
-||| Pointer type for platform
+||| Pointer-sized integer type for a platform.
+||| (Idris2 cannot match on `Type` to recover a width, so this is a plain
+||| dispatch on the platform rather than a `Bits (ptrSize p)` application,
+||| which is ill-typed — `Bits` is an interface, not a width-indexed type.)
 public export
-CPtr : Platform -> Type -> Type
-CPtr p _ = Bits (ptrSize p)
+CPtr : Platform -> Type
+CPtr Linux   = Bits64
+CPtr Windows = Bits64
+CPtr MacOS   = Bits64
+CPtr BSD     = Bits64
+CPtr WASM    = Bits32
 
 --------------------------------------------------------------------------------
--- Memory Layout Proofs
+-- Memory Layout (scalar size / alignment)
 --------------------------------------------------------------------------------
 
-||| Proof that a type has a specific size
+||| The C scalar kinds whose size/alignment this ABI reasons about.
+||| Using an explicit tag (rather than pattern-matching on `Type`, which Idris2
+||| forbids for type-level functions) keeps `cSizeOf`/`cAlignOf` total and sound.
 public export
-data HasSize : Type -> Nat -> Type where
-  SizeProof : {0 t : Type} -> {n : Nat} -> HasSize t n
-
-||| Proof that a type has a specific alignment
-public export
-data HasAlignment : Type -> Nat -> Type where
-  AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n
-
-||| Size of C types (platform-specific)
+data CScalar : Type where
+  ||| C `int` (platform-dependent, 32-bit on every supported target)
+  ScInt : CScalar
+  ||| C `size_t` (pointer-width)
+  ScSize : CScalar
+  ||| Fixed 32-bit word
+  ScBits32 : CScalar
+  ||| Fixed 64-bit word
+  ScBits64 : CScalar
+  ||| IEEE-754 double
+  ScDouble : CScalar
+  ||| Raw pointer (pointer-width)
+  ScPtr : CScalar
+
+||| Size in bytes of a C scalar on a given platform.
 public export
-cSizeOf : (p : Platform) -> (t : Type) -> Nat
-cSizeOf p (CInt _) = 4
-cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4
-cSizeOf p Bits32 = 4
-cSizeOf p Bits64 = 8
-cSizeOf p Double = 8
-cSizeOf p _ = ptrSize p `div` 8
-
-||| Alignment of C types (platform-specific)
+cSizeOf : (p : Platform) -> CScalar -> Nat
+cSizeOf _ ScInt    = 4
+cSizeOf p ScSize   = ptrSize p `div` 8
+cSizeOf _ ScBits32 = 4
+cSizeOf _ ScBits64 = 8
+cSizeOf _ ScDouble = 8
+cSizeOf p ScPtr    = ptrSize p `div` 8
+
+||| Alignment in bytes of a C scalar on a given platform.
 public export
-cAlignOf : (p : Platform) -> (t : Type) -> Nat
-cAlignOf p (CInt _) = 4
-cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4
-cAlignOf p Bits32 = 4
-cAlignOf p Bits64 = 8
-cAlignOf p Double = 8
-cAlignOf p _ = ptrSize p `div` 8
+cAlignOf : (p : Platform) -> CScalar -> Nat
+cAlignOf _ ScInt    = 4
+cAlignOf p ScSize   = ptrSize p `div` 8
+cAlignOf _ ScBits32 = 4
+cAlignOf _ ScBits64 = 8
+cAlignOf _ ScDouble = 8
+cAlignOf p ScPtr    = ptrSize p `div` 8
 
 --------------------------------------------------------------------------------
 -- FFI Declarations (bridging to Zig)
diff --git a/src/interface/abi/dafniser-abi.ipkg b/src/interface/abi/dafniser-abi.ipkg
new file mode 100644
index 0000000..74ca50a
--- /dev/null
+++ b/src/interface/abi/dafniser-abi.ipkg
@@ -0,0 +1,9 @@
+-- SPDX-License-Identifier: MPL-2.0
+package dafniser-abi
+
+sourcedir = "."
+
+modules = Dafniser.ABI.Types,
+          Dafniser.ABI.Layout,
+          Dafniser.ABI.Foreign,
+          Dafniser.ABI.Proofs