Skip to content

Commit 6f0c04b

Browse files
committed
docs(claude-md): correct stale 'v2.2+ Tamarin/ProVerif bridge' entry
Investigation found both backends already fully shipped inside the 105 prover count: - provers/tamarin.rs: 596 LoC, 5 tests, .spthy generation + output parsing + interactive tactics (add_rule/add_lemma/add_restriction/add_builtin), shells out to tamarin-prover - provers/proverif.rs: 800 LoC, 8 tests, .pv generation + output parsing, shells out to proverif Both are wired end-to-end: ProverKind variants (mod.rs:168-169), factory dispatch (mod.rs:1259-1260), FFI codes (ffi/mod.rs 44/45), Idris2 ProverKindInjectivity proof. STATE.md 2026-04-19 confirms 'fully wired'. Real remaining gaps are Wave-3 tracked: no .spthy/.pv corpus fixtures, no CI provisioning for upstream binaries.
1 parent 8442821 commit 6f0c04b

1 file changed

Lines changed: 7 additions & 1 deletion

File tree

CLAUDE.md

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,13 @@ The v1.5 trust hardening added:
137137
**Next (v2.2+)**:
138138
- Train GNN/Transformer on larger corpus (Flux.jl)
139139
- Chapel → Rust C FFI bridge
140-
- Tamarin/ProVerif bridge
140+
141+
Note: Tamarin (`provers/tamarin.rs`, 596 LoC, 5 tests) and ProVerif
142+
(`provers/proverif.rs`, 800 LoC, 8 tests) are already shipped as real
143+
backends inside the 105 prover count — an earlier "v2.2+ Tamarin/ProVerif
144+
bridge" entry was stale doc. Corpus fixtures (`.spthy` / `.pv` samples)
145+
and CI provisioning of `tamarin-prover` / `proverif` binaries are tracked
146+
as Wave-3 work in `docs/handover/TODO.md`.
141147

142148
## Useful Commands
143149

0 commit comments

Comments
 (0)