A tool for checking transitions in cryptographic game-hopping proofs.

ProofFrog checks the validity of game hops for cryptographic game-hopping proofs in the reduction-based security paradigm: it checks that the starting and ending games match the security definition, and that each adjacent pair of games is either interchangeable (by code equivalence) or justified by a stated assumption. Proofs are written in FrogLang, a small C/Java-style domain-specific language designed to look like a pen-and-paper proof. ProofFrog can be used from the command line, a browser-based editor, or an MCP server for integration with AI coding assistants. ProofFrog is suitable for introductory level proofs, but is not as expressive for advanced concepts as other verification tools like EasyCrypt.

Requires Python 3.11+.

python3 -m venv .venv
source .venv/bin/activate
pip install proof_frog

After installing, download the examples repository:

proof_frog download-examples

git clone https://github.com/ProofFrog/ProofFrog
cd ProofFrog
git submodule update --init
python3 -m venv .venv
source .venv/bin/activate
pip install -e ".[dev]"

Full documentation is available at prooffrog.github.io, including:

• Tutorial — hands-on introduction to writing and checking proofs, and additional worked examples
• Language reference — complete FrogLang reference
• Examples — catalogue of example proofs, largely adapted from The Joy of Cryptography
• CLI reference — command-line usage
• Web editor — browser-based editing and proof checking
• Information about editor plugins and proving with AI assistants

ProofFrog is released under the MIT License.

ProofFrog was created by Ross Evans and Douglas Stebila, building on the pygamehop tool created by Douglas Stebila and Matthew McKague. For more information about ProofFrog's design, see Ross Evans' master's thesis and eprint 2025/418.

ProofFrog's syntax and approach to modelling is heavily inspired by Mike Rosulek's excellent book The Joy of Cryptography.

We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC).

Includes icons from the vscode-codicons project.