proof: first-principles proof-obligation map (foundations → non-trivial)

[hyperpolymath]

Proof-obligation map (first principles → non-trivial)

The 2026-05-26 audit reported "no proof debt" — but it only checked for existing proof artifacts (.v/.lean/.agda/.ads…), of which there are none. This issue inverts that: where the system should carry formal guarantees but currently does not.

Framing facts

• esn & lsm declare #![allow(unsafe_code)] but contain zero unsafe blocks — memory-safety is already discharged by the compiler.
• MUST.contractile already forbids proof escape hatches (Admitted/sorry/believe_me/Obj.magic), "removal of formal verification proofs", and "ABI change without proof update" — i.e. it presumes a proof corpus that does not yet exist. These MUSTs are currently vacuous.

Tier 0 — Foundations (totality & numeric well-formedness)

• 0.1 Panic-freedom on operational paths. ~48 unwrap/expect/panic! in neurophone-core, 17 sensors, 11 llm, 10 esn, 7 lsm, 6 bridge. → Result refactor + deny(clippy::unwrap_used); Kani for the provably-infallible ones (e.g. Normal::new(0.5,0.2).unwrap()).
• 0.2 Numeric containment — no NaN/Inf propagation, no integer overflow through the pipelines. → proptest + Kani; F*/Dafny kernel model.
• 0.3 unsafe discipline — switch esn/lsm from allow to #![forbid(unsafe_code)] (also satisfies a declared MUST).

Tier 1 — Core algorithmic correctness

• 1.1 Echo State Property (esn::update): prove the update is a contraction ⇒ fading memory. Sufficient condition ‖W‖∞ < 1 ∧ tanh 1-Lipschitz ∧ leaking-rate convexity. Latent bug: scale_to_spectral_radius actually scales by the max row-sum (∞-norm), not the spectral radius — ESP-sufficient but mislabeled/over-conservative. → Lean/Coq.
• 1.2 LSM bounded dynamics: membrane potential ∈ [reset, θ+ε], refractory respected, bounded firing rate, bounded spike-history memory. → Dafny/F* model of the LIF step + invariant; proptest.
• 1.3 Bridge soundness (bridge): neural→symbolic encoding total, deterministic, round-trips within tolerance. → Coq/Lean relational spec + property tests.

Tier 2 — System orchestration (protocol/state-machine)

• 2.1 Lifecycle safety (NeuroSymbolicSystem: new→initialize→{process|query}*→shutdown): no use before init, no use after shutdown, idempotent shutdown. → TLA+ + TLC; typestate encoding in Rust (illegal transitions unrepresentable; affine-type fit).
• 2.2 Concurrency safety: no deadlock/lost-wakeup (race-freedom already compiler-given). → TLA+ protocol + loom.
• 2.3 Resource/affine lifecycle: sensor/hardware handles acquired & released exactly once. → affine typing (AffineScript) — strongest static-proof candidate.

Tier 3 — Trust boundary / privacy / provenance (PMPL)

• 3.1 Data-egress invariant (claude-client/llm): bound exactly what sensor-derived data crosses device→cloud; no raw PII without consent (PMPL ethical-use). → information-flow/taint spec; TLA+/Alloy egress model + tested allow-list.
• 3.2 Bounded external interaction: retries/timeouts terminate; no request injection. → contracts + proptest.

Recommended toolchain split (within allowed languages)

TLA+ for protocols (2.1, 2.2, 3.1) · Lean/Coq for reservoir math (1.1, 1.3) · Dafny/F* for numeric kernels (1.2, 0.2) · Kani + proptest as the executable bridge to the real Rust.

First concrete step: stand up a proofs/ scaffold (per-toolchain dirs + CI hook) so the existing MUST obligations become enforceable rather than vacuous. Then attack Tier 0 (cheap, broad) and 1.1 (highest-value theorem) first.

Candidate epic; each checkbox can be split into its own issue.