Skip to content

Commit 082587b

Browse files
committed
feat(corpus,security): expand Isabelle corpus to 105 entries and resolve security alerts
- Removed binary artifact: src/chapel/proof_search - Updated dependencies: rand, rustls-webpki - Expanded ProverKind to 105 variants and updated Idris2 injectivity proof - Merged unique Isabelle synthetic proofs from PR #27
1 parent aeac6e3 commit 082587b

11 files changed

Lines changed: 4014 additions & 539 deletions

File tree

CHANGELOG.md

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,16 @@ All notable changes to ECHIDNA will be documented in this file.
55
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
66
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
77

8-
## [Unreleased] - 2026-04-05
8+
## [Unreleased] - 2026-04-20
9+
10+
### Added
11+
- **105 ProverKind variants** (exhaustive HP type-checker ecosystem).
12+
- Updated `ProverKindInjectivity.idr` to prove injectivity for all 105 variants.
13+
- Expanded Isabelle synthetic proof corpus (105 entries).
14+
- Resolved security alerts: Binary-Artifacts (#13), rand (#11, #10), rustls-webpki (#13, #12).
15+
- Atomic repush consolidating corpus expansion and security hardening.
16+
17+
## [2.2.0] - 2026-04-05
918

1019
### Changed
1120

CLAUDE.md

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ This document provides guidelines and context for working with Claude Code on th
44

55
## Project Overview
66

7-
**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 48 prover backends with a comprehensive verification pipeline.
7+
**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 105 prover backends with a comprehensive verification pipeline.
88

99
**Repository**: https://github.com/hyperpolymath/echidna
10-
**Version**: 2.1.0
10+
**Version**: 2.3.0
1111
**License**: PMPL-1.0-or-later
1212

1313
## Repository Structure
1414

1515
```
1616
echidna/
1717
├── src/
18-
│ ├── rust/ # Rust core (48 provers, trust pipeline)
19-
│ │ ├── provers/ # 48 prover backend implementations
18+
│ ├── rust/ # Rust core (105 provers, trust pipeline)
19+
│ │ ├── provers/ # 105 prover backend implementations
2020
│ │ ├── verification/ # Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
2121
│ │ ├── integrity/ # Solver binary integrity (SHAKE3-512, BLAKE3)
2222
│ │ ├── executor/ # Sandboxed solver execution (Podman, bubblewrap)
@@ -70,12 +70,12 @@ Follow conventional commit format:
7070

7171
### Tech Stack
7272

73-
- **Rust**: Core logic, 48 prover backends, trust pipeline, CLI, REPL, API servers
73+
- **Rust**: Core logic, 105 prover backends, trust pipeline, CLI, REPL, API servers
7474
- **Julia**: ML inference (tactic prediction, premise selection, port 8090)
7575
- **ReScript + Deno**: UI components (33 files, zero TypeScript)
7676
- **Chapel**: Optional parallel proof dispatch
7777

78-
### Prover Support (48 Total - ALL IMPLEMENTED)
78+
### Prover Support (105 Total - ALL IMPLEMENTED)
7979

8080
- **Interactive Proof Assistants**: Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F*
8181
- **SMT Solvers**: Z3, CVC5, Alt-Ergo
@@ -101,7 +101,7 @@ The v1.5 trust hardening added:
101101

102102
### Key Components
103103

104-
- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (48 variants), ProverFactory
104+
- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (105 variants), ProverFactory
105105
- `src/rust/dispatch.rs`: Full trust-hardening dispatch pipeline
106106
- `src/rust/verification/`: Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
107107
- `src/rust/integrity/`: Solver binary integrity (SHAKE3-512, BLAKE3)
@@ -114,13 +114,13 @@ The v1.5 trust hardening added:
114114
### Current Status
115115

116116
**Completed (v2.0.0)**:
117-
- 48/48 prover backends across 10 tiers
117+
- 105/105 prover backends across 10 tiers
118118
- Trust & safety hardening (13 tasks complete)
119119
- 638+ tests passing (528 unit + 38 integration + 21 property + interface)
120120
- 3 API interfaces (GraphQL, gRPC, REST) with real prover backend invocation
121121
- Agda meta-checker: 30+ formally verified trust pipeline properties
122122
- Criterion benchmarks: 13 functions covering all critical paths
123-
- FFI bridge: complete C-compatible API for all 48 provers
123+
- FFI bridge: complete C-compatible API for all 105 provers
124124
- Julia ML layer (logistic regression, MRR 0.66)
125125
- 26 CI/CD workflows (including Agda meta-checker)
126126
- Zig FFI layer (4 shared libraries)

0 commit comments

Comments
 (0)