feat(v2.5.0): proof_drift category — 49-language support, PA021

Add ProofDrift (PA021) weak point category detecting formal verification
drift across all estate proof assistant languages:

- Isabelle: sorry, oops, axiomatization
- Coq/Rocq: Admitted, admit tactic, Axiom/Parameter, Obj.magic in extractions
- Lean4: sorry (upgraded Critical, was High), unsafeNativeIO/unsafeBaseIO
- Agda: trustMe/primTrustMe (upgraded Critical), TERMINATING pragma, postulate
- Idris2: assert_total (High), %partial (Medium) — believe_me already ProofDrift
- Julia mirrors: # sorry/# TODO: prove/# admitted comments; @test x isa Y patterns

Language count 47 → 49 (Isabelle + Coq added with dedicated analyzers and
dispatch arms). Category count 20 → 21. PatternCompleteness.idr updated to
maintain completeness proof. PA021 wired into panicbot translator at 0.92
confidence, Control tier.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.claude/CLAUDE.md

@@ -24,7 +24,7 @@ src/
 ├── types.rs             # Core types (AssailReport, WeakPoint, etc.)
 ├── assail/              # Static analysis engine
 │   ├── mod.rs           # Public API: analyze(), analyze_verbose()
-│   ├── analyzer.rs      # 47-language analyzer with per-file detection
+│   ├── analyzer.rs      # 49-language analyzer with per-file detection
 │   └── patterns.rs      # Language-specific attack patterns
 ├── kanren/              # miniKanren-inspired logic engine (v2.0.0)
 │   ├── mod.rs           # Module entry, re-exports
@@ -88,8 +88,8 @@ cp target/release/panic-attack ~/.asdf/installs/rust/nightly/bin/
 
 ## Key Design Decisions
 
-- **47 language analyzers**: Rust, C/C++, Go, Python, JavaScript, Ruby, Elixir, Erlang, Gleam, ReScript, OCaml, SML, Scheme, Racket, Haskell, PureScript, Idris, Lean, Agda, Prolog, Logtalk, Datalog, Zig, Ada, Odin, Nim, Pony, D, Nickel, Nix, Shell, Julia, Lua, + 12 nextgen DSLs
-- **20 weak point categories**: UnsafeCode, PanicPath, CommandInjection, UnsafeDeserialization, AtomExhaustion, UnsafeFFI, PathTraversal, HardcodedSecret, etc.
+- **49 language analyzers**: Rust, C/C++, Go, Python, JavaScript, Ruby, Elixir, Erlang, Gleam, ReScript, OCaml, SML, Scheme, Racket, Haskell, PureScript, Idris, Lean, Agda, Isabelle, Coq, Prolog, Logtalk, Datalog, Zig, Ada, Odin, Nim, Pony, D, Nickel, Nix, Shell, Julia, Lua, + 12 nextgen DSLs
+- **21 weak point categories**: UnsafeCode, PanicPath, CommandInjection, UnsafeDeserialization, AtomExhaustion, UnsafeFFI, PathTraversal, HardcodedSecret, ProofDrift, etc.
 - **Per-file language detection**: Each file analyzed with its own language-specific patterns. Skips `external_corpora/`, `third_party/`, and `corpus/` directories
 - **miniKanren logic engine**: Relational reasoning for taint analysis, cross-language vulnerability chains, and search strategy optimisation
 - **Latin-1 fallback**: Non-UTF-8 files handled gracefully

CHANGELOG.md

@@ -1,5 +1,42 @@
 # Changelog
 
+## [2.1.0] - 2026-04-12
+
+### Added
+- **ProofDrift category (PA021)**: New weak point category detecting formal verification drift
+  across all proof assistant languages. Catches banned proof escape hatches (`sorry`, `Admitted`,
+  `believe_me`, `oops`, `trustMe`, `assert_total`, `%partial`, `{-# TERMINATING #-}`) and
+  Julia mirror files substituting `@test x isa Y` or `# sorry` comments for formal proofs.
+  Confidence 0.92 — proof escape hatches have essentially no false positives in their file types.
+- **Isabelle/HOL language support**: `.thy` files parsed with `analyze_isabelle()` detecting
+  `sorry`, `oops`, and `axiomatization` as ProofDrift findings.
+- **Coq/Rocq language support**: `.v` files parsed with `analyze_coq()` detecting `Admitted`,
+  `admit` tactic, `Axiom`/`Parameter` declarations, and `Obj.magic` in extraction artifacts.
+- **Isabelle + Coq dispatch**: Both new languages wired into `analyze_inner()` dispatch.
+- **Lean4 ProofDrift upgrade**: `sorry` upgraded from UnsafeCode → ProofDrift (Critical).
+  Added `unsafeNativeIO`/`unsafeBaseIO` as ProofDrift (IO discipline bypass).
+- **Agda ProofDrift upgrade**: `trustMe`/`primTrustMe` upgraded to ProofDrift (Critical).
+  Added `{-# TERMINATING #-}`, `{-# NON_TERMINATING #-}`, bare `postulate` as ProofDrift.
+- **Idris2 ProofDrift upgrade**: `believe_me` already ProofDrift; added `assert_total` (High)
+  and `%partial` (Medium) as ProofDrift findings.
+- **Julia mirror detection**: `# sorry`, `# TODO: prove`, `# admitted` comments and
+  `@test x isa Y` patterns (no value check) flagged as ProofDrift in Julia files.
+- **FP suppression wiring**: `apply_suppression()` now runs on every scan, marking
+  weak points `suppressed: true` when logic engine finds defensive-pattern context.
+  Suppressed items stay in report for audit transparency; filtered by panicbot and CI gates.
+- **PA021 → panicbot**: ProofDrift mapped to fleet category `static-analysis/proof-drift`
+  with 0.92 confidence and Control tier.
+- **Idris2 ABI completeness**: `PatternCompleteness.idr` updated — Isabelle, Coq added to
+  `Lang` enum; ProofDrift added to `WPCategory` with `detectorsFor` covering all new languages.
+- **Hypatia integration**: JSON AssailReport consumed by Hypatia Elixir rules. Logtalk
+  export removed 2026-04-12.
+
+### Changed
+- **Language count**: 47 → 49 (added Isabelle, Coq)
+- **Category count**: 20 → 21 (added ProofDrift)
+- **Verbose output**: Two views — filtered (active, what CI sees) and unfiltered (total,
+  audit transparency) with explicit labelling of what each count means.
+
 ## [2.0.0+] - 2026-03-23
 
 ### Fixed

Cargo.toml

@@ -6,7 +6,7 @@ edition = "2021"
 rust-version = "1.85.0"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 license-file = "LICENSE"
-description = "Universal static analysis, stress testing, and logic-based bug signature detection for 47 languages"
+description = "Universal static analysis, stress testing, and logic-based bug signature detection for 49 languages"
 repository = "https://github.com/hyperpolymath/panic-attack"
 
 [dependencies]

EXPLAINME.adoc

@@ -7,7 +7,7 @@ The README makes claims. This file backs them up.
 
 == Claims Substantiation
 
-=== Claim 1: "47-language static analysis across multiple families"
+=== Claim 1: "49-language static analysis across multiple families"
 
 **How it works:** The `src/assail/analyzer.rs` module implements a per-file language detector that identifies file extension and shebang, dispatching to language-specific pattern matchers in `src/assail/patterns.rs`. Each language family (C/C++, Python, JavaScript, Rust, Go, etc.) has dedicated regex-based weak point detectors (unwrap, panic, unsafe blocks, expect, eval, hardcoded secrets). The analyzer processes 47 distinct language patterns without requiring external parsers—pattern-based shallow analysis enables fast scanning across heterogeneous codebases.
 
@@ -43,7 +43,7 @@ The README makes claims. This file backs them up.
 
 | `src/main.rs` | CLI entry: 20 subcommands (assail, assault, temporal, panll, groove, bridge, etc.)
 | `src/lib.rs` | Library API exposing all analysis engines
-| `src/assail/` | Static analysis (47 languages, 20 weak point categories)
+| `src/assail/` | Static analysis (49 languages, 21 weak point categories)
 | `src/assail/analyzer.rs` | Per-file language detection and pattern matching dispatcher
 | `src/assail/patterns.rs` | Language-specific regex patterns for weak points
 | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang)

ROADMAP.adoc

@@ -6,7 +6,7 @@
 
 = panic-attack Roadmap
 
-_Static analysis and bug signature detection across 47 languages, used in 500+ repos._
+_Static analysis and bug signature detection across 49 languages, used in 500+ repos._
 
 toc::[]
 
@@ -18,7 +18,7 @@ binary, panicbot (gitbot-fleet CI integration), and mass-panic (org-scale batch
 
 **Key capabilities today:**
 
-* 47-language analyzer with per-file detection and 20 weak-point categories
+* 49-language analyzer with per-file detection and 21 weak-point categories
 * miniKanren v2.0.0 logic engine (taint analysis, cross-language reasoning, search strategies)
 * Patch Bridge CVE lifecycle engine (OSV API, reachability scan, phantom dependency detection)
 * Cryptographic attestation chain (intent/evidence/seal)
@@ -34,8 +34,9 @@ binary, panicbot (gitbot-fleet CI integration), and mass-panic (org-scale batch
 * [x] Search strategy: risk-weighted file prioritisation
 * [x] Forward chaining: derive new vulnerability facts from rules
 * [x] Backward queries: find files that could cause a vulnerability type
-* [ ] Context-facts for false-positive suppression (~10 rules, target ~8% -> ~2-3% FP rate)
-* [ ] Context-facts for Hypatia Elixir rules: export FactDB snapshot as JSON for direct consumption by Hypatia rule engine (replaces removed Logtalk export; Hypatia now consumes JSON AssailReport via Elixir rules)
+* [x] Context-facts for false-positive suppression (10 rules active, ~8% -> ~2-3% FP target; heuristics intentionally broad — tune v2.1.1)
+* [x] Hypatia integration: JSON AssailReport consumed by Elixir rules directly (Logtalk export removed 2026-04-12)
+* [x] Isabelle + Coq language support (49 languages total; `.thy` → Isabelle, `.v` → Coq)
 
 == v2.2.0 -- VeriSimDB Integration
 
@@ -90,10 +91,12 @@ The estate maintains Isabelle theories, Idris2 ABI definitions, and Lean4/Agda
 proofs alongside Julia/Rust mirrors.  Nothing currently checks that the mirrors
 stay in sync with their formal counterparts.
 
-* [ ] Detect `sorry` / `Admitted` / `believe_me` / `unsafeCoerce` / `Obj.magic` in formal files (`.thy`, `.idr`, `.lean`, `.agda`) — these are the estate's banned dangerous patterns
-* [ ] Detect `@assert` / `@test` standing in for a formally proven theorem in Julia mirror files
+* [x] Detect `sorry` / `Admitted` / `believe_me` / `oops` / `trustMe` in formal files (`.thy`, `.idr`, `.lean`, `.agda`, `.v`) — banned proof escape hatches (PA021)
+* [x] Detect `assert_total` / `%partial` in Idris2, `{-# TERMINATING #-}` / `postulate` in Agda, `axiomatization` in Isabelle, `Axiom`/`Parameter` in Coq — totality/axiom bypasses
+* [x] Detect `@test x isa Y` (no value check) standing in for a formally proven theorem in Julia mirror files
+* [x] Detect `# sorry` / `# TODO: prove` / `# admitted` comments in Julia mirror implementations
 * [ ] Flag Rust/Julia functions whose name matches an Isabelle definition but whose signature has drifted
-* [ ] Detect `# TODO: prove` / `-- sorry` comments in mirror implementations
+* [ ] Detect `Obj.magic` in Coq-extracted OCaml (upstream axiom bypass in extracted artifacts)
 
 === `input_boundary` — Structured-data parsing and deserialization
 

src/abi/PatternCompleteness.idr

@@ -21,7 +21,7 @@ module PanicAttack.ABI.PatternCompleteness
 -- Language enumeration (mirrors src/types.rs Language enum, 47 variants)
 -- ═══════════════════════════════════════════════════════════════════════
 
-||| All 47 programming languages supported by the scanner.
+||| All 49 programming languages supported by the scanner.
 ||| This MUST stay in sync with src/types.rs Language enum.
 public export
 data Lang
@@ -35,7 +35,7 @@ data Lang
   -- Functional
   | Haskell | PureScript
   -- Proof assistants
-  | Idris | Lean | Agda
+  | Idris | Lean | Agda | Isabelle | Coq
   -- Logic programming
   | Prolog | Logtalk | Datalog
   -- Systems languages
@@ -90,6 +90,8 @@ analyzerFor PureScript    = SpecificAnalyzer
 analyzerFor Idris         = SpecificAnalyzer
 analyzerFor Lean          = SpecificAnalyzer
 analyzerFor Agda          = SpecificAnalyzer
+analyzerFor Isabelle      = SpecificAnalyzer
+analyzerFor Coq           = SpecificAnalyzer
 analyzerFor Prolog        = SpecificAnalyzer
 analyzerFor Logtalk       = SpecificAnalyzer
 analyzerFor Datalog       = SpecificAnalyzer
@@ -145,7 +147,7 @@ crossLangAlwaysApplied _ = MkCrossLangChecked
 -- WeakPointCategory enumeration (mirrors src/types.rs, 20 categories)
 -- ═══════════════════════════════════════════════════════════════════════
 
-||| All 20 weak point categories detectable by the scanner.
+||| All 21 weak point categories detectable by the scanner.
 public export
 data WPCategory
   = UncheckedAllocation
@@ -168,6 +170,10 @@ data WPCategory
   | UncheckedError
   | InfiniteRecursion
   | UnsafeTypeCoercion
+  ||| Formal verification drift: banned proof escape hatches or mirror files
+  ||| substituting assertions for proofs. Detected in .idr, .lean, .agda,
+  ||| .thy, .v, and Julia mirror files.
+  | ProofDrift
 
 ||| Witness that a detection rule exists for a weak point category.
 ||| Each variant names the language(s) whose analyzer detects it.
@@ -177,7 +183,7 @@ data HasDetector : WPCategory -> Type where
   DetectedBy : (langs : List Lang) -> HasDetector cat
 
 ||| Every weak point category has at least one detector.
-||| Total: Idris2 verifies all 20 constructors are covered.
+||| Total: Idris2 verifies all 21 constructors are covered.
 ||| The list of detecting languages mirrors the actual pattern
 ||| matching code in analyzer.rs.
 public export
@@ -202,6 +208,7 @@ detectorsFor HardcodedSecret      = DetectedBy [Rust, C, Cpp, Go, Python, JavaSc
 detectorsFor UncheckedError       = DetectedBy [Go, Rust, C, Cpp]
 detectorsFor InfiniteRecursion    = DetectedBy [Haskell, PureScript, Scheme, Racket]
 detectorsFor UnsafeTypeCoercion   = DetectedBy [OCaml, Haskell, DLang, Nim]
+detectorsFor ProofDrift           = DetectedBy [Idris, Lean, Agda, Isabelle, Coq, Julia]
 
 ||| Proof: every weak point category has at least one detector.
 public export