Language · Rocq Prover

Rocq Prover

Tracked open-source repos with Rocq Prover as the primary language, sorted by stars.

13 repos

#1
CompCert ↗@AbsIntRocq Prover
The CompCert formally-verified C compiler
★ 2,219+5Star change over the last 7 days
#2
stalin-sort ↗@gustavo-depaulaRocq Prover
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
★ 1,706+0Star change over the last 7 days
#3
Coq-HoTT ↗@HoTTRocq Prover
A Coq library for Homotopy Type Theory
★ 1,405+1Star change over the last 7 days
#4
rocq-of-rust ↗@formal-landRocq Prover
Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
★ 1,161+3Star change over the last 7 days
#5
UniMath ↗@UniMathRocq Prover
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
★ 1,017+0Star change over the last 7 days
#6
fiat-crypto ↗@mit-plvRocq Prover
Cryptographic Primitive Code Generation by Fiat
★ 839+0Star change over the last 7 days
#7
magmide ↗@magmideRocq Prover
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
★ 835+0Star change over the last 7 days
#8
category-theory ↗@jwiegleyRocq Prover
An axiom-free formalization of category theory in Coq for personal study and practical work
★ 806+1Star change over the last 7 days
#9
frap ↗@achlipalaRocq Prover
Formal Reasoning About Programs
★ 729+2Star change over the last 7 days
#10
math-comp ↗@math-compRocq Prover
Mathematical Components
★ 695+0Star change over the last 7 days
#11
verdi ↗@uwplseRocq Prover
A framework for formally verifying distributed systems implementations in Coq
★ 625+0Star change over the last 7 days
#12
metarocq ↗@MetaRocqRocq Prover
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
★ 549+1Star change over the last 7 days
#13
VST ↗@PrincetonUniversityRocq Prover
Verified Software Toolchain
★ 507+0Star change over the last 7 days

← Back to languages