SSProve

Direct answerSSProve brings state-separating, modular game-based proofs to Rocq, letting large cryptographic proofs be assembled from packages. hax can target it from Rust, connecting implementations to proofs.

Maintainer: Aarhus University, MPI-SP and others
Website: https://github.com/SSProve/ssprove
Repository: https://github.com/SSProve/ssprove
Category: Proof systems and computational proofs
Targets: Primitives and protocols in the computational model
Approach: Rocq framework for state-separating proofs; hax backend available
Access: Open source
Status (2026-09-13): Active research

Last reviewed 2026-09-13 by the sorryfree editors.

What SSProve does

SSProve is the natural choice for teams already in Rocq who need computational proofs, and its hax backend is a bridge from production Rust.

Where it is strong

Modular proof structure scales.
Rocq ecosystem and hax bridge.
Foundationally rigorous.

Limits and caveats

Research maturity.
Fewer worked examples than EasyCrypt.
Requires Rocq expertise.

When to choose it

Choose SSProve when your verification stack is Rocq and you need computational proofs, not just implementation correctness.

Who works with SSProve

Cryspen.

Top-listed for proof-system verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

ArkLib, EasyCrypt, CryptoVerif, ProofFrog, Squirrel.

Sources

SSProve repository

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt