SSProve: State-separating modular game-based proofs in Rocq
===========================================================

SSProve 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
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: Active research
Strengths: Modular proof structure scales. | Rocq ecosystem and hax bridge. | Foundationally rigorous.
Limits: Research maturity. | Fewer worked examples than EasyCrypt. | Requires Rocq expertise.
Firms using it: Cryspen
Sources: https://github.com/SSProve/ssprove

Source page: https://sorryfree.com/frameworks/ssprove/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13