For Researchers

This area of the site is for people who want to understand ProofFrog’s design, primarily from a scientific perspective.

If you are learning provable security or are new to ProofFrog, we recommend starting with the manual.

  • Scientific Background — ProofFrog’s design choices and positioning relative to other tools.
  • Engine Internals — high-level architecture, core modules, the transformation pipeline by category, diagnostics and near-miss matching, the engine-introspection CLI commands, and the LSP and MCP servers.
  • Soundness — what ProofFrog claims, what is in the trust base, what is not claimed, mitigations a careful user can apply, and the comparison framing relative to EasyCrypt and CryptoVerif.
  • GenAI & Proving — using LLM-based coding assistants to draft and iterate on proofs (a research-and-experimentation tool, not a recommended student workflow).
  • External Uses — curated case studies of external projects using ProofFrog.
  • Publications — papers, theses, talks, and how to cite ProofFrog.

Lineage

ProofFrog was built by Ross Evans, Matthew McKague, and Douglas Stebila at the University of Waterloo, building on the earlier pygamehop tool by Douglas Stebila and Matthew McKague at Queensland University of Technology. Full bibliographic details are on the Publications page. Development is supported by the Natural Sciences and Engineering Research Council of Canada (NSERC) Discovery grant RGPIN-2022-03187.

This site uses Just the Docs, a documentation theme for Jekyll.