rocq ☆
« Back to VersTracker
Description:
Proof assistant for higher-order logic
Type: Formula  |  Tracked Since: Dec 28, 2025
Links: Homepage  |  formulae.brew.sh
Category: Developer tools
Tags: proof-assistant formal-verification theorem-prover logic mathematics
Install: brew install rocq
About:
Rocq is a proof assistant designed for formalizing mathematical theorems and verifying software correctness. It provides a rich expressive language based on dependent type theory, allowing users to write precise specifications and machine-checked proofs. Its main value proposition is enabling the development of highly reliable software and rigorous mathematical formalizations.
Key Features:
  • Dependent type theory core
  • Extensive standard library
  • Plugin architecture for extensions
  • Tactics for interactive proof construction
Use Cases:
  • Formalizing mathematical proofs
  • Verifying correctness of critical software
  • Research in programming languages and logic
Alternatives:
  • Lean – Lean focuses on automation and performance, while Rocq offers a mature ecosystem and extensive libraries.
  • Isabelle – Isabelle uses a meta-logic (LCF-style) and offers Isar, a readable proof language, whereas Rocq is based on dependent type theory.
Version History
Detected Version Rev Change Commit
Mar 21, 2026 6:11pm 1 REVISION_ONLY 1a449de4
Oct 4, 2025 11:10pm 0 VERSION_BUMP bcefff82
Sep 11, 2025 5:24am 1 VERSION_BUMP d0c6cbcd
« Back to VersTracker  |  Browse Packages  |  About