docs: reframe FFI + formal-proofs surfaces as experimental (W2-4) (#48)

## What changed & why

The prod-readiness audit found the Zig FFI and Agda proofs are
aspirational:
FFI ops are placeholders calling no Julia code, the "Idris2 ABI +
generated
header" pipeline in `ABI-FFI-README.md` never existed as anything but
removed
template scaffolding, and the Agda proofs cover discrete ℕ-lemmas, not
the
ℝ/Float64 statistical theorems the docs implied. Per the binding user
decision recorded in `.claude/tasks/prod-readiness/README.md` ("FFI
(Zig/C-ABI)
and Agda proofs are EXPERIMENTAL"), this PR is the docs/positioning
sweep
that follows W1-6 (Zig FFI compiles + CI) and W1-7 (Agda proofs
type-check +
CI) — no `.jl`/`.agda`/`.zig` logic changes, comment-text and docs only.

Work order: `.claude/tasks/prod-readiness/w2-4-experimental-reframe.md`.

### Files changed, before → after

| File | Before | After |
|---|---|---|
| `README.adoc` | No section describing FFI/proofs maturity. | Adds the
single canonical `== Experimental surfaces` section (after Architecture,
before License): labels FFI and Proofs both **Experimental**, states the
FFI entry points are placeholders and the Idris2 ABI layer is
design-only, states the Agda lemmas are ℕ-level not ℝ, and links
`ABI-FFI-README.md` / `proofs/README.adoc` / `PROOF-NEEDS.md`. Confirms
the Julia core remains tested/reference-validated. |
| `ABI-FFI-README.md` | Described the Idris2 ABI + generated-header
pipeline as if it existed; directory tree showed `src/abi/`,
`generated/abi/`, `bindings/` as real. | Adds an EXPERIMENTAL status
banner at the top pointing to README.adoc's canonical section; directory
tree and prose now say plainly that `src/abi/`, `generated/abi/`, and
`bindings/` do not exist in this repo and that only `ffi/zig/` is real
(compiles, CI-tested, placeholder ops). |
| `EXPLAINME.adoc` | Tools table listed "Idris2 ABI" as an available
component; prose claimed "optional formal verification of statistical
properties" and "formal verification that all numerical computation
originates from Julia". | Removes the Idris2 ABI table row (with a NOTE
explaining why); Zig FFI row now says EXPERIMENTAL/placeholder/links
canonical section; "Dogfooded" prose reframed to state the FFI standard
is experimental, the 10 Agda lemmas are ℕ-level proxies not ℝ theorems,
and the Julia-origin guarantee is a code-structure property (executor.jl
boundary), not an Agda-proven one. |
| `PROOF-NEEDS.md` | Title/intro implied a coverage catalogue; "Current
State" claimed `src/abi/*.idr` proofs existed (Idris2 ABI),
self-contradicting its own later "Template ABI Cleanup" note that they
were removed 2026-03-29. | Retitled "Open Proof Targets" with an
EXPERIMENTAL status line up top; "Current State" now says the Idris2
template ABI was removed 2026-03-29 and `src/abi/` does not exist, and
"Existing ABI proofs: none" — resolving the self-contradiction. File is
kept (not deleted), per the work order. |
| `RSR_OUTLINE.adoc` | Generic RSR template doc read as if describing
this repo's actual state. | Adds a NOTE clarifying it documents the
generic template Statistikles was bootstrapped from, that `src/abi/` in
it is target layout only, and pointing to README.adoc's canonical
section for Statistikles' actual status. |
| `docs/AI-CONVENTIONS.md` | "ABI/FFI Standard" section listed Idris2
ABI (`src/abi/`) and generated headers (`generated/abi/`) as standard
components without qualification. | Reframed as "Target design"; each
bullet now states explicitly what is/isn't present — Idris2 ABI "not
present in this repo; design-only", Zig FFI "real and CI-tested, but
EXPERIMENTAL: … placeholders", generated headers "not present; no
generation pipeline exists yet". |
| `docs/CROSS-VERIFICATION-ARCHITECTURE.md` | Layer 3 (ECHIDNA)
described as doing "Formal proofs of statistical identities via
Agda/Lean 4" without qualification; Layer 5 (TypeLL) described L10 as
"formally-proven epistemological types" without qualification. | Adds an
ASPIRATIONAL status banner at the top scoping the whole document; Layer
3 now says "planned; not wired up" and clarifies the 10 existing Agda
lemmas are ℕ-proxies, not ℝ identities, and ECHIDNA dispatch from
`echidna_adapter.jl` isn't implemented; Layer 5 clarifies L9-10 are a
target dependent on the unwired Layer-3 pipeline, so no value in the
codebase currently carries an L9/L10 guarantee. |
| `proofs/README.adoc` | Already had an accurate EXPERIMENTAL status
paragraph (from W1-7) but didn't point back to a repo-wide canonical
section. | Adds a one-line pointer to README.adoc's "Experimental
surfaces" section so the two docs can't drift apart. |
| `.well-known/humans.txt` | `Components: Idris2 ABI, Zig FFI`
(unqualified, implies both exist/are real). | `Components: Zig FFI
(experimental — placeholder ops); Idris2 ABI (design-only, not
present)`. |
| `src/bridge/echidna_adapter.jl` | Module header: "Formal proof
dispatch for statistical properties. Dispatches proof obligations to
ECHIDNA's 48-prover backend…"; docstring: "Statistical property that can
be formally verified." — both present-tense, implying live dispatch. |
Header retitled "EXPERIMENTAL / design-only proof-dispatch scaffolding",
states dispatch is not wired up and the identities below are proof
*targets*, not currently-formally-verified statements; docstring
reworded to "Statistical property targeted for future formal
verification (not yet dispatched…)". No logic changed. |
| `src/bridge/typell_levels.jl` | Comment described Levels 9-12 as "by
external proof systems" without flagging they're unconnected. | Adds
EXPERIMENTAL/scaffolding notes at the top-level comment and above the
Level 9-10 struct definitions, stating no value in the codebase
currently carries a Level 9-12 guarantee and the ECHIDNA dispatch that
would populate one isn't wired up. No logic changed. |
| `.machine_readable/6a2/STATE.a2ml` | No machine-readable maturity
fields for FFI/proofs. | Adds an `[experimental-surfaces]` block
mirroring README.adoc's wording exactly (`ffi-maturity =
"experimental"`, `proof-maturity = "experimental"` + matching notes), so
the human- and machine-readable claims can't drift apart. Valid a2ml
`[section]` / `key = "value"` syntax, consistent with sibling files. |

Not touched: the Julia core's tested/reference-validated claims (per the
work
order's requirement 5) and `PROOF-NEEDS.md` was relabelled, not deleted.

## Verification run & result

**Acceptance criterion 1** — `git grep -in "formally verified\|formally
proven"` (excluding `.claude/tasks/`):

```
$ git grep -in "formally verified\|formally proven" -- . ':!.claude/tasks'
.machine_readable/integrations/proven.a2ml:2:# Proven Integration — Formally Verified Safety Library
src/bridge/echidna_adapter.jl:8:# currently formally verified. If/when wired up, the intent is to route to:
```

Both hits are accurate: `proven.a2ml` describes the external,
actually-proven
`hyperpolymath/proven` safety library (unrelated to this repo's
FFI/proofs
boundary — different subject entirely), and the `echidna_adapter.jl` hit
is
itself the "not yet / not currently" phrasing this task requires ("…are
proof
*targets*, not statements that are **currently formally verified**"). No
stray present-tense claims remain.

**Acceptance criterion 2** — no doc asserts the C-ABI reaches the stats
core:
confirmed by review of every touched file above; `ABI-FFI-README.md`,
`docs/AI-CONVENTIONS.md`, and `.well-known/humans.txt` now explicitly
state
the FFI entry points are placeholders not backed by the Julia core.

**Acceptance criterion 3** — single canonical section:

```
$ grep -rn "Experimental surfaces" --include='*.adoc' --include='*.md' --include='*.a2ml' .
README.adoc:137:== Experimental surfaces          (the only place the section is *defined*)
ABI-FFI-README.md                                  (links it)
EXPLAINME.adoc                                     (links it)
PROOF-NEEDS.md                                      (links it)
RSR_OUTLINE.adoc                                    (links it)
docs/CROSS-VERIFICATION-ARCHITECTURE.md             (links it)
proofs/README.adoc                                  (links it)
.machine_readable/6a2/STATE.a2ml                    (mirrors it, machine-readable)
```

**Acceptance criterion 4 (A2ML validation)** —
`.machine_readable/6a2/STATE.a2ml`
is the only `.a2ml` file this PR touches (adds the
`[experimental-surfaces]`
block). Locally verified bracket/quote balance and structural
consistency
with sibling `.machine_readable/6a2/*.a2ml` files (`[section]` headers,
`key = "value"` pairs) — no local `a2ml-validate-action` binary is
available
in this sandbox, so the authoritative check is the "Validate A2ML
manifests"
job in `.github/workflows/dogfood-gate.yml` (`a2ml-validate`), which
triggers
on `pull_request: branches: ['**']` and will run against this PR.

## Anything skipped

Nothing in scope was skipped. Out of scope per the work order (deferred
by
user decision, not attempted here): making the FFI real or proving the
statistical theorems over ℝ; no code logic changed beyond comment-text.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -24,3 +24,11 @@ test-count = 632
 test-count-note = "@test assertions across runtests.jl, e2e_test.jl, property_test.jl, reference_validation_test.jl"
 test-failures = 0
 ci-workflows = 14
+
+[experimental-surfaces]
+# Machine-readable mirror of README.adoc's "Experimental surfaces" section.
+# Keep in sync; neither field may claim more than the human-readable docs do.
+ffi-maturity = "experimental"
+ffi-note = "ffi/zig compiles and is CI-tested; entry points are placeholders not yet backed by the Julia core; the Idris2 ABI layer (src/abi/) is design-only and does not exist in this repo"
+proof-maturity = "experimental"
+proof-note = "10 Agda lemmas type-checked by agda --safe in CI, proven over ℕ as discrete proxies; the statistical theorems over ℝ/Float64 remain open targets (see PROOF-NEEDS.md)"

.well-known/humans.txt

@@ -10,5 +10,5 @@ From: United Kingdom
 Last update: 2026-02-20
 Standards: RSR (Rhodium Standard Repository)
 License: MPL-2.0 (Palimpsest MPL)
-Components: Idris2 ABI, Zig FFI
+Components: Zig FFI (experimental — placeholder ops); Idris2 ABI (design-only, not present)
 Tools: just, Podman, Guix

ABI-FFI-README.md

@@ -4,14 +4,28 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # STATISTIKLES ABI/FFI Documentation
 
+> **STATUS — EXPERIMENTAL.** The Zig FFI compiles and is CI-tested
+> (`.github/workflows/zig.yml`), but its exported entry points are placeholders,
+> not yet backed by the Julia statistical core. The Idris2 ABI layer described
+> below is **design-only**: `src/abi/` does not exist in this repo (the template
+> scaffolding that once lived there was removed — see `PROOF-NEEDS.md`, "Template
+> ABI Cleanup"). Everything in this document past this notice describes the
+> *intended* Hyperpolymath RSR design, not the current state of this repository.
+> See the "Experimental surfaces" section of `README.adoc` for the canonical
+> summary.
+
 ## Overview
 
-This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
+This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design
+(target design; not yet fully implemented in this repo):
 
-- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs
+- **ABI (Application Binary Interface)** *intended* to be defined in **Idris2**
+  with formal proofs — not yet present (`src/abi/` does not exist)
 - **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility
-- **Generated C headers** bridge Idris2 ABI to Zig FFI
-- **Any language** can call through standard C ABI
+  — compiles and is CI-tested, but operations are placeholders
+- **Generated C headers** *would* bridge Idris2 ABI to Zig FFI — no generation
+  pipeline exists yet
+- **Any language** can call through the standard C ABI once real operations land
 
 ## Architecture
 
@@ -51,10 +65,13 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
 
 ## Directory Structure
 
+The tree below is the *target* layout. `src/abi/`, `generated/abi/`, and
+`bindings/` do not exist in this repo yet — only `ffi/zig/` is real.
+
 ```
 statistikles/
 ├── src/
-│   ├── abi/                    # ABI definitions (Idris2)
+│   ├── abi/                    # NOT PRESENT — ABI definitions (Idris2), design-only
 │   │   ├── Types.idr           # Core type definitions with proofs
 │   │   ├── Layout.idr          # Memory layout verification
 │   │   └── Foreign.idr         # FFI function declarations
@@ -71,11 +88,11 @@ statistikles/
 │       └── include/
 │           └── statistikles.h   # C header (optional, can be generated)
 │
-├── generated/                  # Auto-generated files
+├── generated/                  # NOT PRESENT — auto-generated files
 │   └── abi/
-│       └── statistikles.h       # Generated from Idris2 ABI
+│       └── statistikles.h       # Would be generated from Idris2 ABI
 │
-└── bindings/                   # Language-specific wrappers (optional)
+└── bindings/                   # NOT PRESENT — language-specific wrappers (optional)
     ├── rust/
     ├── rescript/
     └── julia/
@@ -197,7 +214,10 @@ zig build -Doptimize=ReleaseFast  # Build optimized
 zig build test                    # Run tests
 ```
 
-### Generate C Header from Idris2 ABI
+### Generate C Header from Idris2 ABI (target design — not runnable today)
+
+`src/abi/` does not exist in this repo, so the command below has no `Types.idr`
+to compile. It documents the intended pipeline only.
 
 ```bash
 cd src/abi
@@ -332,7 +352,10 @@ cd ffi/zig
 zig build test-integration
 ```
 
-### ABI Verification (Idris2)
+### ABI Verification (Idris2) (target design — not runnable today)
+
+There is no Idris2 ABI in this repo to run `verifyABI`/`verifyLayoutsCorrect`
+against; this block documents the intended verification surface only.
 
 ```idris
 -- Compile-time verification
@@ -350,7 +373,8 @@ main = do
 
 When modifying the ABI/FFI:
 
-1. **Update ABI first** (`src/abi/*.idr`)
+1. **Update ABI first** (`src/abi/*.idr`) — target design; `src/abi/` does not
+   exist yet, so this step is currently a no-op
    - Modify type definitions
    - Update proofs
    - Ensure backward compatibility

EXPLAINME.adoc

@@ -64,18 +64,29 @@ checked against independently-derived ground-truth values in
 | **Distributions.jl** | Probability distributions
 | **DataFrames.jl** | Tabular data manipulation
 | **LM Studio** | Local LLM for neural routing (localhost:1234)
-| **Idris2 ABI** | https://www.idris-lang.org (optional formal proofs of statistical invariants)
-| **Zig FFI** | https://ziglang.org (optional high-performance bridges)
+| **Zig FFI** | https://ziglang.org (EXPERIMENTAL — compiles and is CI-tested, but entry points are placeholders not yet backed by the Julia core; see "Experimental surfaces" in README.adoc)
 |===
 
+NOTE: An earlier draft of this table listed an "Idris2 ABI" row. `src/abi/` does
+not exist in this repo — the Idris2 ABI layer is design-only. See
+`ABI-FFI-README.md` for the target design and README.adoc's "Experimental
+surfaces" section for the canonical status.
+
 == Dogfooded Across The Account
 
-Uses the hyperpolymath ABI/FFI standard (Idris2 + Zig) for optional formal verification of statistical properties.
+Uses the hyperpolymath FFI standard (Zig) for the C-ABI boundary. FFI is
+EXPERIMENTAL: it compiles and is CI-tested, but its ops are placeholders, not
+Julia-backed. The Idris2 ABI half of the standard is design-only here.
 
 Statistikles-specific:
 - Neural-symbolic boundary enforcement via execute_tool() (src/tools/executor.jl)
-- Optional Idris2 proofs for invariants like "p-value ∈ [0,1]" and "variance ≥ 0"
-- Formal verification that all numerical computation originates from Julia
+- `proofs/` has 10 Agda lemmas type-checked under `agda --safe` in CI, proven
+  over ℕ as discrete proxies (e.g. for "p-value ∈ [0,1]" and "variance ≥ 0");
+  the ℝ/Float64 statistical theorems themselves remain open targets — see
+  `proofs/README.adoc` and `PROOF-NEEDS.md`
+- Deterministic execution: all numerical computation originates from Julia,
+  enforced by the neural-symbolic boundary above (this is a code-structure
+  guarantee, not an Agda-proven one)
 
 == File Map: Key Modules
 

PROOF-NEEDS.md

@@ -2,12 +2,21 @@
 SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
-# PROOF-NEEDS.md
+# PROOF-NEEDS.md — Open Proof Targets
+
+*Status: EXPERIMENTAL.* This file catalogues **open targets** for the Agda
+proof suite in `proofs/` — work not yet done, not a claim of coverage. For the
+proofs that already exist and what they actually prove (ℕ-level lemmas, not
+the ℝ/Float64 statistical theorems), see `proofs/README.adoc`. For the overall
+FFI + proofs status, see the "Experimental surfaces" section of `README.adoc`.
+
 ## Current State
 
 - **LOC**: ~11,900
-- **Languages**: Julia, Agda, Idris2, Zig
-- **Existing ABI proofs**: `src/abi/*.idr` (template-level)
+- **Languages**: Julia, Agda, Zig (Idris2 template ABI removed 2026-03-29 — see
+  "Template ABI Cleanup" below; `src/abi/` does not exist)
+- **Existing ABI proofs**: none — the template-level `src/abi/*.idr` files were
+  removed 2026-03-29 for creating a false impression of formal verification
 - **Existing verification**: 3 Agda proof files in `proofs/Statistikles/`
   - `Inequalities.agda` — statistical inequalities
   - `RankIdentities.agda` — rank-based test identities

README.adoc

@@ -134,6 +134,21 @@ The boundary is `src/tools/executor.jl:execute_tool()`. Everything above it is n
 statistical value crosses this boundary in the upward direction without having been
 computed by a verified Julia function.
 
+== Experimental surfaces
+
+Two boundaries in this repo are pre-production. Both compile and are CI-checked, but
+neither backs the claims their names might suggest:
+
+* **FFI (`ffi/zig/`)** — *Experimental.* Compiles and is CI-tested, but the exported
+  entry points are placeholders not yet backed by the Julia core; the Idris2 ABI layer
+  is design-only (`src/abi/` does not exist in this repo). Details: `ABI-FFI-README.md`.
+* **Proofs (`proofs/`)** — *Experimental.* Small ℕ-level lemmas type-checked by
+  `agda --safe` in CI; the statistical theorems over ℝ remain open targets. Details:
+  `proofs/README.adoc` (proof catalogue) and `PROOF-NEEDS.md` (open targets).
+
+Neither boundary weakens the Julia statistical core, which is tested and
+reference-validated (see `test/reference_validation_test.jl`).
+
 == License
 
 This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details.

RSR_OUTLINE.adoc

@@ -11,6 +11,12 @@ image:https://img.shields.io/badge/RSR-Infrastructure-cd7f32[RSR Infrastructure]
 image:https://img.shields.io/badge/Phase-Maintenance-brightgreen[Phase]
 image:https://img.shields.io/badge/Guix-Primary-purple?logo=gnu[Guix]
 
+NOTE: This file documents the generic RSR *template* that Statistikles was
+bootstrapped from — it is not a status report on this repo. In particular,
+`src/abi/` (Idris2 ABI) below is part of the template's target layout and
+does **not** exist in this repository; see the "Experimental surfaces"
+section of `README.adoc` for Statistikles' actual FFI/proofs status.
+
 == Overview
 
 **The canonical template for RSR (Rhodium Standard Repository) projects.**

docs/AI-CONVENTIONS.md

@@ -63,9 +63,16 @@ NEUROSYM.a2ml, or PLAYBOOK.a2ml in the repository root.
 
 ## ABI/FFI Standard
 
-- ABI definitions: **Idris2** with dependent types (`src/abi/`).
-- FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`).
-- Generated C headers: `generated/abi/`.
+Target design (Hyperpolymath RSR standard) — see README.adoc's "Experimental
+surfaces" section for current status:
+
+- ABI definitions: **Idris2** with dependent types (`src/abi/`) — **not present
+  in this repo**; design-only. Do not assume `src/abi/` exists.
+- FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`) — real and
+  CI-tested, but EXPERIMENTAL: exported ops are placeholders, not yet backed
+  by the Julia core.
+- Generated C headers: `generated/abi/` — not present; no generation pipeline
+  exists yet.
 
 ## Build System
 

docs/CROSS-VERIFICATION-ARCHITECTURE.md

@@ -4,6 +4,14 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Cross-Verification Architecture
 
+*Status: ASPIRATIONAL.* This document describes the target multi-repo
+verification architecture. Only Layer 1 (Statistikles/Julia computation) and
+a small experimental slice of Layer 3 (10 ℕ-level Agda lemmas, not statistical
+identities over ℝ) exist today; Aspasia, ECHIDNA arbitration, VeriSimDB
+persistence, and TypeLL levels 9-12 are design targets, not implemented
+integrations. See the "Experimental surfaces" section of `README.adoc` for the
+current, honest status of the FFI and proofs boundaries specifically.
+
 ## Three-Body Verification Triangle
 
 ```
@@ -26,15 +34,22 @@ Statistikles ◄─────────────────► Aspasia
 - Socratic engine: numerical, ontological, interpretation checks
 - 6-step resolution ladder for disagreements (NIST StRD → Interval → Symbolic → Human)
 
-### Layer 3: ECHIDNA (Rust + 48 provers) — Arbitration
-- Formal proofs of statistical identities via Agda/Lean 4
+### Layer 3: ECHIDNA (Rust + 48 provers) — Arbitration (planned; not wired up)
+- Target: formal proofs of statistical identities via Agda/Lean 4. Today,
+  `proofs/` has 10 Agda lemmas proven over ℕ as discrete proxies — not
+  statistical identities over ℝ — and ECHIDNA dispatch from
+  `src/bridge/echidna_adapter.jl` is not yet implemented (see
+  `proofs/README.adoc`, "Integration with ECHIDNA (aspirational)")
 - SMT verification of arithmetic properties via Z3/CVC5
 - Trust levels 1-5 for every verified property
 
 ### Layer 4: VeriSimDB (Port 8096) — Persistence
 - All results, audits, proofs persisted with VQL-UT queries
 - 8 modalities: numerical, audit, proof, metadata, timeseries, graph, raw, config
 
-### Layer 5: TypeLL (Levels 1-10) — Type Safety
-- From simple Float64 (L1) to formally-proven epistemological types (L10)
-- Tropical semiring types at L7-8, verification provenance at L9-10
+### Layer 5: TypeLL (Levels 1-10) — Type Safety (L1-3 real; L9-10 target)
+- From simple Float64 (L1) to a *target* of formally-proven epistemological
+  types (L10) — L9-10 depend on the Layer 3 proof/verification pipeline above,
+  which is not yet wired up, so no value in this codebase actually carries an
+  L9/L10 guarantee yet
+- Tropical semiring types at L7-8, verification provenance at L9-10 (target)

proofs/README.adoc

@@ -2,6 +2,9 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Statistikles Formal Proofs (Agda)
 
+See also the "Experimental surfaces" section of `README.adoc` for the
+one-line canonical summary of this boundary alongside the FFI one.
+
 *Status: EXPERIMENTAL.* These modules type-check under `agda --safe` with no
 postulates and no holes — but they are *not yet* proofs of the statistical
 theorems Statistikles relies on. Every lemma below is stated and proven over