Top 23 Rocq Prover coq Projects
-
Project mention: Lies, Damned Lies and Proofs: Formal Methods Are Not Slopless | news.ycombinator.com | 2026-01-17
> Third, you need to decide how far “down the stack” you want to go. That is to say, the software you want to verify operates over some kind of more complex system, for instance, maybe it’s C code which gets compiled down to X86 and runs on a particular chip, or maybe it’s a controller for a nuclear reactor and part of the system is the actual physical dynamics of the reactor. Do you really want your proof to involve specifying the semantics of the C compiler and the chip, or the way that the temperature and other variables fluctuate in the reactor?
I can appreciate what he's getting at, but my utopian vision for the future is that we won't need to reinvent the wheel like this each time we want verified software! E.g. for high-consequence systems, the hard part of compiler correctness is already handled by the efforts of (Compcert)[https://github.com/AbsInt/CompCert], and SystemVerilog assertions for the design guarantees of processors is becoming more commonplace.
-
AppSignal
AppSignal knows why the f*#k it crashed. Stop vibe-debugging. Every exception, every backtrace, grouped so you see patterns, not noise.
-
UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
But how is Claude so good at maths though? I'm struggling to understand how it is raising issues such as this one https://github.com/jwiegley/category-theory/issues/598 in a mathematical category theory library written in Rocq prover, and creating and merging PRs there too. Can't see how this could be based on glorified pattern matching, which is how I always viewed LLMs.
-
-
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
-
-
-
-
-
-
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
-
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
-
-
-
Project mention: Extracting verified C++ from the Rocq theorem prover at Bloomberg | news.ycombinator.com | 2026-01-23
This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project:
https://skylabsai.github.io/BRiCk/index.html
https://github.com/SkyLabsAI/BRiCk
-
-
-
-
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Rocq Prover coq discussion
Rocq Prover coq related posts
Index
What are some of the best open-source coq projects in Rocq Prover? This list will help you:
| # | Project | Stars |
|---|---|---|
| 1 | CompCert | 2,237 |
| 2 | UniMath | 1,017 |
| 3 | magmide | 836 |
| 4 | category-theory | 813 |
| 5 | math-comp | 699 |
| 6 | verdi | 627 |
| 7 | jasmin | 375 |
| 8 | proofs | 312 |
| 9 | fourcolor | 251 |
| 10 | analysis | 246 |
| 11 | equations | 236 |
| 12 | koika | 187 |
| 13 | certirocq | 179 |
| 14 | kami | 170 |
| 15 | coq-library-undecidability | 144 |
| 16 | ConCert | 129 |
| 17 | corn | 116 |
| 18 | BRiCk | 105 |
| 19 | vericert | 100 |
| 20 | hs-to-rocq | 96 |
| 21 | rupicola | 71 |
| 22 | aneris | 37 |
| 23 | rocq-simple-io | 34 |
Sponsored