ProofFrog

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 and lacks comparable levels of assurance.

Installation

Requires Python 3.11+.

From PyPI

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

After installing, download the examples repository:

proof_frog download-examples

From source

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]"

Documentation

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
• LaTeX export — render FrogLang files to LaTeX (cryptocode pseudocode) via python -m proof_frog export-latex

Emacs. An Emacs major mode providing syntax highlighting, indentation, Imenu navigation, and LSP integration (via eglot or lsp-mode) is available in the emacs folder. See its README for installation instructions.

License

ProofFrog is released under the MIT License.

Acknowledgements

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.