Skip to content

Commit 78127c6

Browse files
docs: clarify v2.2+ roadmap status with implementation details
2 parents 1d5b7de + c411739 commit 78127c6

1 file changed

Lines changed: 28 additions & 4 deletions

File tree

CLAUDE.md

Lines changed: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -134,10 +134,34 @@ The v1.5 trust hardening added:
134134
- Idris2 formal proofs: 7 GNN properties (0 believe_me)
135135
- 28 new tests, 0 clippy warnings
136136

137-
**Next (v2.2+)**:
138-
- Train GNN/Transformer on larger corpus (Flux.jl)
139-
- Chapel → Rust C FFI bridge
140-
- Tamarin/ProVerif bridge
137+
**Next (v2.2+)** (precise status):
138+
139+
- **Chapel → Rust C FFI bridge (L2, half-done)**. Zig shim
140+
(`src/zig_ffi/`, 738 LoC, 4 files) and Chapel POC (`src/chapel/`,
141+
970 LoC) in place behind `--features chapel`; `cargo build --features
142+
chapel` works standalone, 6/6 `proof_search` tests pass. The gap:
143+
`dispatch.rs` still bypasses the feature-gated `ChapelParallelSearch`
144+
strategy in `proof_search.rs`. Integration is split into 7 L2 sub-waves
145+
tracked in `docs/handover/TODO.md`, gated on L1 Cap'n Proto completion.
146+
Direct Rust↔Chapel today goes through Zig (no shortcut path).
147+
148+
- **Train GNN/Transformer on larger corpus (Flux.jl, scaffold-only)**.
149+
Flux.jl is declared in `src/julia/Project.toml` and imported across
150+
9 files; ~1.4k LoC of training scaffolds exist
151+
(`train_advanced_models.jl`, `training/train.jl`,
152+
`models/neural_solver.jl`). **Never invoked on real data**:
153+
`models/neural/` does not exist, `models/model_metadata.txt` reads
154+
`0 words, 0 classes`, and `src/julia/api/gnn_endpoint.jl:40-114`
155+
falls back to cosine similarity when no trained model is found.
156+
Corpus ready: `training_data/` 553 MB, 66,674 proofs / 179,933 tactics
157+
across 16 prover systems — untouched.
158+
159+
Note: Tamarin (`provers/tamarin.rs`, 596 LoC, 5 tests) and ProVerif
160+
(`provers/proverif.rs`, 800 LoC, 8 tests) were previously listed under
161+
v2.2+ as "bridge" work — in fact both are already shipped real backends
162+
inside the 105 prover count. Remaining Wave-3 work for these is corpus
163+
fixtures (`.spthy` / `.pv` samples) and CI provisioning of upstream
164+
binaries, tracked in `docs/handover/TODO.md`.
141165

142166
## Useful Commands
143167

0 commit comments

Comments
 (0)