1.theorem-labs / oss-verify-proofs
Theorem statements about OSS-Fuzz fuzz targets as compiled RISC-V binaries, and machine-checked Rocq proofs of them
- formal-verification
- fuzzing
- oss-fuzz
- proofs
- riscv
- rocq
+22 stars
from 172 · score 3.14
Trending repositories
Ranked by Attention Score: stars gained over the last 7 complete days
23 repositories by Attention Score · Oct 28, 2026 – Nov 3, 2026 (UTC)
2.MetaRocq / metarocq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
- coq
- metaprogramming
- coq-formalization
- rocq
+5 stars
from 563 · score 1.79
3.math-comp / math-comp
Mathematical Components
- coq
- ssreflect
- mathcomp
- coq-formalization
- rocq
- rocq-library
- +2 more
+4 stars
from 705 · score 1.61
4.mit-plv / fiat-crypto
Cryptographic Primitive Code Generation by Fiat
+3 stars
from 848 · score 1.39
5.jasmin-lang / jasmin
Language for high-assurance and high-speed cryptography
+2 stars
from 387 · score 1.10
6.QuickChick / QuickChick
Randomized Property-Based Testing Plugin for Coq
+2 stars
from 295 · score 1.10
7.UniMath / UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
- coq
- mathematics
- unimath
- coq-library
- foundations
- rocq
- +1 more
+1 stars
from 1,021 · score 0.69
8.rocq-community / fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
- coq
- ssreflect
- mathcomp
- four-color-theorem
- coq-ci
+1 stars
from 252 · score 0.69
9.math-comp / analysis
Mathematical Components compliant Analysis Library
- rocq
- analysis
- coq
- mathcomp
- ssreflect
+1 stars
from 246 · score 0.69
10.rocq-prover / equations
A function definition package for Rocq
- coq
- programming-language
- dependent-types
- rocq
+1 stars
from 238 · score 0.69
11.uds-psl / coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
+1 stars
from 144 · score 0.69
12.rocq-community / coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
- coq
- library
- programming
- coq-platform
- coq-ci
+1 stars
from 135 · score 0.69
13.uds-psl / MPCTT
Modeling and Proving in Computational Type Theory
+1 stars
from 128 · score 0.69
+1 stars
from 127 · score 0.69
+1 stars
from 122 · score 0.69
16.rocq-community / corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
- coq-library
- real-number
- coq
- coq-ci
- coq-platform
+1 stars
from 116 · score 0.69
17.SSProve / ssprove
A foundational framework for modular cryptographic proofs in Coq
- cryptography
- coq-library
- coq-formalization
- state-separating-proofs
- formal-verification
- modular-cryptographic-proofs
+1 stars
from 90 · score 0.69
18.affeldt-aist / monae
Monadic effects and equational reasoning in Rocq
- monads
- monad-transformers
- probabilistic-programming
- nondeterminism
- mathcomp
- ssreflect
- +2 more
+1 stars
from 77 · score 0.69
+1 stars
from 57 · score 0.69
20.adampetcher / fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography.
+1 stars
from 57 · score 0.69
21.impermeable / rocq-waterproof
The Waterproof plugin for the Rocq proof assistant allows you to write Rocq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
+1 stars
from 52 · score 0.69
22.math-comp / finmap
Finite sets, finite maps, multisets and generic sets
- coq
- ssreflect
- mathcomp
- finite-sets
+1 stars
from 50 · score 0.69
23.rocq-community / graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
- coq
- graph-theory
- mathcomp
- docker-coq-action
- mathcomp-ci
+1 stars
from 45 · score 0.69