Metadata-Version: 2.4
Name: proof_frog
Version: 0.5.0
Summary: A tool for checking transitions in cryptographic game-hopping proofs
Keywords: cryptography,game-hopping,proofs
Author-email: Ross Evans <rpevans@uwaterloo.ca>, Douglas Stebila <dstebila@uwaterloo.ca>
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-Expression: MIT
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Programming Language :: Python :: 3.14
Classifier: Topic :: Security :: Cryptography
License-File: LICENSE
Requires-Dist: antlr4-python3-runtime >= 4.13
Requires-Dist: colorama >= 0.4
Requires-Dist: z3-solver >= 4.12
Requires-Dist: sympy >= 1.12
Requires-Dist: flask >= 3.0
Requires-Dist: watchdog >= 4.0
Requires-Dist: click >= 8.0
Requires-Dist: pygls >= 1.3
Requires-Dist: mypy ; extra == "dev"
Requires-Dist: pylint ; extra == "dev"
Requires-Dist: types-colorama ; extra == "dev"
Requires-Dist: pytest ; extra == "dev"
Requires-Dist: pytest-xdist ; extra == "dev"
Requires-Dist: black ; extra == "dev"
Requires-Dist: flit ; extra == "dev"
Requires-Dist: twine ; extra == "dev"
Requires-Dist: mcp[cli] >= 1.0 ; extra == "mcp"
Project-URL: Documentation, https://prooffrog.github.io
Project-URL: Release Notes, https://github.com/ProofFrog/ProofFrog/blob/main/RELEASE.md
Project-URL: Source, https://github.com/ProofFrog/ProofFrog
Provides-Extra: dev
Provides-Extra: mcp

<p align="center">
  <img src="https://github.com/ProofFrog/ProofFrog/blob/main/proof_frog/web/prooffrog.png?raw=true" alt="ProofFrog logo" width="120"/>
</p>

# ProofFrog

[![Tests](https://github.com/ProofFrog/ProofFrog/actions/workflows/test.yml/badge.svg)](https://github.com/ProofFrog/ProofFrog/actions/workflows/test.yml)
[![PyPI](https://img.shields.io/pypi/v/proof_frog)](https://pypi.org/project/proof_frog/)
[![Python](https://img.shields.io/pypi/pyversions/proof_frog)](https://pypi.org/project/proof_frog/)
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://github.com/ProofFrog/ProofFrog/blob/main/LICENSE)

**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.

![ProofFrog web interface](https://raw.githubusercontent.com/ProofFrog/ProofFrog/refs/heads/main/media/screenshot-web.png)

## 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](https://prooffrog.github.io/), including:

- [Tutorial](https://prooffrog.github.io/manual/tutorial/) — hands-on introduction to writing and checking proofs, and additional [worked examples](https://prooffrog.github.io/manual/worked-examples/)
- [Language reference](https://prooffrog.github.io/manual/language-reference/) — complete FrogLang reference
- [Examples](https://prooffrog.github.io/examples/) — catalogue of example proofs, largely adapted from [*The Joy of Cryptography*](https://joyofcryptography.com/)
- [CLI reference](https://prooffrog.github.io/manual/cli-reference/) — command-line usage
- [Web editor](https://prooffrog.github.io/manual/web-editor/) — browser-based editing and proof checking
- Information about [editor plugins](https://prooffrog.github.io/manual/editor-plugins/) and [proving with AI assistants](https://prooffrog.github.io/researchers/gen-ai/)

## License

ProofFrog is released under the [MIT License](https://github.com/ProofFrog/ProofFrog/blob/main/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](https://uwspace.uwaterloo.ca/bitstream/handle/10012/20441/Evans_Ross.pdf) and [eprint 2025/418](https://eprint.iacr.org/2025/418).

ProofFrog's syntax and approach to modelling is heavily inspired by Mike Rosulek's excellent book [*The Joy of Cryptography*](https://joyofcryptography.com/).

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

<img src="https://github.com/ProofFrog/ProofFrog/blob/main/media/NSERC.jpg?raw=true" alt="NSERC logo" width="750"/>

Includes icons from the [vscode-codicons](https://github.com/microsoft/vscode-codicons) project.

