Rocq Stats

Lemma statistics and documentation for Rocq/Coq formalizations

Projects

DSDP Formalization

Dual protocols for private multi-party matrix multiplication - Information-theoretic security proofs in Rocq/Coq

322 lemmas
47 main
28 theorems
22 files
10,609 lines
bec7c86 commit

About Rocq Stats

A documentation generator for Rocq/Coq formalizations. Extracts lemma information, analyzes dependencies, and generates browsable documentation.

Features

  • Automatic lemma extraction from .v files
  • Main/Helper classification
  • Dependency analysis between lemmas
  • Source code links to specific commits

Add Your Project

Want to add your Rocq/Coq project? Submit a Pull Request with a YAML config file.

  1. Fork the repository
  2. Add a YAML file in projects/ with your repo URL, branch, and commit hash
  3. Submit a PR — it will be auto-built and merged

View full instructions →