diff --git a/verification/verification/0.1-AI-MANIFEST.a2ml b/verification/verification/0.1-AI-MANIFEST.a2ml
deleted file mode 100644
index 39b370f..0000000
--- a/verification/verification/0.1-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,27 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "verification-pillar"
-level: 1
-parent: "../0-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  Primary verification pillar. Contains evidence for correctness,
-  performance, formal proofs, randomized testing, and aerospace-grade
-  high-assurance metrics (MC/DC coverage, traceability, safety cases).
-
-canonical_locations:
-  tests: "tests/"
-  benchmarks: "benchmarks/"
-  proofs: "proofs/"
-  fuzzing: "fuzzing/"
-  simulations: "simulations/"
-  coverage: "coverage/"
-  traceability: "traceability/"
-  safety_case: "safety_case/"
-
-invariants:
-  - "Evidence MUST be reproducible and documented"
-  - "High-assurance deployments MUST satisfy traceability and safety_case requirements"
diff --git a/verification/verification/README.adoc b/verification/verification/README.adoc
deleted file mode 100644
index efa7fb2..0000000
--- a/verification/verification/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Verification Pillar
diff --git a/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml b/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index 6416309..0000000
--- a/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,11 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "benches-pillar"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  Benches pillar.
diff --git a/verification/verification/benchmarks/README.adoc b/verification/verification/benchmarks/README.adoc
deleted file mode 100644
index beb83cd..0000000
--- a/verification/verification/benchmarks/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Benchmarks Unit
diff --git a/verification/verification/coverage/0.2-AI-MANIFEST.a2ml b/verification/verification/coverage/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index fc15bd3..0000000
--- a/verification/verification/coverage/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,12 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "verification-unit-coverage"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  High-assurance verification unit for coverage. 
-  Critical for safety-of-life and aerospace-grade deployment standards.
diff --git a/verification/verification/coverage/README.adoc b/verification/verification/coverage/README.adoc
deleted file mode 100644
index c10a6ac..0000000
--- a/verification/verification/coverage/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Coverage Unit
diff --git a/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml b/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index 79c4fef..0000000
--- a/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,11 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "fuzzing-unit"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  Fuzzing unit for high-rigor verification.
diff --git a/verification/verification/fuzzing/README.adoc b/verification/verification/fuzzing/README.adoc
deleted file mode 100644
index b07ea68..0000000
--- a/verification/verification/fuzzing/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Fuzzing Unit
diff --git a/verification/verification/proofs/0.2-AI-MANIFEST.a2ml b/verification/verification/proofs/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index 0e5666f..0000000
--- a/verification/verification/proofs/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,11 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "verification-unit-proofs"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  Sub-unit focusing on proofs.
diff --git a/verification/verification/proofs/README.adoc b/verification/verification/proofs/README.adoc
deleted file mode 100644
index 520f5e9..0000000
--- a/verification/verification/proofs/README.adoc
+++ /dev/null
@@ -1,60 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Formal Verification Proofs
-
-This directory contains formal proofs organised by proof assistant.
-
-== Directory Structure
-
-[source]
-----
-proofs/
-├── idris2/          # Idris2 proofs (ABI, dependent types)
-│   ├── ABI/         # ABI-specific proofs (mandatory)
-│   │   ├── Pointers.idr    # Non-null pointer safety
-│   │   ├── Layout.idr      # Memory layout correctness
-│   │   ├── Platform.idr    # Platform type size proofs
-│   │   ├── Foreign.idr     # FFI return type proofs
-│   │   └── Compliance.idr  # C ABI compliance
-│   └── Types.idr    # Core data type well-formedness
-├── lean4/           # Lean4 proofs (algebra, lattices)
-│   └── ApiTypes.lean
-├── agda/            # Agda proofs (induction, metatheory)
-│   └── Properties.agda
-├── coq/             # Coq proofs (type systems, compilation)
-│   └── TypeSafety.v
-└── tlaplus/         # TLA+ specs (distributed protocols)
-    └── StateMachine.tla
-----
-
-== Verification Commands
-
-[source,bash]
-----
-just proof-check-all       # Run all proof checkers
-just proof-check-idris2    # Idris2 only
-just proof-check-lean4     # Lean4 only
-just proof-check-agda      # Agda only
-just proof-check-coq       # Coq only
-----
-
-== Banned Patterns
-
-The following MUST NOT appear in any proof file:
-
-- `believe_me` (Idris2)
-- `assert_total` (Idris2)
-- `postulate` (Idris2/Agda)
-- `sorry` (Lean4)
-- `Admitted` (Coq)
-- `unsafeCoerce` (Haskell)
-
-CI enforces this via `panic-attack assail --proofs-only`.
-
-== Adding New Proofs
-
-1. Choose the appropriate prover (see PROOF-NEEDS.md)
-2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory
-3. Ensure `%default total` (Idris2) or equivalent
-4. Run the verification command
-5. Update PROOF-STATUS.md
diff --git a/verification/verification/proofs/agda/Properties.agda b/verification/verification/proofs/agda/Properties.agda
deleted file mode 100644
index 90e4c3c..0000000
--- a/verification/verification/proofs/agda/Properties.agda
+++ /dev/null
@@ -1,37 +0,0 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
---
--- Agda Proof Template: Inductive and coinductive properties
--- Replace with your project's domain-specific proofs.
--- All proofs must be total (no postulate, no {-# TERMINATING #-}).
-
-module Properties where
-
-open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_)
-open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans)
-open import Data.List using (List; []; _∷_; length; _++_)
-open import Data.List.Properties using (length-++ )
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans)
-
--- Example: Proof that list append preserves total length
--- Replace with your project's domain proofs.
-
-append-length : ∀ {A : Set} (xs ys : List A) →
-  length (xs ++ ys) ≡ length xs + length ys
-append-length xs ys = length-++ xs
-
--- Example: Monotonicity proof template
--- Use for state machines, confidence scores, trust levels
-record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where
-  field
-    preserves : ∀ {x y} → x ≤A y → f x ≤A f y
-
--- Example: Idempotence proof template
--- Use for normalisation, deduplication, formatting
-record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where
-  field
-    idem : ∀ (x : A) → f (f x) ≡A f x
-
--- Example: Natural number successor is monotone
-suc-monotone : Monotone _≤_ suc
-suc-monotone = record { preserves = s≤s }
diff --git a/verification/verification/proofs/coq/TypeSafety.v b/verification/verification/proofs/coq/TypeSafety.v
deleted file mode 100644
index c2ec6eb..0000000
--- a/verification/verification/proofs/coq/TypeSafety.v
+++ /dev/null
@@ -1,73 +0,0 @@
-(* SPDX-License-Identifier: PMPL-1.0-or-later *)
-(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *)
-(*
-   Coq Proof Template: Type system soundness
-   Replace with your project's type system proofs.
-   All proofs must be complete — NO Admitted allowed.
-*)
-
-Require Import Coq.Lists.List.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Bool.Bool.
-Import ListNotations.
-
-(** * Example: Simple expression language with type safety *)
-(** Replace this entire section with your project's type system. *)
-
-(** Types *)
-Inductive ty : Type :=
-  | TyNat  : ty
-  | TyBool : ty.
-
-(** Expressions *)
-Inductive expr : Type :=
-  | EConst : nat -> expr
-  | ETrue  : expr
-  | EFalse : expr
-  | EPlus  : expr -> expr -> expr
-  | EEq    : expr -> expr -> expr.
-
-(** Values *)
-Inductive value : Type :=
-  | VNat  : nat -> value
-  | VBool : bool -> value.
-
-(** Typing relation *)
-Inductive has_type : expr -> ty -> Prop :=
-  | T_Const : forall n, has_type (EConst n) TyNat
-  | T_True  : has_type ETrue TyBool
-  | T_False : has_type EFalse TyBool
-  | T_Plus  : forall e1 e2,
-      has_type e1 TyNat -> has_type e2 TyNat ->
-      has_type (EPlus e1 e2) TyNat
-  | T_Eq    : forall e1 e2,
-      has_type e1 TyNat -> has_type e2 TyNat ->
-      has_type (EEq e1 e2) TyBool.
-
-(** Evaluation *)
-Inductive eval : expr -> value -> Prop :=
-  | E_Const : forall n, eval (EConst n) (VNat n)
-  | E_True  : eval ETrue (VBool true)
-  | E_False : eval EFalse (VBool false)
-  | E_Plus  : forall e1 e2 n1 n2,
-      eval e1 (VNat n1) -> eval e2 (VNat n2) ->
-      eval (EPlus e1 e2) (VNat (n1 + n2))
-  | E_Eq    : forall e1 e2 n1 n2,
-      eval e1 (VNat n1) -> eval e2 (VNat n2) ->
-      eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)).
-
-(** Value typing *)
-Definition value_has_type (v : value) (t : ty) : Prop :=
-  match v, t with
-  | VNat _, TyNat   => True
-  | VBool _, TyBool => True
-  | _, _            => False
-  end.
-
-(** Type soundness: well-typed expressions evaluate to well-typed values *)
-Theorem type_soundness : forall e t v,
-  has_type e t -> eval e v -> value_has_type v t.
-Proof.
-  intros e t v Htype Heval.
-  induction Htype; inversion Heval; subst; simpl; auto.
-Qed.
diff --git a/verification/verification/proofs/idris2/ABI/Compliance.idr b/verification/verification/proofs/idris2/ABI/Compliance.idr
deleted file mode 100644
index b94a5db..0000000
--- a/verification/verification/proofs/idris2/ABI/Compliance.idr
+++ /dev/null
@@ -1,41 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- ABI Proof: C ABI compliance
--- Proves that struct layouts are C ABI compliant.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module ABI.Compliance
-
-import ABI.Layout
-import ABI.Platform
-
-%default total
-
-||| Evidence that every field in a layout is correctly aligned.
-public export
-data AllFieldsAligned : List StructField -> Type where
-  AFANil  : AllFieldsAligned []
-  AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs)
-
-||| Evidence that every field is within the struct bounds.
-public export
-data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where
-  AFBNil  : AllFieldsInBounds size []
-  AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs)
-
-||| A struct layout is C ABI compliant when:
-||| 1. All fields are aligned to their natural alignment
-||| 2. All fields are within bounds of the struct size
-||| 3. The struct size is a multiple of the struct alignment
-public export
-record CABICompliant (layout : StructLayout) where
-  constructor MkCompliant
-  fieldsAligned  : AllFieldsAligned (layoutFields layout)
-  fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout)
-  sizeAligned    : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0
-
-||| An empty struct is trivially compliant (size=1, alignment=1).
-export
-emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1)
-emptyStructCompliant = MkCompliant AFANil AFBNil Refl
diff --git a/verification/verification/proofs/idris2/ABI/Foreign.idr b/verification/verification/proofs/idris2/ABI/Foreign.idr
deleted file mode 100644
index 1e550dd..0000000
--- a/verification/verification/proofs/idris2/ABI/Foreign.idr
+++ /dev/null
@@ -1,53 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- ABI Proof: FFI function return type proofs
--- Proves that all FFI functions return expected types.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module ABI.Foreign
-
-%default total
-
-||| Result type for FFI operations.
-||| All FFI functions must return through this type.
-public export
-data FFIResult : Type -> Type where
-  FFISuccess : (value : a) -> FFIResult a
-  FFIError   : (code : Int) -> (msg : String) -> FFIResult a
-
-||| Proof that FFIResult is a functor (map preserves structure).
-export
-mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b
-mapFFIResult f (FFISuccess value) = FFISuccess (f value)
-mapFFIResult f (FFIError code msg) = FFIError code msg
-
-||| Proof that mapping identity preserves the result.
-export
-mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r
-mapIdPreserves (FFISuccess value) = Refl
-mapIdPreserves (FFIError code msg) = Refl
-
-||| An FFI function specification: name, argument types, return type.
-public export
-record FFISpec where
-  constructor MkFFISpec
-  ffiName : String
-  ffiReturnType : Type
-
-||| Proof that an FFI spec has a specific return type.
-||| Use this to verify at compile time that FFI functions return the
-||| types we expect across the C ABI boundary.
-public export
-FFIReturns : FFISpec -> Type -> Type
-FFIReturns spec ty = ffiReturnType spec = ty
-
-||| C calling convention marker.
-||| Proofs about calling convention compatibility.
-public export
-data CallingConv = CDecl | StdCall | FastCall
-
-||| All hyperpolymath FFI uses CDecl.
-public export
-defaultCallingConv : CallingConv
-defaultCallingConv = CDecl
diff --git a/verification/verification/proofs/idris2/ABI/Layout.idr b/verification/verification/proofs/idris2/ABI/Layout.idr
deleted file mode 100644
index 9040a5e..0000000
--- a/verification/verification/proofs/idris2/ABI/Layout.idr
+++ /dev/null
@@ -1,63 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- ABI Proof: Memory layout correctness
--- Proves struct size, alignment, and padding properties.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module ABI.Layout
-
-%default total
-
-||| Witness that a type has a known size in bytes at compile time.
-public export
-interface HasSize (ty : Type) where
-  sizeOf : Nat
-
-||| Witness that a type has a known alignment in bytes.
-public export
-interface HasAlignment (ty : Type) where
-  alignOf : Nat
-
-||| Calculate padding needed to reach the next aligned offset.
-||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0
-public export
-paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat
-paddingFor offset alignment = let r = modNatNZ offset alignment ok
-                              in case r of
-                                   Z => Z
-                                   (S _) => minus alignment r
-
-||| Proof that an offset with zero remainder needs zero padding.
-export
-alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} ->
-                      modNatNZ n a ok = 0 -> paddingFor n a = 0
-alignedNeedsPadding n a prf = rewrite prf in Refl
-
-||| A field within a struct, carrying its offset and size.
-public export
-record StructField where
-  constructor MkField
-  fieldName : String
-  fieldOffset : Nat
-  fieldSize : Nat
-  fieldAlignment : Nat
-
-||| Proof that a field is correctly aligned within a struct.
-public export
-FieldAligned : StructField -> Type
-FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0
-
-||| Proof that a field does not overflow past a given struct size.
-public export
-FieldInBounds : (structSize : Nat) -> StructField -> Type
-FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz
-
-||| A struct layout is a list of fields with a total size.
-public export
-record StructLayout where
-  constructor MkLayout
-  layoutName : String
-  layoutFields : List StructField
-  layoutSize : Nat
-  layoutAlignment : Nat
diff --git a/verification/verification/proofs/idris2/ABI/Platform.idr b/verification/verification/proofs/idris2/ABI/Platform.idr
deleted file mode 100644
index a8d6b94..0000000
--- a/verification/verification/proofs/idris2/ABI/Platform.idr
+++ /dev/null
@@ -1,63 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- ABI Proof: Platform-specific type size proofs
--- Proves that C type sizes are correct per platform.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module ABI.Platform
-
-%default total
-
-||| Supported target platforms for ABI verification.
-public export
-data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64
-              | Windows64 | FreeBSD64 | WASM32
-
-||| Pointer size in bytes for each platform.
-public export
-ptrSize : Platform -> Nat
-ptrSize WASM32 = 4
-ptrSize _ = 8
-
-||| C `int` size in bytes.
-public export
-cIntSize : Platform -> Nat
-cIntSize _ = 4
-
-||| C `size_t` size in bytes (matches pointer size).
-public export
-cSizeT : Platform -> Nat
-cSizeT = ptrSize
-
-||| Proof that size_t always equals pointer size on all platforms.
-export
-sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p
-sizeTEqPtrSize _ = Refl
-
-||| Proof that pointer size is always 4 or 8 bytes.
-export
-ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8)
-ptrSizeValid WASM32 = Left Refl
-ptrSizeValid Linux64 = Right Refl
-ptrSizeValid LinuxARM64 = Right Refl
-ptrSizeValid MacOS64 = Right Refl
-ptrSizeValid MacOSARM64 = Right Refl
-ptrSizeValid Windows64 = Right Refl
-ptrSizeValid FreeBSD64 = Right Refl
-
-||| Proof that C int is always 4 bytes on all platforms.
-export
-cIntAlways4 : (p : Platform) -> cIntSize p = 4
-cIntAlways4 _ = Refl
-
-||| Proof that pointer size is always at least 4 bytes.
-export
-ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p)
-ptrSizeAtLeast4 WASM32 = lteRefl
-ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
-ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
-ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
-ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
-ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
-ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl)))
diff --git a/verification/verification/proofs/idris2/ABI/Pointers.idr b/verification/verification/proofs/idris2/ABI/Pointers.idr
deleted file mode 100644
index 31b6c5f..0000000
--- a/verification/verification/proofs/idris2/ABI/Pointers.idr
+++ /dev/null
@@ -1,52 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- ABI Proof: Non-null pointer safety
--- Template proof — customise for your project's pointer types.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module ABI.Pointers
-
-import Data.So
-
-%default total
-
-||| A pointer value that has been proven non-null.
-||| The `So` constraint carries a compile-time witness that `ptr /= 0`.
-public export
-record SafePtr where
-  constructor MkSafePtr
-  ptr : Bits64
-  {auto 0 nonNull : So (ptr /= 0)}
-
-||| Proof that SafePtr can never hold a null (zero) value.
-||| This is enforced by the `So` constraint in the record.
-export
-safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0)
-safePtrNeverNull sp = sp.nonNull
-
-||| Wrap a raw pointer with a runtime null check.
-||| Returns Nothing if the pointer is null.
-export
-checkPtr : (raw : Bits64) -> Maybe SafePtr
-checkPtr 0 = Nothing
-checkPtr raw = case choose (raw /= 0) of
-  Left prf => Just (MkSafePtr raw)
-  Right _ => Nothing
-
-||| Proof that checkPtr 0 always returns Nothing.
-export
-checkPtrZeroIsNothing : checkPtr 0 = Nothing
-checkPtrZeroIsNothing = Refl
-
-||| An opaque handle backed by a non-null pointer.
-||| Use this for FFI resource handles (file descriptors, sockets, etc.).
-public export
-record Handle (tag : String) where
-  constructor MkHandle
-  safePtr : SafePtr
-
-||| Proof that two handles with equal pointers are equal.
-export
-handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2
-handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl
diff --git a/verification/verification/proofs/idris2/Types.idr b/verification/verification/proofs/idris2/Types.idr
deleted file mode 100644
index cc7cce8..0000000
--- a/verification/verification/proofs/idris2/Types.idr
+++ /dev/null
@@ -1,38 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- Typing Proof: Core data type well-formedness
--- Template — replace with your project's core types.
--- All proofs MUST be constructive (no believe_me, no assert_total).
-
-module Types
-
-%default total
-
-||| Example: A bounded natural number (0 to max).
-||| Replace with your project's core types.
-public export
-record Bounded (max : Nat) where
-  constructor MkBounded
-  value : Nat
-  {auto 0 inBounds : LTE value max}
-
-||| Proof that a Bounded value is always <= max.
-export
-boundedLeMax : (b : Bounded max) -> LTE b.value max
-boundedLeMax b = b.inBounds
-
-||| Proof that zero is always a valid Bounded value.
-export
-zeroIsBounded : {max : Nat} -> Bounded (S max)
-zeroIsBounded = MkBounded 0
-
-||| Example: A non-empty list with a compile-time guarantee.
-public export
-data NonEmpty : List a -> Type where
-  IsNonEmpty : NonEmpty (x :: xs)
-
-||| Proof that cons always produces a non-empty list.
-export
-consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs)
-consIsNonEmpty _ _ = IsNonEmpty
diff --git a/verification/verification/proofs/lean4/ApiTypes.lean b/verification/verification/proofs/lean4/ApiTypes.lean
deleted file mode 100644
index 144a943..0000000
--- a/verification/verification/proofs/lean4/ApiTypes.lean
+++ /dev/null
@@ -1,44 +0,0 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
---
--- Typing Proof: Public API type safety
--- Template — replace with your project's API types.
--- Proves properties about exported function signatures.
-
--- Example: Result type used across API boundaries
-inductive ApiResult (α : Type) where
-  | ok    : α → ApiResult α
-  | error : Nat → String → ApiResult α
-
-namespace ApiResult
-  -- Proof: map preserves structure (functor law: map id = id)
-  def map (f : α → β) : ApiResult α → ApiResult β
-    | .ok v      => .ok (f v)
-    | .error c m => .error c m
-
-  theorem map_id : ∀ (r : ApiResult α), map id r = r := by
-    intro r
-    cases r with
-    | ok v => simp [map]
-    | error c m => simp [map]
-
-  -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f)
-  theorem map_comp (f : α → β) (g : β → γ) :
-      ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by
-    intro r
-    cases r with
-    | ok v => simp [map, Function.comp]
-    | error c m => simp [map]
-
--- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000)
--- Replace with your project's numeric invariants
-structure BoundedNat (max : Nat) where
-  val : Nat
-  le_max : val ≤ max
-
-theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max :=
-  b.le_max
-
--- Proof: zero is always bounded
-def zeroBounded (h : 0 < max) : BoundedNat max :=
-  ⟨0, Nat.zero_le max⟩
diff --git a/verification/verification/proofs/tlaplus/StateMachine.tla b/verification/verification/proofs/tlaplus/StateMachine.tla
deleted file mode 100644
index 27f2d69..0000000
--- a/verification/verification/proofs/tlaplus/StateMachine.tla
+++ /dev/null
@@ -1,91 +0,0 @@
---------------------------- MODULE StateMachine ----------------------------
-(* SPDX-License-Identifier: PMPL-1.0-or-later                              *)
-(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)                  *)
-(*                                                                          *)
-(* TLA+ Specification Template: State Machine                               *)
-(* Replace with your project's distributed protocol or state machine.       *)
-(* Use TLC model checker to verify properties.                              *)
-(*                                                                          *)
-(* Example: A simple request pipeline with safety properties.               *)
-(* Replace States, Init, Next with your project's actual states.            *)
-(***************************************************************************)
-
-EXTENDS Naturals, Sequences, FiniteSets
-
-CONSTANTS
-    MaxRequests  \* Upper bound on concurrent requests (for model checking)
-
-VARIABLES
-    state,       \* Current pipeline state
-    processed,   \* Number of processed requests
-    queue        \* Request queue
-
-vars == <<state, processed, queue>>
-
-\* Pipeline states — replace with your project's states
-States == {"idle", "scanning", "routing", "dispatching", "done", "failed"}
-
-\* Valid transitions — replace with your project's transition rules
-ValidTransition(from, to) ==
-    \/ from = "idle"        /\ to = "scanning"
-    \/ from = "scanning"    /\ to = "routing"
-    \/ from = "scanning"    /\ to = "failed"
-    \/ from = "routing"     /\ to = "dispatching"
-    \/ from = "routing"     /\ to = "failed"
-    \/ from = "dispatching" /\ to = "done"
-    \/ from = "dispatching" /\ to = "failed"
-    \/ from = "done"        /\ to = "idle"
-    \/ from = "failed"      /\ to = "idle"
-
-\* Initial state
-Init ==
-    /\ state = "idle"
-    /\ processed = 0
-    /\ queue = <<>>
-
-\* Transition action
-Transition(newState) ==
-    /\ ValidTransition(state, newState)
-    /\ state' = newState
-    /\ IF newState = "done"
-       THEN processed' = processed + 1
-       ELSE processed' = processed
-    /\ UNCHANGED queue
-
-\* Enqueue a request (only when idle or scanning)
-Enqueue ==
-    /\ state \in {"idle", "scanning"}
-    /\ Len(queue) < MaxRequests
-    /\ queue' = Append(queue, "request")
-    /\ UNCHANGED <<state, processed>>
-
-\* Next-state relation
-Next ==
-    \/ \E s \in States : Transition(s)
-    \/ Enqueue
-
-\* Fairness: the system must eventually process
-Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
-
-\* ---- SAFETY PROPERTIES ----
-
-\* State is always valid
-TypeInvariant == state \in States
-
-\* Processed count never decreases (monotonicity)
-ProcessedMonotonic == processed >= 0
-
-\* Queue never exceeds max
-QueueBounded == Len(queue) <= MaxRequests
-
-\* No impossible transitions (e.g., idle -> done)
-NoSkipStates ==
-    [][state' # state =>
-        ValidTransition(state, state')]_state
-
-\* ---- LIVENESS PROPERTIES ----
-
-\* Every request eventually completes or fails
-EventualCompletion == <>(state = "done" \/ state = "failed")
-
-============================================================================
diff --git a/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml b/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index 818fba4..0000000
--- a/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,12 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "verification-unit-safety_case"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  High-assurance verification unit for safety case. 
-  Critical for safety-of-life and aerospace-grade deployment standards.
diff --git a/verification/verification/safety_case/README.adoc b/verification/verification/safety_case/README.adoc
deleted file mode 100644
index ffb53bd..0000000
--- a/verification/verification/safety_case/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Safety case Unit
diff --git a/verification/verification/simulations/0.2-AI-MANIFEST.a2ml b/verification/verification/simulations/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index f40fc1c..0000000
--- a/verification/verification/simulations/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,11 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "simulations-unit"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  Simulations unit for high-rigor verification.
diff --git a/verification/verification/simulations/README.adoc b/verification/verification/simulations/README.adoc
deleted file mode 100644
index 42e184c..0000000
--- a/verification/verification/simulations/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Simulations Unit
diff --git a/verification/verification/tests/0.2-AI-MANIFEST.a2ml b/verification/verification/tests/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index 0008fcf..0000000
--- a/verification/verification/tests/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1 +0,0 @@
-# AI Manifest - Level 1: tests
diff --git a/verification/verification/tests/README.adoc b/verification/verification/tests/README.adoc
deleted file mode 100644
index 3930981..0000000
--- a/verification/verification/tests/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Tests Unit
diff --git a/verification/verification/traceability/0.2-AI-MANIFEST.a2ml b/verification/verification/traceability/0.2-AI-MANIFEST.a2ml
deleted file mode 100644
index defa125..0000000
--- a/verification/verification/traceability/0.2-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,12 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
----
-### [META]
-id: "verification-unit-traceability"
-level: 2
-parent: "../0.1-AI-MANIFEST.a2ml"
-
----
-### [AI_MANIFEST]
-description: |
-  High-assurance verification unit for traceability. 
-  Critical for safety-of-life and aerospace-grade deployment standards.
diff --git a/verification/verification/traceability/README.adoc b/verification/verification/traceability/README.adoc
deleted file mode 100644
index e6e54bc..0000000
--- a/verification/verification/traceability/README.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Traceability Unit
diff --git a/www/.well-known/.well-known/ai.txt b/www/.well-known/.well-known/ai.txt
deleted file mode 100644
index 6668d66..0000000
--- a/www/.well-known/.well-known/ai.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# ai.txt - AI interaction policy
-# See: https://site.spawning.ai/spawning-ai-txt
-
-User-Agent: *
-Disallow-Training: yes
-Disallow-Summarization: no
-Disallow-Generation: yes
-
-# This project's code is licensed under PMPL-1.0-or-later.
-# AI agents may read and analyze this code for assisting contributors.
-# AI agents must NOT use this code for model training without explicit consent.
-# AI agents must preserve Emotional Lineage per PMPL Section 3.
-#
-# For AI agent integration instructions, see:
-#   0-AI-MANIFEST.a2ml (universal AI entry point)
-#   AI.a2ml (Claude-specific instructions)
-#   .machine_readable/ (structured project state)
diff --git a/www/.well-known/.well-known/humans.txt b/www/.well-known/.well-known/humans.txt
deleted file mode 100644
index 60be6cf..0000000
--- a/www/.well-known/.well-known/humans.txt
+++ /dev/null
@@ -1,14 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# humanstxt.org
-
-/* TEAM */
-Maintainer: {{AUTHOR}} ({{OWNER}})
-Contact: {{AUTHOR_EMAIL}}
-From: United Kingdom
-
-/* SITE */
-Last update: {{CURRENT_DATE}}
-Standards: RSR (Rhodium Standard Repository)
-License: PMPL-1.0-or-later (Palimpsest MPL)
-Components: Idris2 ABI, Zig FFI
-Tools: just, Podman, Guix
diff --git a/www/.well-known/.well-known/security.txt b/www/.well-known/.well-known/security.txt
deleted file mode 100644
index 93ce46e..0000000
--- a/www/.well-known/.well-known/security.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# RFC 9116 - security.txt
-# https://securitytxt.org/
-
-Contact: mailto:{{SECURITY_EMAIL}}
-Expires: {{CURRENT_YEAR}}-12-31T23:59:59.000Z
-Encryption: {{PGP_KEY_URL}}
-Preferred-Languages: en
-Canonical: https://{{FORGE}}/{{OWNER}}/{{REPO}}/.well-known/security.txt
-Policy: https://{{FORGE}}/{{OWNER}}/{{REPO}}/blob/main/SECURITY.md
-Hiring: https://{{WEBSITE}}/careers