Proof Programme

PROOF-PROGRAMME — first-principles soundness

panic-attack's formal-verification strategy. The full programme lives in PROOF-PROGRAMME.md — this page is the operator-facing orientation.

Status

Tier	Module	What it proves	Status
Foundation	src/abi/PatternCompleteness.idr	PA1 — every Lang / WPCategory has a detector	✅ Qed (2026-04-11)
Foundation	src/abi/ClassificationSoundness.idr	PA2 — Severity total order + maxSeverity commutativity	✅ Qed (2026-04-11)
Layer 1.0	src/abi/Stripping.idr	Line-comment-strip foundation lemmas + base cases of stripLineCommentsIdempotent	**~ Partial (2026-06-02)** — shape lemma + base cases Qed-closed; slash-slash inductive closure open
Layer 1.1–1.25	(not yet started)	Per-PA-code soundness + completeness (25 obligations)	Open
Layer 2.1	(not yet started)	miniKanren unification + search correctness (Coq, ~1500 LoC)	Open
Layer 2.2	(not yet started)	Taint propagation completeness (fixed-point lattice in Coq)	Open
Layer 3.1	(not yet started)	Hexad ↔ Octad round-trip (proptest sufficient)	Open
Layer 3.2	(not yet started)	Attestation chain unforgeability (Idris2 + Ed25519 EUF-CMA assumption)	Open
Layer 3.3	(not yet started)	Bridge reachability soundness (Coq graph)	Open

Three layers

Surface — per-category detection (Layer 1.0–1.25)

For each WeakPointCategory, prove:

• Soundness: every detector emission corresponds to a real instance of the pattern.
• Completeness: every real instance of the pattern is detected (modulo declared scope — e.g. test files, see Context-Awareness).

PA1 proves DISPATCH completeness (every category has a detector). PA2 proves SEVERITY ordering on what's emitted. Layer-1 work extends this per category to the pattern-recognition function itself.

Layer 1.0 is the common foundation: prove the analyzer's comment/string-stripping pass at src/assail/analyzer.rs:931 is idempotent and preserves non-token positions. Every per-category proof then applies its predicate to strip s and treats strip as a fixed point.

Engine — miniKanren + taint (Layer 2)

src/kanren/core.rs is a microKanren-style engine. Three properties:

1. Unification correctness — unify(u, v, σ) returns σ' iff there's an mgu θ with θ(u) = θ(v) extending σ.
2. Substitution composition — walk*(t, σ) is the canonical representative of t's equivalence class.
3. Search completeness — mplus interleaving doesn't drop a satisfiable goal under bounded depth.

Recommended prover: Coq (Bender/Hemann's miniKanren correctness work is in Coq; reuse).

Layer 2.2 — taint propagation completeness: if a source-to-sink dataflow exists, the rule engine emits a WeakPoint whose recommended_attack reflects the sink. Mechanise as a fixed-point lattice; the kanren engine becomes the procedural computation of the lattice; the proof shows procedural answer = least fixed point.

Persistence + Integrity — hexad / attestation / reachability (Layer 3)

1. Hexad ↔ Octad round-trip — panic-attack-hexad → verisimdb-octad → panic-attack-hexad is the identity on hexad fields. Proptest in Rust is sufficient evidence; formalising in Idris2 would be busywork.
2. Attestation chain unforgeability — Intent → Evidence → Seal with Ed25519 sig. Reduces to standard EUF-CMA. Mechanise via Idris2 + an EUF-CMA assumption + chain structure.
3. Bridge reachability — src/bridge/reachability.rs classifies deps. Property: classify(dep) = Phantom ⇒ dep does not appear on any reachable path from the root. Graph reachability proof in Coq.

proven cross-fit

From the 2026-06-02 survey, only TWO hyperpolymath/proven modules qualify as semantic-equivalent + perf-neutral port-to-Rust candidates:

#	Swap	Where in panic-attack	How
1	SafePath::has_traversal + sanitize_filename	src/abduct/mod.rs:123,266; src/main.rs:2314,2377 (fs::canonicalize(..).unwrap_or_else)	Port to Rust + proptest invariants against proven's Idris2 reference
2	SafeUrl::parse	src/storage/mod.rs:1071 (VERISIMDB_URL currently unvalidated before HTTP POST)	Port to Rust wrapping url::Url + proptest scheme-required invariant

Both NOT via FFI — libproven.so dylib build dep too heavy for cargo install panic-attack's distribution model.

Skip list (semantic mismatch / already total): SafeJson (serde already total + typed), SafeRegex (regex crate is RE2-lineage), SafeDateTime (chrono total on emit), SafeCommand (Command::new doesn't shell-interpolate), SafeEnv (env keys are compile-time literals), SafeUUID (deterministic-timestamp UUIDs by design).

proven gaps (must prove from first principles): miniKanren engine, 49-language analyzer dispatch (PA1 already covers it), hexad/octad data model, A2ML attestation chain, bridge reachability, sweep tracker, adjudicate/axial merge.

Sequencing

Phase	Output	Estimated effort	Risk
1	Layer 1.0 foundation (this slice)	3-5 days	low
2	Quick wins: Hexad↔Octad proptest + Layer 1 PA001/PA004/PA017	1 week	low
3	proven cross-fit: SafePath + SafeUrl ports	1 week	low
4	Layer 3.2 attestation chain	1 week	low
5	Layer 2.1 miniKanren correctness	4 weeks	medium
6	Layer 1.1–1.25 remaining per-category	4 weeks	medium
7	Layer 3.3 bridge reachability	1.5 weeks	medium
8	Layer 2.2 taint completeness	3 weeks	high
9	Layer 2.3 FFI ABI (deferred)	TBD	high

Total to phase 8: ~16 calendar weeks of focused proof work.

Honest gaps

Every new proof module must Qed-close (Coq) or be totality-checked (Idris2) before landing. No Admitted / believe_me / assert_total.

Layer 1.0 slice (#111) ships the foundation lemmas + structural base cases Qed-closed. The slash-slash inductive closure is recorded as an open obligation in PROOF-NEEDS.md — the closure lemma stripIsIdentityOnStrippedBody is the next slice's headline.

Related

• Home
• PROOF-PROGRAMME.md — full programme (in-repo)
• PROOF-NEEDS.md — open-obligation ledger
• Context-Awareness — v2.5.5 module-level FP suppression that the per-PA-code proofs will formally justify