diff --git a/.gitignore b/.gitignore
index 5265098..5bca6ca 100644
--- a/.gitignore
+++ b/.gitignore
@@ -99,3 +99,6 @@ proofs/**/*.glob
 
 # Lean build artefacts
 proofs/**/*.olean
+
+# Agda interfaces are generated checker artefacts, not proof receipts
+*.agdai
diff --git a/docs/ECHIDNA-INTEGRATION.adoc b/docs/ECHIDNA-INTEGRATION.adoc
index deca593..3359c71 100644
--- a/docs/ECHIDNA-INTEGRATION.adoc
+++ b/docs/ECHIDNA-INTEGRATION.adoc
@@ -120,10 +120,18 @@ module).
 `ProofResult.trust_source` / `JobResult.trust_source` record where the trust
 data came from:
 
-* `echidna`: ECHIDNA reported `trust.axioms` itself. echidnabot passes them
-  on unchanged (a _receipt_).
-* `local-fallback`: echidnabot derived the axioms from the source and
-  output (a _warrant_).
+* `echidna`: ECHIDNA reported `trust.axioms` itself. The REST consumer
+  validates the typed receipt, but then maps axiom names, merges a local
+  source scan and recalculates confidence. The resulting `ProofResult` is
+  an enriched assessment, not an unchanged receipt; this label alone does
+  not distinguish all locally derived data.
+* `local-fallback`: echidnabot derived the axioms from source and/or
+  output. This is a local assessment, not a mechanically sound warrant.
+
+The current direct client bypasses VeriSimDB/VCL. See
+link:ESTATE-ROUTING-AUDIT.adoc[the estate routing audit] for the invariant
+assessment, an unwired backend-specific Rust adapter seam, and the remaining
+production migration. No central routing is claimed by this integration.
 
 This is a plain enum that copies the distinction drawn by
 `hyperpolymath/epistemic-types`. It is not a dependency, because that
diff --git a/docs/ESTATE-HANDOFFS.adoc b/docs/ESTATE-HANDOFFS.adoc
new file mode 100644
index 0000000..883b8b1
--- /dev/null
+++ b/docs/ESTATE-HANDOFFS.adoc
@@ -0,0 +1,84 @@
+// SPDX-License-Identifier: MPL-2.0
+= Scoped estate handoff prompts
+
+These prompts concern gaps actually identified during the echidnabot audit.
+No changes outside `hyperpolymath/echidnabot` were made. The names
+`hyperpolymath/stuff-of-awesome`, `metadatastician` and
+`catachresis-colloquium` were supplied as possible estate contexts; their
+contents/ownership were not inspected here. Do not attribute defects to
+those repositories or owners without a separate audit.
+
+== Session/toolchain provisioner
+
+Provision latest stable Rust 1.99.1, Agda 2.8.0.2 (Cubical-compatible mode),
+Idris2 0.8.0, Lean 4.35.0 and Rocq 9.3.0, plus Creusot 0.14.0 with its
+required nightly-2026-08-03/rustc-dev/llvm-tools, OCaml/opam, Why3/Why3find
+and solver versions required by that Creusot release. Verify official
+checksums and record installed versions; do not substitute similarly named
+npm packages. Cubicle 1.2.0 is a separate optional model checker, not Agda's
+Cubical mode. Install it only for an identified model-checking obligation.
+
+Current sandbox blocks static.rust-lang.org, Debian package hosts and
+release-assets.githubusercontent.com. Provide a trusted prebuilt toolchain
+image or enable official download hosts and dependency access through the
+session's supported setup. Do not weaken proof flags or treat missing tools
+as a successful check. Preserve echidnabot's current Rust pin until the
+stable bump passes build/tests/clippy. Run scripts/check-agda-proofs.sh,
+then kernel-check the independent candidates under proofs/theory, record
+statement correspondence, and discharge first-party Rust obligations in
+Creusot on actual code. Report every remaining open obligation.
+
+== hyperpolymath/verisimdb — ECHIDNA-specific route contract
+
+Inspect the actual VCL executor, Rust client, authorisation and federation
+surfaces before designing anything. Agree with echidna/echidnabot owners a
+versioned ECHIDNA proof-submission/result contract reachable through
+VeriSimDB via VCL. Existing execute_vcl query success is not proof success.
+Define source parameterisation or content references, allowed targets,
+correlation, receipt extraction, capability/version discovery, timeout,
+cancellation, idempotency and retry semantics. Return exactly the typed
+ECHIDNA receipt at the consumer boundary; do not invent universal backend
+interoperability. Provide positive and planted-negative integration evidence.
+Until the contract exists, echidnabot's VeriSimEchidnaGateway is an unwired
+obligation, not a functional central route.
+
+== hyperpolymath/echidna — receipt and gateway producer alignment
+
+Audit the actual GraphQL/REST producer paths and echidna.prove.result/1
+contract before proposing changes. Coordinate the ECHIDNA-specific VCL
+route with VeriSimDB. Preserve the original receipt fields and explicitly
+state which receipt identity, authenticity and request-binding guarantees
+are available; a theorem-name goal must not be assumed to equal source
+text or its content ID. Keep receipt reporting separate from local
+confidence/warrant inference. Record checked proof evidence for the pinned
+trust-kernel implementation rather than equating annotations with discharge.
+Do not silently change the shared schema or claim universal interoperability.
+
+== hyperpolymath/mathesis — catalogue only checked evidence
+
+Use the estate-mathematical-architecture grading and current standards proof
+policy together. Index source-owned receipts from echidnabot only after
+execution evidence exists. The new Agda ReceiptBoundary and FixtureIdentity
+sources are currently AGDA-PENDING; there is no Grade 3 receipt yet. Rust
+ConfidenceLevel::Level3 must not be ingested as mathematics Grade 3.
+Track independent target checks, proposition correspondence, assumptions,
+source hashes and exact toolchains separately. Do not flatten these into a
+percentage or relocate source proof ownership into Mathesis.
+
+== hyperpolymath/standards — reconciliation review, not a defect claim
+
+Review the interaction of Mathesis Grade 3 (locally checked Agda) with the
+proof policy's Rust/Creusot, Idris2 interface and Agda plus Rocq/Lean mappings.
+Document explicitly that the Grade 3 milestone does not discharge independent
+recheck obligations or prove Rust refinement. Clarify architecture examples
+that mention --erasure or full --cubical against the canonical strict
+--safe --without-K --cubical-compatible profile and reviewed exceptions.
+Retain separate policy intent, installed gates and observed receipts.
+
+== epistemic-types — no upstream defect established
+
+No upstream change is requested on the strength of this audit. Its explicit
+separation of map-only structure, factivity and warrant soundness informed
+the local repair. The echidnabot theory candidates do not import that Agda
+library and must not be advertised as a checked integration or faithful
+transport of its witnesses.
diff --git a/docs/ESTATE-ROUTING-AUDIT.adoc b/docs/ESTATE-ROUTING-AUDIT.adoc
new file mode 100644
index 0000000..89603d6
--- /dev/null
+++ b/docs/ESTATE-ROUTING-AUDIT.adoc
@@ -0,0 +1,192 @@
+// SPDX-License-Identifier: MPL-2.0
+= Estate routing audit — 2026-11-01
+
+== Verdict and authority
+
+Against the supplied invariant, estate communication must pass through
+VeriSimDB via VCL. echidnabot currently violates that invariant for delegated
+ECHIDNA communication. The direct client is intentional current behaviour,
+not dead code: defaults, API modes, startup checks, tests and integration docs
+all support it. No local routing policy, central adapter, or authorised direct
+exception was found. Calling it _transitional_ is a proposed migration decision,
+not a description of an existing migration mechanism. This audit treats the
+invariant supplied with the task as normative; it does not claim to have found
+an estate-wide policy declaration in this checkout.
+
+== Rust evidence (baseline ab26bd54)
+
+* `src/dispatcher/echidna_client.rs::new` constructs a reqwest client from
+  `EchidnaConfig.endpoint` and `rest_endpoint`. `verify_proof` selects direct
+  GraphQL or REST; Auto falls back from GraphQL to REST on error. Neither
+  route calls VeriSimDB. Relabelling the endpoint as a database URL does not
+  translate either protocol into VCL.
+* `handshake` calls `/api/provers`, then `/api/health` if needed.
+  `verify_proof_rest` posts to `/api/verify`; the GraphQL implementation posts
+  a verification mutation. Tactics, health and prover availability also use
+  direct HTTP. Routing only proof submission would leave bypasses.
+* `src/main.rs::serve` constructs `Arc<EchidnaClient>` and calls
+  `startup_handshake`. The CLI verification path also constructs the client.
+  `process_job` calls health and prover status before its local-isolation
+  branch; even local-isolation is therefore not network-free.
+* `src/config.rs::EchidnaApiMode` and the TOML examples expose direct modes,
+  not a central-routing switch. `Cargo.toml` has no VeriSimDB client.
+  `tests/live_echidna.rs` exercises direct interoperability; those tests are
+  not evidence of estate routing compliance.
+* BoJ-only MCP routing (`src/llm.rs`) is a separate boundary, not proof that
+  dispatcher HTTP travels through VeriSimDB. SQLite persistence and content
+  IDs likewise do not establish a routed communication path.
+
+== Receipt versus derived assessment
+
+`src/dispatcher/prove_result.rs::ProveResult::from_value` is the existing
+consumer boundary for `echidna.prove.result/1`: exact schema/status,
+required fields, unknown top-level field rejection, bounded integer duration,
+and finite optional confidence. Key order is unrestricted; unknown nested
+trust fields are ignored. It is not a signature verifier, identity check,
+request/goal correlator, or theorem soundness proof.
+
+The actual `rest_verify_result` behaviour is more limited than earlier
+integration prose claimed. It parses the typed receipt, maps reported axiom
+names to flags, merges a local source scan, ignores reported confidence and
+recalculates confidence locally. It then returns `ProofResult` labelled
+`TrustSource::Echidna`. That label means reported axioms contributed, NOT
+that all returned trust data is an unchanged receipt. The original typed
+object is not retained in that result. Legacy REST and GraphQL follow their
+own conversion paths; typed receipts are not mandatory on all current paths.
+This audit does not silently change those production semantics.
+
+The epistemic-types reference is
+https://github.com/hyperpolymath/epistemic-types/tree/5422cd5bf1418c44321bf0f77e894737a451d8f5[5422cd5].
+Its README describes a constructive map-only base, separately added factivity
+and sound-warrant assumptions. A JSON receipt or provenance enum supplies
+neither `reflect` nor warrant soundness. Local confidence is a derived
+assessment, not a mechanically sound warrant. There is no Rust epistemic-types
+dependency or proof transport integration here.
+
+== Backend-specific design and code added
+
+`src/dispatcher/verisim_echidna.rs` supplies an intentionally unwired Rust
+seam, not a universal interoperability layer:
+
+. `EchidnaProveRequest` carries only ECHIDNA prover/source input. It is not a
+  published wire schema or VCL syntax.
+. `VeriSimEchidnaGateway` is the explicit integration obligation: submit via
+  authorised VeriSimDB/VCL routing and extract one ECHIDNA receipt.
+. `VeriSimEchidnaAdapter::prove` validates that receipt using the existing
+  `ProveResult::from_value`, returns the typed object without enrichment,
+  rejects legacy bodies, and propagates errors without a direct fallback.
+
+No concrete gateway implements that obligation. A trait implementation can
+lie about its route; the type is not proof of network policy. Unit tests use
+stubs only. The seam preserves typed receipt fields (not original JSON bytes
+or ignored extension fields), and does not promote a verified status to fact.
+
+For grounding, VeriSimDB's Rust connector inspected at
+https://github.com/hyperpolymath/verisimdb/blob/dd8270951a4ddbe2f9189b276cc7dac60cd9cd7d/connectors/clients/rust/src/vcl.rs[dd827095]
+exposes `execute_vcl(query)` posting a query envelope to
+`/api/v1/vcl/execute`, returning success, statement type, row count and data.
+That generic query surface does not by itself establish an ECHIDNA invocation,
+a receipt extraction rule, or universal backend interoperability. No invented
+`PROVE` statement, federation capability, or generic JSON passthrough is used
+in this patch.
+
+== Required migration (planned, not implemented)
+
+* Agree a versioned ECHIDNA-specific gateway contract with VeriSimDB/VCL:
+  supported operation, authorised target/provers, source binding, submission
+  and result correlation, receipt extraction, capability/version discovery,
+  timeout/cancellation, idempotency and retry behaviour. Do not interpolate
+  untrusted proof source into VCL text. Define parameterisation or separately
+  stored content references with the backend implementer.
+* Retain the validated receipt separately from derived local assessments and
+  their provenance. Persist both explicitly through JobResult/store/reporting;
+  do not overwrite receipt confidence or imply formal warrant soundness.
+  Bind results to requests using an agreed contract, not an assumed equality
+  between the receipt's theorem-name `goal` and source text/content ID.
+* Wire serve, CLI, workers, health, availability, handshake and tactics to
+  central routing; fail closed when routing/capabilities are unavailable.
+  Do not downgrade to legacy or direct ECHIDNA on route failure. If an explicit
+  development-only direct exception is authorised, make it opt-in and visibly
+  non-estate-compliant, not the production default.
+* Cover retry classification, duplicate submissions, unavailable gateway,
+  malformed/wrong-version receipts, rejected authorisation and correlation
+  mismatches. Add a live central-route test plus network-denial tests proving
+  no ECHIDNA endpoint is contacted by estate mode. Audit other estate clients
+  separately rather than claiming this adapter routes the entire bot.
+
+== Verification and status
+
+Implemented in this patch: audit, corrected documentation, backend-specific
+adapter seam and stub tests for receipt preservation, validation rejection and
+error propagation. Production direct behaviour remains unchanged. Central
+routing, persistence of the original receipt and honest separated assessment
+provenance remain planned. No live VCL/ECHIDNA test was performed.
+
+The sandbox has neither `cargo` nor `rustup` on PATH; compilation, rustfmt and
+Rust tests could not be run. New tests are therefore unverified, not passing
+claims. Run `cargo test dispatcher::verisim_echidna` with the repository's
+pinned toolchain, followed by the full test suite and clippy before rollout.
+
+== Policy alignment and Grade 3 target (follow-up)
+
+The owner requires Grade 3 proofing, with mathematics architecture sourced
+from Mathesis and other verification policy from standards. Sources inspected:
+
+* https://github.com/hyperpolymath/mathesis/blob/50a012dba57fe90c9aca8d57241690c133ab117c/estate-mathematical-architecture[Mathesis estate mathematical architecture],
+  especially sections 3 and 5. Grade 3 means an iteratively formulated
+  Agda proof that actually type-checks locally, without independent-system
+  translation yet. It is not a confidence percentage or a Rust test level.
+* https://github.com/hyperpolymath/standards/blob/46ee18323305d5b36e2eef936e47dd54c39ea736/3-practice/PROOF-POLICY.adoc[Standards proof policy],
+  especially sections 1, 2.1, 2.2 and 5. First-party Rust implementation
+  obligations belong on the code in Creusot; shared interface/wire contracts
+  belong in Idris2; theory belongs in Agda, with Rocq and Lean rechecks and
+  explicit statement correspondence. An Agda model alone does not prove
+  runtime refinement of Rust.
+
+The architecture's illustrative Agda flags are not a substitute for the
+standards policy's canonical invocation:
+`agda --safe --without-K --cubical-compatible <module.agda>`.
+Full Cubical or incompatible profiles require separate explicit review.
+Grade 3 is an intermediate mathematics milestone, not closure of the
+standards policy's independent recheck obligations. Record grades separately
+from proof-ledger status and engineering implementation assurance.
+
+For this patch, Grade 3 is NOT attained. No Agda witness, Creusot discharge,
+or Idris2 interface proof was produced or checked. Stub tests are unrun and
+therefore do not even establish `tested-only`. Obligations remain `open`:
+
+[cols="2,1,3",options="header"]
+|===
+|Obligation |Mapped verifier |Outstanding evidence
+|Receipt validation and no direct fallback in the new adapter
+|Creusot on Rust
+|Code contracts, explicit dependency assumptions, generated obligation discharge
+|ECHIDNA gateway request/receipt and error protocol
+|Idris2
+|Agreed backend protocol and checked interface contract; no invented wire model
+|Receipt transport does not imply factivity or warrant soundness
+|Agda (Grade 3 target)
+|Explicit statement and assumptions, local strict-profile type-check receipt;
+subsequent independent rechecks remain open
+|Estate network routing invariant
+|Implementation and deployment evidence
+|Concrete gateway, all call sites migrated, network-denial integration tests;
+trait obligations alone do not establish this property
+|===
+
+Retain source ownership in echidnabot. Mathesis may index receipts but must
+not become a parallel proof owner. Each future result must name the exact
+source revision, proposition, assumptions, tool/library versions, invocation
+and observed outcome. Agda, Idris2 and Creusot are also absent from PATH in
+this sandbox. Missing tools are open obligations, not waived checks.
+
+=== Subsequent source preparation
+
+Unverified theory candidates and a strict local Agda check command have now
+been added. This does not change the `open` proof statuses above. See
+link:PROOF-STATUS.adoc[the current proof ledger] for the pre-existing fixture
+inventory, ABI scaffold defects, new Agda/Lean/Rocq candidates and observed
+toolchain installation blockers. See
+link:ESTATE-HANDOFFS.adoc[scoped handoff prompts] for external contract and
+environment work. No Grade 3 or production central-routing completion is
+claimed from source preparation.
diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
new file mode 100644
index 0000000..fd85057
--- /dev/null
+++ b/docs/PROOF-STATUS.adoc
@@ -0,0 +1,169 @@
+// SPDX-License-Identifier: MPL-2.0
+= Proof status — estate routing and receipt boundary
+:toc:
+
+== Evidence rules
+
+Updated 2026-11-01 on `arena/68c18146-echidnabot`, based on
+`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. New files are working-tree
+candidates, not committed or checked proof receipts. No Grade 3 attainment
+is claimed. `open` means not checked/done, `argued` means an explicit
+assumption, and `tested-only` requires an actual observed bounded check.
+ConfidenceLevel::Level3 is a runtime heuristic, NOT Mathesis Grade 3.
+
+Policies and pinned references are in
+link:ESTATE-ROUTING-AUDIT.adoc[the routing audit]. Theory requires strict
+Agda checks, with separately recorded Rocq/Lean statement correspondence and
+kernel results. Rust behaviour requires Creusot on actual first-party code;
+a mathematical model does not establish runtime refinement.
+
+== Local obligation ledger
+
+[cols="1,2,1,3",options="header"]
+|===
+|ID |Statement and artefact |Status |Required evidence / limits
+|T-RECEIPT
+|A general evidence token does not imply its claim;
+`proofs/agda/ReceiptBoundary.agda`
+|open
+|AGDA-PENDING. `no-unconditional-reflection` constructs a contradiction
+from unconditional reflection by instantiating Claim with Empty and evidence
+with Unit. `receive-with-soundness` requires an explicit evidence-to-claim
+function. This is new local theory, informed by epistemic-types, NOT a port
+of that library or proof of the Rust parser. No external library or postulate.
+|T-RECEIPT-ROCQ / T-RECEIPT-LEAN
+|Same statements, quantification, evidence packaging and assumptions as
+T-RECEIPT
+|open
+|Independent re-proof source candidates now exist under
+`proofs/theory/{rocq,lean}/ReceiptBoundary.*`, without libraries, axioms or
+admitted obligations. Neither was compiled; no transport or checked
+correspondence exists. A Prop-only reformulation of Set-level quantification
+is not silently interchangeable. The candidates deliberately use Rocq Set
+and Lean Type rather than silently shrinking the claims to Prop.
+|E-ADAPTER
+|`VeriSimEchidnaAdapter::prove` validates the gateway payload and propagates
+failure without calling a direct client
+|open
+|Creusot contracts and all first-party Rust obligations remain undischarged.
+Async/gateway, serde and dependency contracts need an explicit trust boundary.
+Stub tests are present but unrun; absence of a direct endpoint in this struct
+is code-review evidence, not proof of gateway behaviour.
+|E-RECEIPT
+|`ProveResult::from_value` checks the existing typed receipt constraints
+|open
+|Rust/Creusot proof on actual code. Existing tests are not proof receipts.
+Structural validation alone supplies no authentication, correlation or factivity.
+|I-GATEWAY
+|Shared ECHIDNA-specific VeriSimDB/VCL protocol contract
+|open
+|Backend agreement and Idris2 contract required before implementation;
+no executable central route is supplied by the new trait.
+|E-ROUTING
+|All relevant production estate calls use authorised VeriSimDB/VCL routing
+|open
+|Current direct client is a counterexample. Call-site migration and deployment
+network tests remain absent. No model proof can make this row pass today.
+|E-PROVENANCE
+|Original typed receipt stays separate from locally computed assessment
+|open
+|New unwired adapter returns the validated receipt. Existing production REST
+conversion still merges axioms, recomputes confidence and drops original fields.
+Persistence, aggregation and reporting require a deliberate migration.
+|===
+
+== Pre-existing proof material and semantic reconstruction
+
+The old `proofs/ECHO-TYPES-AUDIT.adoc` classified the four Lean/Coq files
+as prover fixtures. That remains true. Its statement that ABI scaffolding
+is out of scope does NOT make that scaffolding verified.
+
+* `proofs/coq/trivial_ok.v`: `forall (A : Prop), A -> A`.
+* `proofs/lean/trivial_ok.lean`: `(A : Prop) -> A -> A`.
+* New `proofs/agda/FixtureIdentity.agda`: `(A : Set) -> A -> A`.
+  This is a semantic reconstruction of the constructive identity schema,
+  because there was no Agda record. It is not witness transport. Rocq/Lean
+  Prop and Agda Set differ; correspondence is limited to propositional
+  identity and remains `open` until checked and justified explicitly.
+  All three current executions are unavailable in this sandbox.
+* `proofs/coq/admitted_stub.v` and `proofs/lean/sorry_stub.lean` are negative
+  fixtures, not candidate proofs. Their escape hatches must stay intact.
+  They are excluded from Grade 3 counts, not repaired into passing fixtures.
+* JSON files under `proofs/test_fixtures` are webhook/prover inputs, not proofs.
+
+=== ABI scaffold debt (not verified)
+
+`src/abi/{Types,Layout,Foreign}.idr` contains literal `{{PROJECT}}` module
+names, unresolved holes and placeholder foreign symbols. These are templates,
+not an instantiated echidnabot ABI. `HasSize`/`HasAlignment` have unrestricted
+constructors and therefore do not establish actual compiler layout.
+`exampleStructSize` claims 16 while its own comment describes 24 bytes.
+`offsetInBounds` quantifies over arbitrary Field values without membership or
+bounds premises, so it cannot be proved as written. Layout checking and
+foreign pointer/lifetime obligations also remain unresolved.
+
+Status: `open`. Do not replace holes with postulates or transcribe these
+claims to Agda as if they were true. A semantic rewrite needs the actual
+exported ABI, supported targets, field representations, ownership and bounds
+premises; the Rust interface proof policy remains active. No new ABI symbols
+or layout contracts are invented in this patch.
+
+== Assumed boundaries (argued, not proven)
+
+* `serde_json` at the Cargo.lock version: parsing/value representation and
+  numeric/deserialisation behaviour used by ProveResult. No external proof
+  was checked here. A Rust proof must name any trusted extern specification.
+* Gateway trait implementers: compliance with authorised routing, extraction,
+  authentication and request correlation is an obligation, not type-enforced.
+* `echidna-core` at `645d7a2489c644706210e171acba6f52741ad3b8`:
+  imported trust kernel behaviour. Upstream annotations alone are not a
+  checked Creusot receipt for this crate and its callers.
+* Any future claim of theorem truth needs the relevant prover kernel/checker
+  boundary and assumptions, separately from receipt transport.
+
+== Toolchain acquisition attempt
+
+Published stable releases observed through GitHub's release API on 2026-11-01:
+Rust 1.99.1; Agda 2.8.0.2; Creusot 0.14.0; Idris2 0.8.0;
+Lean 4.35.0; Rocq 9.3.0; Cubicle 1.2.0. None was installed or run.
+Creusot 0.14.0 itself pins `nightly-2026-08-03` with rustc-dev and llvm-tools;
+it cannot simply be built against latest stable Rust. Its INSTALL requires
+Cargo, opam/OCaml, Why3/Why3find and solver acquisition.
+
+Actual network observations:
+
+* `static.rust-lang.org` and `deb.debian.org`: TLS connection failed;
+  Debian HTTP also returned an empty reply.
+* The Agda Linux release asset was requested through api.github.com;
+  its redirect to `release-assets.githubusercontent.com` failed TLS.
+* The sandbox permits GitHub source/API and npm/PyPI registries, not the
+  distribution/package hosts needed by the normal installers. Unrelated npm
+  packages named agda/rustup are not substituted for trusted toolchains.
+
+Required environment help: provision verified toolchains through the session
+setup, or allow the official distribution and package hosts (including release
+assets and the dependencies required by opam). Cubical Agda is a mode of Agda,
+not the separate Cubicle model checker. Full Cubical is not the canonical
+proof profile and needs a separately reviewed exception where necessary.
+The existing Rust pin is preserved until an actual tested toolchain update;
+this is an unmet latest-stable target, not a completed upgrade.
+
+== Reproduction and completion criteria
+
+`./scripts/check-agda-proofs.sh` requires exactly Agda 2.8.0.2, ignores stale
+interfaces, uses no external libraries, and runs the strict policy flags.
+It prints source hashes, base revision and invocations. Capture the output
+and record the observed result here; do not edit statuses based on expected
+success. Its missing-tool failure was observed in this session (exit 127).
+This is evidence that absence is not silently skipped, not a proof execution.
+
+`cargo test --locked dispatcher::verisim_echidna` and the existing protocol
+suites remain unrun. Creusot, Idris2 and independent theory rechecks also
+remain unrun. CI wiring for the new theory gate and its real positive/negative
+controls is still open; a local check command is not an installed CI gate.
+
+Completion requires: actual checker receipts; backend protocol agreement;
+production routing and provenance migration; implementation/interface proofs;
+matched theory rechecks; preserved fixture detection; and regression tests.
+This session has NOT completed old/new proof updating or the original routing
+work. Documentation and unverified source candidates are partial progress only.
diff --git a/proofs/ECHO-TYPES-AUDIT.adoc b/proofs/ECHO-TYPES-AUDIT.adoc
index 0f2277a..741dc64 100644
--- a/proofs/ECHO-TYPES-AUDIT.adoc
+++ b/proofs/ECHO-TYPES-AUDIT.adoc
@@ -74,3 +74,12 @@ echo-types audit lives at `+echidna/docs/PROOF-NEEDS.md+` § "`Echo-types
 audit (2026-06-01)`". Two L3-shape obligations are cross-referenced
 there (`+ProofStateSerialisation+` roundtrip = EQUIV;
 `+ProverKindInjectivity+` = INJ); none flow through echidnabot.
+
+=== Follow-up (2026-11-01)
+
+The classification above is historical, not a claim that all current proof
+material is verified. See link:../docs/PROOF-STATUS.adoc[the current ledger]
+for new unverified Agda theory, the identity-fixture semantic reconstruction,
+and explicit ABI scaffold debt. The negative fixtures remain deliberately
+incomplete. The ABI templates are not checked proofs; the earlier scope
+exclusion does not discharge their obligations.
diff --git a/proofs/agda/FixtureIdentity.agda b/proofs/agda/FixtureIdentity.agda
new file mode 100644
index 0000000..c7559c8
--- /dev/null
+++ b/proofs/agda/FixtureIdentity.agda
@@ -0,0 +1,11 @@
+-- SPDX-License-Identifier: MPL-2.0
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+
+-- Semantic reconstruction of the constructive identity shared by the
+-- positive Lean/Coq dogfood fixtures, not a translation receipt.
+-- Agda Set differs from Rocq Prop and Lean Prop; correspondence is restricted
+-- to the propositional identity schema, not arbitrary universe conversion.
+module FixtureIdentity where
+
+identity : (A : Set) → A → A
+identity A evidence = evidence
diff --git a/proofs/agda/ReceiptBoundary.agda b/proofs/agda/ReceiptBoundary.agda
new file mode 100644
index 0000000..22c7395
--- /dev/null
+++ b/proofs/agda/ReceiptBoundary.agda
@@ -0,0 +1,47 @@
+-- SPDX-License-Identifier: MPL-2.0
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+
+-- Theory only: no theorem here establishes behaviour of Rust, JSON parsers,
+-- network routing, a prover, or cryptographic authentication.
+module ReceiptBoundary where
+
+-- Small constructive core, with no standard-library dependency.
+data Empty : Set where
+
+record Unit : Set where
+  constructor unit
+
+-- A receipt carries evidence of some explicitly named type. There is no
+-- implicit operation converting that evidence into the claimed proposition.
+record Warrant (Claim : Set) : Set₁ where
+  constructor warrant
+  field
+    Evidence : Set
+    evidence : Evidence
+
+-- Soundness is extra structure. It cannot be obtained just by receiving a
+-- token, validating its JSON shape, or assigning it a confidence level.
+record SoundWarrant {Claim : Set} (w : Warrant Claim) : Set where
+  constructor sound-warrant
+  field
+    sound : Warrant.Evidence w → Claim
+
+receive-with-soundness : {Claim : Set} → (w : Warrant Claim) →
+                        SoundWarrant w → Claim
+receive-with-soundness w checked =
+  SoundWarrant.sound checked (Warrant.evidence w)
+
+-- A token can exist even when the claim has no inhabitant.
+empty-claim-token : Warrant Empty
+empty-claim-token = warrant Unit unit
+
+-- Concrete constructive counterexample to any *unconditional* factivity
+-- interface for arbitrary receipt/warrant tokens.
+no-unconditional-reflection :
+  ((Claim : Set) → Warrant Claim → Claim) → Empty
+no-unconditional-reflection reflect = reflect Empty empty-claim-token
+
+-- In particular this receipt cannot possess a soundness function.
+no-soundness-for-empty-token : SoundWarrant empty-claim-token → Empty
+no-soundness-for-empty-token checked =
+  receive-with-soundness empty-claim-token checked
diff --git a/proofs/theory/lean/ReceiptBoundary.lean b/proofs/theory/lean/ReceiptBoundary.lean
new file mode 100644
index 0000000..4e2b0d1
--- /dev/null
+++ b/proofs/theory/lean/ReceiptBoundary.lean
@@ -0,0 +1,35 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Independent re-proof candidate, NOT checked evidence. Core only; no Mathlib.
+-- Type 0 scope must be compared with Agda Set and Rocq Set explicitly.
+namespace EchidnabotReceiptBoundary
+
+structure ReceiptWarrant (Claim : Type) : Type 1 where
+  Evidence : Type
+  evidence : Evidence
+
+structure SoundReceiptWarrant {Claim : Type} (w : ReceiptWarrant Claim) where
+  sound : w.Evidence → Claim
+
+/-- Derive a claim from a receipt warrant and an explicit soundness witness. -/
+def receiveWithSoundness {Claim : Type}
+    (w : ReceiptWarrant Claim) (checked : SoundReceiptWarrant w) : Claim :=
+  checked.sound w.evidence
+
+def emptyClaimToken : ReceiptWarrant Empty :=
+  { Evidence := Unit, evidence := () }
+
+/-- An unconditional reflection function for every claim yields a contradiction. -/
+def noUnconditionalReflection
+    (reflect : (Claim : Type) → ReceiptWarrant Claim → Claim) : Empty :=
+  reflect Empty emptyClaimToken
+
+/-- A soundness witness for the empty-claim token yields a contradiction. -/
+def noSoundnessForEmptyToken
+    (checked : SoundReceiptWarrant emptyClaimToken) : Empty :=
+  receiveWithSoundness emptyClaimToken checked
+
+#print axioms receiveWithSoundness
+#print axioms noUnconditionalReflection
+#print axioms noSoundnessForEmptyToken
+
+end EchidnabotReceiptBoundary
diff --git a/proofs/theory/lean/lean-toolchain b/proofs/theory/lean/lean-toolchain
new file mode 100644
index 0000000..a6aff06
--- /dev/null
+++ b/proofs/theory/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0
diff --git a/proofs/theory/rocq/ReceiptBoundary.v b/proofs/theory/rocq/ReceiptBoundary.v
new file mode 100644
index 0000000..6233aab
--- /dev/null
+++ b/proofs/theory/rocq/ReceiptBoundary.v
@@ -0,0 +1,40 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Independent re-proof candidate, NOT checked evidence. No libraries,
+   axioms or admitted obligations. The explicit small-type scope must be
+   compared with Agda Set before correspondence is claimed. *)
+
+Record ReceiptWarrant (Claim : Set) : Type := {
+  evidence_type : Set;
+  evidence_token : evidence_type
+}.
+
+Arguments evidence_type {Claim} _.
+Arguments evidence_token {Claim} _.
+
+Record SoundReceiptWarrant {Claim : Set} (w : ReceiptWarrant Claim) : Type := {
+  sound : evidence_type w -> Claim
+}.
+
+Arguments sound {Claim w} _ _.
+
+(** Derive a claim from a receipt warrant and an explicit soundness witness. *)
+Definition receive_with_soundness {Claim : Set}
+    (w : ReceiptWarrant Claim) (checked : SoundReceiptWarrant w) : Claim :=
+  sound checked (evidence_token w).
+
+Definition empty_claim_token : ReceiptWarrant Empty_set :=
+  {| evidence_type := unit; evidence_token := tt |}.
+
+(** An unconditional reflection function for every claim yields a contradiction. *)
+Definition no_unconditional_reflection
+    (reflect : forall Claim : Set, ReceiptWarrant Claim -> Claim) : Empty_set :=
+  reflect Empty_set empty_claim_token.
+
+(** A soundness witness for the empty-claim token yields a contradiction. *)
+Definition no_soundness_for_empty_token
+    (checked : SoundReceiptWarrant empty_claim_token) : Empty_set :=
+  receive_with_soundness empty_claim_token checked.
+
+Print Assumptions receive_with_soundness.
+Print Assumptions no_unconditional_reflection.
+Print Assumptions no_soundness_for_empty_token.
diff --git a/scripts/check-agda-proofs.sh b/scripts/check-agda-proofs.sh
new file mode 100755
index 0000000..4ea20c0
--- /dev/null
+++ b/scripts/check-agda-proofs.sh
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Strict local theory check. This does NOT check Rust refinement or routing.
+set -euo pipefail
+cd "$(dirname "${BASH_SOURCE[0]}")/.."
+
+expected='Agda version 2.8.0.2'
+if ! command -v agda >/dev/null; then
+    echo 'OPEN: Agda 2.8.0.2 is required; no proof was checked.' >&2
+    exit 127
+fi
+actual=$(agda --version)
+if [[ "$actual" != "$expected" ]]; then
+    printf 'OPEN: expected %s, observed %s. Review the pin explicitly.\n' "$expected" "$actual" >&2
+    exit 1
+fi
+printf 'Tool: %s\nBase commit (not a clean-tree claim): %s\n' "$actual" "$(git rev-parse HEAD)"
+printf 'Working-tree source hashes:\n'
+sha256sum proofs/agda/ReceiptBoundary.agda proofs/agda/FixtureIdentity.agda
+for source in proofs/agda/ReceiptBoundary.agda proofs/agda/FixtureIdentity.agda; do
+    # Ignore old interfaces so a previous, weaker-profile check is not reused.
+    command=(agda --safe --without-K --cubical-compatible --exact-split
+        --no-sized-types --no-guardedness --no-libraries --no-default-libraries
+        --ignore-interfaces -i proofs/agda "$source")
+    printf 'Invocation:'
+    printf ' %q' "${command[@]}"
+    printf '\n'
+    "${command[@]}"
+done
+printf '%s\n' 'AGDA-VERIFIED for these source hashes only; independent rechecks and Rust refinement remain OPEN.'
diff --git a/src/dispatcher/mod.rs b/src/dispatcher/mod.rs
index 4b48a47..7ddbff5 100644
--- a/src/dispatcher/mod.rs
+++ b/src/dispatcher/mod.rs
@@ -5,6 +5,7 @@
 
 pub mod echidna_client;
 pub mod prove_result;
+pub mod verisim_echidna;
 
 pub use echidna_client::{EchidnaClient, EchidnaHandshake, MIN_ECHIDNA_VERSION};
 pub use prove_result::{ProveResult, PROVE_RESULT_SCHEMA};
@@ -42,12 +43,13 @@ pub struct ProofResult {
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)]
 #[serde(rename_all = "kebab-case")]
 pub enum TrustSource {
-    /// ECHIDNA reported the axiom data itself (an `echidna.prove.result/1`
-    /// `trust` object). echidnabot transports it unchanged (a receipt); the
-    /// level is still computed by ECHIDNA's trust kernel, linked in.
+    /// ECHIDNA reported axioms in an `echidna.prove.result/1` receipt.
+    /// The direct REST path also merges a local source scan and recomputes
+    /// confidence using the linked trust kernel. This label does not mean
+    /// the enriched trust data is an unchanged receipt or a sound warrant.
     Echidna,
-    /// echidnabot computed the trust data from what ECHIDNA returned, using
-    /// ECHIDNA's trust kernel and source scanner: a warrant, not a receipt.
+    /// echidnabot derived trust data locally using the linked ECHIDNA trust
+    /// kernel and source scanner. No formal warrant soundness is established.
     #[default]
     LocalFallback,
 }
diff --git a/src/dispatcher/prove_result.rs b/src/dispatcher/prove_result.rs
index 2d25794..9fa3ffe 100644
--- a/src/dispatcher/prove_result.rs
+++ b/src/dispatcher/prove_result.rs
@@ -16,8 +16,10 @@
 //! as this shape, and anything else falls back to the legacy REST shape.
 //!
 //! The `trust` object is ECHIDNA's own judgement (a *receipt*, in the
-//! vocabulary of `hyperpolymath/epistemic-types`). echidnabot transports it
-//! instead of re-deriving a score; see [`super::TrustSource`].
+//! vocabulary of `hyperpolymath/epistemic-types`). This type preserves its
+//! recognised fields. The current direct REST consumer subsequently merges
+//! local axioms and re-derives confidence; its enriched `ProofResult` is not
+//! an unchanged receipt. Structural validation does not establish soundness.
 //!
 //! Validation here is deliberately strict about the parts a consumer depends
 //! on (schema tag, status vocabulary, the I-JSON integer bound on
diff --git a/src/dispatcher/verisim_echidna.rs b/src/dispatcher/verisim_echidna.rs
new file mode 100644
index 0000000..5699e35
--- /dev/null
+++ b/src/dispatcher/verisim_echidna.rs
@@ -0,0 +1,137 @@
+// SPDX-License-Identifier: MPL-2.0
+//! Proposed ECHIDNA-specific VeriSimDB/VCL boundary, NOT a live transport.
+//!
+//! No implementation of the gateway or production wiring exists here. See
+//! `docs/ESTATE-ROUTING-AUDIT.adoc`. This is not a generic database/prover API.
+
+use async_trait::async_trait;
+use serde_json::Value;
+
+use super::{ProveResult, ProverKind};
+use crate::error::Result;
+
+/// Input to the proposed ECHIDNA route; deliberately not a VCL wire format.
+#[derive(Debug)]
+pub struct EchidnaProveRequest<'a> {
+    pub prover: &'a ProverKind,
+    pub content: &'a str,
+}
+
+/// Backend-specific integration point awaiting a real gateway contract.
+///
+/// Implementations must submit through VeriSimDB's authorised VCL route and
+/// extract exactly one ECHIDNA receipt, not a query-success flag or row count.
+/// They must propagate routing failures without falling back to direct HTTP.
+/// This trait documents obligations; it does not prove routing or soundness.
+#[async_trait]
+pub trait VeriSimEchidnaGateway: Send + Sync {
+    /// Submit a proof request and return the extracted ECHIDNA receipt as JSON.
+    ///
+    /// # Errors
+    /// Implementations must propagate routing failures to the caller.
+    async fn prove_receipt(&self, request: EchidnaProveRequest<'_>) -> Result<Value>;
+}
+
+/// Validates only the ECHIDNA receipt, without local trust enrichment.
+///
+/// This adapter has no ECHIDNA endpoint, direct client, or legacy fallback.
+/// Receipt validation is structural, not evidence that the claim is true or
+/// that the supplied gateway actually used VCL.
+pub struct VeriSimEchidnaAdapter<G> {
+    gateway: G,
+}
+
+impl<G: VeriSimEchidnaGateway> VeriSimEchidnaAdapter<G> {
+    /// Create an adapter using the supplied gateway.
+    pub fn new(gateway: G) -> Self {
+        Self { gateway }
+    }
+
+    /// Submit a request and return a structurally validated ECHIDNA receipt.
+    ///
+    /// Recognised fields are returned without local trust enrichment; unknown
+    /// fields within `trust` are ignored.
+    ///
+    /// # Errors
+    /// Propagates gateway errors and validation errors from
+    /// [`ProveResult::from_value`].
+    pub async fn prove(&self, request: EchidnaProveRequest<'_>) -> Result<ProveResult> {
+        ProveResult::from_value(self.gateway.prove_receipt(request).await?)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::error::Error;
+
+    struct Stub(Value);
+
+    #[async_trait]
+    impl VeriSimEchidnaGateway for Stub {
+        async fn prove_receipt(&self, request: EchidnaProveRequest<'_>) -> Result<Value> {
+            assert_eq!(request.prover.as_str(), "lean");
+            assert_eq!(request.content, "goal");
+            Ok(self.0.clone())
+        }
+    }
+
+    fn receipt() -> Value {
+        serde_json::json!({
+            "schema": "echidna.prove.result/1", "status": "verified",
+            "prover": "Lean", "goal": "goal", "duration_ms": 12,
+            "message": "ok", "echidna_version": "2.3.0",
+            "trust": {"axioms": ["sorryAx", "backend-specific"], "confidence": 0.2}
+        })
+    }
+
+    async fn run(value: Value) -> Result<ProveResult> {
+        VeriSimEchidnaAdapter::new(Stub(value))
+            .prove(EchidnaProveRequest {
+                prover: &ProverKind::new("lean"),
+                content: "goal",
+            })
+            .await
+    }
+
+    #[tokio::test]
+    async fn preserves_typed_receipt_without_enrichment() {
+        let value = receipt();
+        let result = run(value.clone()).await.unwrap();
+        assert_eq!(serde_json::to_value(result).unwrap(), value);
+    }
+
+    #[tokio::test]
+    async fn rejects_legacy_envelopes_versions_and_invalid_receipts() {
+        assert!(run(serde_json::json!({"valid": true})).await.is_err());
+        for (key, value) in [
+            ("schema", serde_json::json!("echidna.prove.result/2")),
+            ("status", serde_json::json!("success")),
+            ("duration_ms", serde_json::json!(1_u64 << 53)),
+        ] {
+            let mut body = receipt();
+            body[key] = value;
+            assert!(run(body).await.is_err());
+        }
+    }
+
+    struct Unavailable;
+
+    #[async_trait]
+    impl VeriSimEchidnaGateway for Unavailable {
+        async fn prove_receipt(&self, _: EchidnaProveRequest<'_>) -> Result<Value> {
+            Err(Error::Unsupported("ECHIDNA VCL route unavailable".into()))
+        }
+    }
+
+    #[tokio::test]
+    async fn propagates_gateway_failure_without_direct_fallback() {
+        let result = VeriSimEchidnaAdapter::new(Unavailable)
+            .prove(EchidnaProveRequest {
+                prover: &ProverKind::new("lean"),
+                content: "goal",
+            })
+            .await;
+        assert!(matches!(result, Err(Error::Unsupported(_))));
+    }
+}
diff --git a/src/trust/confidence.rs b/src/trust/confidence.rs
index f5c3d09..c1506ce 100644
--- a/src/trust/confidence.rs
+++ b/src/trust/confidence.rs
@@ -10,10 +10,11 @@
 //! ECHIDNA's [`TrustFactors`] and wraps the answer in a report.
 //!
 //! Epistemic note (pattern from `hyperpolymath/epistemic-types`, not a
-//! dependency): a level computed here is a *warrant* — echidnabot's own
-//! reading of ECHIDNA's output. When ECHIDNA itself supplies trust data in an
-//! `echidna.prove.result/1` object, that is the *receipt* and is preferred;
-//! see [`crate::dispatcher::TrustSource`].
+//! dependency): a level computed here is a local assessment, not a formally
+//! sound warrant. The direct REST path parses ECHIDNA's typed receipt but
+//! merges local axioms and recomputes confidence; the enriched result is not
+//! the original receipt. See [`crate::dispatcher::TrustSource`]. Mathesis
+//! Grade 3 is a separate proof-evidence grade, not `ConfidenceLevel::Level3`.
 
 use echidna_core::trust::axiom_tracker::DangerLevel;
 use echidna_core::trust::{compute_trust_level, ProverClass, TrustFactors, TrustLevel};