Top 21 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.
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
-
-
> I think we want a Special Purpose language focused on emitting guaranteed constant time machine code for an algorithm.
https://github.com/jasmin-lang/jasmin
-
-
-
-
-
-
-
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
-
-
-
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,184 |
| 2 | UniMath | 1,009 |
| 3 | math-comp | 683 |
| 4 | verdi | 624 |
| 5 | jasmin | 358 |
| 6 | proofs | 310 |
| 7 | analysis | 244 |
| 8 | fourcolor | 242 |
| 9 | equations | 238 |
| 10 | koika | 173 |
| 11 | certirocq | 170 |
| 12 | kami | 167 |
| 13 | coq-library-undecidability | 137 |
| 14 | ConCert | 126 |
| 15 | corn | 116 |
| 16 | vericert | 98 |
| 17 | hs-to-rocq | 95 |
| 18 | BRiCk | 92 |
| 19 | rupicola | 67 |
| 20 | aneris | 37 |
| 21 | rocq-simple-io | 35 |
Sponsored