diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 0d197895..e3025dd5 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -36,7 +36,9 @@ for the canonical statement.
 | **Deno** | Runtime & package management | Replaces Node/npm/bun |
 | **Rust/SPARK** | Performance-critical, systems, WASM, CLI tools, safety-critical | "Rust" always means "Rust/SPARK" per terminology note above. Preferred over Ada where reachable. |
 | **Zig** | FFI layer (hyperpolymath ABI/FFI standard), memory-safe systems where Rust/SPARK is overkill | Also the migration target for V-lang |
-| **Idris2** | Formal verification (sole option) | ATS2 rejected. Proven-library status in `proven` repo. |
+| **Idris2** | Formal verification (primary, ABI-style proofs) | ATS2 rejected. Proven-library status in `proven` repo. |
+| **Agda** | Formal verification (foundational / type-theoretic constructions) | Used by `hyperpolymath/echo-types` (loss-with-residue / proof-relevant fibers) and other foundational formalisations. Constructive only — no postulates in load-bearing tracks. |
+| **echo-types library** | Loss-with-residue formalism (Agda) | `hyperpolymath/echo-types` — canonical formalisation of `Echo f y := Σ (x : A) , (f x ≡ y)`. Cite from this lib rather than reinventing in downstream code. |
 | **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI |
 | **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like |
 | **Gleam** | Backend services | Runs on BEAM or compiles to JS |
diff --git a/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc b/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc
index 705d6dc1..d1be7bd6 100644
--- a/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc
+++ b/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc
@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations
 
diff --git a/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc b/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc
index 705d6dc1..d1be7bd6 100644
--- a/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc
+++ b/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc
@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations
 
diff --git a/ai-instruction/sonnet.md b/ai-instruction/sonnet.md
index 87077343..5df38d9a 100644
--- a/ai-instruction/sonnet.md
+++ b/ai-instruction/sonnet.md
@@ -83,8 +83,8 @@ You are implementing <one-line task statement> in <repo path>.
 
 - <License headers: SPDX-License-Identifier: PMPL-1.0-or-later unless otherwise
   stated (AGPL-3.0-or-later for IDApTIK / Airborne Submarine Squadron)>
-- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Gleam; no
-  TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm)>
+- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Agda / Gleam; no
+  TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm; Agda for foundational proofs incl. echo-types)>
 - <Testing: run tests before claiming completion; "dune build passes" is NOT
   the same as "behaviourally correct" — cite a behavioural check>
 - <No dangerous patterns: believe_me, assert_total, Admitted, sorry,
diff --git a/consent-aware-http/RSR_OUTLINE.adoc b/consent-aware-http/RSR_OUTLINE.adoc
index 705d6dc1..d1be7bd6 100644
--- a/consent-aware-http/RSR_OUTLINE.adoc
+++ b/consent-aware-http/RSR_OUTLINE.adoc
@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations