Top 3 Rocq Prover Compiler 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
-
-
Rocq Prover Compiler discussion
Rocq Prover Compiler related posts
Index
What are some of the best open-source Compiler projects in Rocq Prover? This list will help you:
| # | Project | Stars |
|---|---|---|
| 1 | CompCert | 2,207 |
| 2 | jasmin | 362 |
| 3 | certirocq | 173 |
Sponsored