Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
55b1132
feat(aspect): add slug() and dotted_key() canonical-form methods
claude May 25, 2026
ac071e7
feat(agent): AspectTagger auto-populates goal.aspects via dotted_key(…
claude May 25, 2026
4f0477b
refactor(test): migrate 10 hardcoded aspect literals to Aspect::dotte…
claude May 25, 2026
b59059a
feat(learning): boundary filter — only dotted aspects reach domain_hi…
claude May 25, 2026
d5554ec
docs(statistics): update docstring with canonical "category.aspect" f…
claude May 25, 2026
32a275a
feat(julia): apply_domain_weights gains category-prefix rollup on exa…
claude May 25, 2026
1bff8cf
docs(handover): THEOREM-METADATA-MIGRATION follow-up plan
claude May 25, 2026
c907176
Merge branch 'main' into claude/amazing-cori-KwA2V
hyperpolymath May 25, 2026
9cce60d
test(perf): bump backend-creation wall from 100ms to 250ms
hyperpolymath May 26, 2026
dc92271
chore(docs): move loose root analysis files to docs/design/
claude May 26, 2026
bd89129
chore(docs): relocate planning, warmup, and academic files
claude May 26, 2026
f9d723f
chore(scripts): move corpus-balance shell scripts from root to scripts/
claude May 26, 2026
89290fb
chore(reports): collect security scan outputs in reports/
claude May 26, 2026
a764a11
chore(docs): remove 9 superseded one-time-analysis docs
claude May 26, 2026
4c1a18e
chore(docs): remove 20 version-archaeology docs pinned to v1.0/v1.2/v1.3
claude May 26, 2026
219aa1f
chore(misc): remove 6 sub-project / misc rot files
claude May 26, 2026
aaaa819
chore(config): unify configs/ into config/ per RSR-H11
claude May 26, 2026
e94542a
chore(reports): merge audits/ contents into reports/audits/
claude May 26, 2026
2e098b3
docs: add RSR_COMPLIANCE.adoc at root per RSR-H9 / RSR-S4
claude May 26, 2026
ec102e0
docs(implementation): merge backend reference docs into implementatio…
claude May 26, 2026
ece2f9a
docs: align NOTICE to MPL-2.0 (was still claiming dual MIT/Palimpsest…
claude May 26, 2026
69e2ae8
chore(fmt): apply cargo fmt to D1 + S5 files
claude May 26, 2026
b22ce8e
chore(config): add SPDX-License-Identifier header to config.ncl
claude May 26, 2026
6c52e7f
docs: add canonical human-readable ARCHITECTURE.md
claude May 26, 2026
ab4d7c1
docs: add canonical PROVER_COUNT.md tier table
claude May 26, 2026
8eeed79
docs: add ENV-VARS.md cataloguing every environment variable
claude May 26, 2026
1c77aed
docs(handover): add HANDOVER-INDEX.md navigation map
claude May 26, 2026
21ade8c
docs: align CLAUDE.md + PROVEN-INTEGRATION.md to current state
claude May 26, 2026
434260a
docs(github): update PROVEN-INTEGRATION.md prover count to 128
claude May 26, 2026
894a3cb
Merge main into amazing-cori-KwA2V
hyperpolymath May 26, 2026
df78d82
docs(wiki): canonical wiki page sources, sync target
claude May 26, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/PROVEN-INTEGRATION.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ This document outlines the recommended [proven](https://github.com/hyperpolymath

## Integration Notes

ECHIDNA as a neurosymbolic theorem proving platform supporting 12 provers requires formally verified proof management:
ECHIDNA as a neurosymbolic theorem proving platform supporting 128 prover backends (12 core; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md)) requires formally verified proof management:

- **SafeGraph** models proof dependencies as DAGs. The `Acyclic` proof guarantees no circular dependencies in proof chains, and `topoSort` provides correct ordering for proof verification. `PathExists` verifies lemma reachability.

Expand Down
23 changes: 13 additions & 10 deletions CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,19 +4,22 @@ This document provides guidelines and context for working with Claude Code on th

## Project Overview

**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.
**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 128 prover backends with a comprehensive verification pipeline.

**Repository**: https://github.com/hyperpolymath/echidna
**Version**: 2.3.0
**Version**: 2.3.0 (see `CHANGELOG.md`; release-tag publication tracked in `docs/handover/TODO.md`)
**License**: MPL-2.0
**Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md)
**Canonical prover count**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) (128 total, 12 core)
**Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md)

## Repository Structure

```
echidna/
├── src/
│ ├── rust/ # Rust core (105 provers, trust pipeline)
│ │ ├── provers/ # 105 prover backend implementations
│ ├── rust/ # Rust core (128 provers, trust pipeline)
│ │ ├── provers/ # 128 prover backend implementations
│ │ ├── verification/ # Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
│ │ ├── integrity/ # Solver binary integrity (SHAKE3-512, BLAKE3)
│ │ ├── executor/ # Sandboxed solver execution (Podman, bubblewrap)
Expand All @@ -38,7 +41,7 @@ echidna/
│ │ ├── grpc/ # gRPC (tonic, port 50051)
│ │ └── rest/ # REST (axum + OpenAPI, port 8000)
│ ├── julia/ # Julia ML components
│ └── rescript/ # ReScript+Deno UI (10 files — built locally, not yet shipped)
│ └── rescript/ # ReScript UI (10 files — migration to AffineScript-TEA in progress)
├── .machine_readable/ # A2ML metadata (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml, …)
├── .github/workflows/ # 17 CI/CD workflows
├── Cargo.toml # Rust workspace root
Expand Down Expand Up @@ -69,9 +72,9 @@ Follow conventional commit format:

### Tech Stack

- **Rust**: Core logic, 105 prover backends, trust pipeline, CLI, REPL, API servers
- **Rust**: Core logic, 128 prover backends, trust pipeline, CLI, REPL, API servers
- **Julia**: ML inference (tactic prediction, premise selection, port 8090)
- **ReScript + Deno**: UI components (10 files, zero TypeScript — local build only)
- **AffineScript + Deno** (canonical; migration in progress from `src/rescript/`): UI served by Deno
- **Chapel**: Optional parallel proof dispatch

### Prover Support (105 Total - ALL IMPLEMENTED)
Expand Down Expand Up @@ -100,7 +103,7 @@ The v1.5 trust hardening added:

### Key Components

- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (105 variants), ProverFactory
- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (128 variants), ProverFactory
- `src/rust/dispatch.rs`: Full trust-hardening dispatch pipeline
- `src/rust/verification/`: Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
- `src/rust/integrity/`: Solver binary integrity (SHAKE3-512, BLAKE3)
Expand All @@ -113,13 +116,13 @@ The v1.5 trust hardening added:
### Current Status

**Completed (v2.0.0)**:
- 105/105 prover backends across 10 tiers
- 105/128 prover backends across 10 tiers
- Trust & safety hardening (13 tasks complete)
- 638+ tests passing (528 unit + 38 integration + 21 property + interface)
- 3 API interfaces (GraphQL, gRPC, REST) with real prover backend invocation
- Agda meta-checker: 30+ formally verified trust pipeline properties
- Criterion benchmarks: 13 functions covering all critical paths
- FFI bridge: complete C-compatible API for all 105 provers
- FFI bridge: complete C-compatible API for all 128 provers
- Julia ML layer (logistic regression, MRR 0.66)
- 26 CI/CD workflows (including Agda meta-checker)
- Zig FFI layer (4 shared libraries)
Expand Down
279 changes: 0 additions & 279 deletions ECHIDNA_COMPARISON_ANALYSIS.md

This file was deleted.

Loading
Loading