ProofFrog

ProofFrog is a tool for checking transitions in cryptographic game-hopping proofs.

This VSCode extension provides language support for ProofFrog's domain-specific language, FrogLang.

About ProofFrog

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.

Features

• Syntax highlighting for .primitive, .scheme, .game, and .proof files
• Parse error diagnostics shown as squiggles on save
• Semantic analysis (type checking) diagnostics on save
• Go-to-definition for import paths (Cmd/Ctrl+click)
• Hover information for imported names
• Completion for scheme and primitive members (type . after an import alias)
• Code lens annotations on .proof files showing pass/fail for each game hop
• Proof hops tree view in the Explorer sidebar when viewing a .proof file

Requirements

• Python 3.11+ with ProofFrog installed:

  pip install prooffrog
  

• The extension connects to a Python LSP server (python -m proof_frog lsp), so ProofFrog must be installed in the Python environment that the extension uses.

Configuration

If you use a virtual environment, set this to the full path:

{
  "prooffrog.pythonPath": "/path/to/venv/bin/python"
}