ProofFrog: Checker for game-hopping proofs in provable security
===============================================================

ProofFrog checks that the game transitions in a provable-security proof are valid, giving paper authors and reviewers a mechanical check on the skeleton of a reduction. It ships an MCP server so AI assistants can drive it.

Maintainer: Ross Evans, Douglas Stebila (University of Waterloo)
Website: https://github.com/ProofFrog/ProofFrog
Category: Proof systems and computational proofs
Targets: Game-based security proofs (papers)
Approach: Custom language (FrogLang) and checker for game transitions; MCP server for AI assistants
Access: Open source
Status: Research (2025)
Strengths: Low barrier for cryptographers. | AI-assistant integration. | Catches structural proof errors early.
Limits: Not a full computational prover. | Research project. | Limited primitive library.
Firms using it: none listed
Sources: https://github.com/ProofFrog/ProofFrog

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