1.jasmin-lang / jasmin
Language for high-assurance and high-speed cryptography
+28 stars
from 361 · score 3.37
Trending repositories
Ranked by Attention Score: stars gained over the last 90 complete days
37 repositories by Attention Score · Aug 6, 2026 – Nov 3, 2026 (UTC)
2.MetaRocq / metarocq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
- coq
- metaprogramming
- coq-formalization
- rocq
+23 stars
from 545 · score 3.18
3.jwiegley / category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
- category-theory
- coq
- monad
- profunctor
- comonads
- monoid
- +7 more
+17 stars
from 802 · score 2.89
4.mit-plv / fiat-crypto
Cryptographic Primitive Code Generation by Fiat
+16 stars
from 835 · score 2.83
5.math-comp / math-comp
Mathematical Components
- coq
- ssreflect
- mathcomp
- coq-formalization
- rocq
- rocq-library
- +2 more
+16 stars
from 693 · score 2.83
6.HoTT / Coq-HoTT
A Coq library for Homotopy Type Theory
- type-theory
- homotopy-type-theory
- univalent-foundations
+12 stars
from 1,395 · score 2.56
7.CertiRocq / certirocq
A Verified Compiler for Gallina, Written in Gallina
- coq
- gallina
- compiler
- formal-verification
- rocq-prover
+12 stars
from 171 · score 2.56
8.rocq-prover / vsrocq
Visual Studio Code extension for Rocq
- coq
- vscode
- vscode-extension
- editor
- vscodium
- rocq
- +1 more
+11 stars
from 453 · score 2.48
9.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
+10 stars
from 1,012 · score 2.40
10.QuickChick / QuickChick
Randomized Property-Based Testing Plugin for Coq
+7 stars
from 290 · score 2.08
11.DeepSpec / InteractionTrees
A Library for Representing Recursive and Impure Programs in Coq
+7 stars
from 254 · score 2.08
12.rocq-community / fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
- coq
- ssreflect
- mathcomp
- four-color-theorem
- coq-ci
+7 stars
from 246 · score 2.08
13.uds-psl / coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
+5 stars
from 140 · score 1.79
14.uds-psl / MPCTT
Modeling and Proving in Computational Type Theory
+5 stars
from 124 · score 1.79
+5 stars
from 123 · score 1.79
+5 stars
from 118 · score 1.79
17.math-comp / analysis
Mathematical Components compliant Analysis Library
- rocq
- analysis
- coq
- mathcomp
- ssreflect
+3 stars
from 244 · score 1.39
18.rocq-prover / equations
A function definition package for Rocq
- coq
- programming-language
- dependent-types
- rocq
+3 stars
from 236 · score 1.39
19.uwplse / verdi
A framework for formally verifying distributed systems implementations in Coq
- verdi
- coq
- coq-library
- proof
- distributed-systems
+2 stars
from 625 · score 1.10
20.rocq-community / corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
- coq-library
- real-number
- coq
- coq-ci
- coq-platform
+2 stars
from 115 · score 1.10
21.SSProve / ssprove
A foundational framework for modular cryptographic proofs in Coq
- cryptography
- coq-library
- coq-formalization
- state-separating-proofs
- formal-verification
- modular-cryptographic-proofs
+2 stars
from 89 · score 1.10
22.affeldt-aist / monae
Monadic effects and equational reasoning in Rocq
- monads
- monad-transformers
- probabilistic-programming
- nondeterminism
- mathcomp
- ssreflect
- +2 more
+2 stars
from 76 · score 1.10
23.adampetcher / fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography.
+2 stars
from 56 · score 1.10
24.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.
+2 stars
from 51 · score 1.10
25.rocq-community / graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
- coq
- graph-theory
- mathcomp
- docker-coq-action
- mathcomp-ci
+2 stars
from 44 · score 1.10
26.VeriNum / vcfloat
VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
+2 stars
from 32 · score 1.10
27.math-comp / mczify
Micromega tactics for Mathematical Components
- coq
- ssreflect
- mathcomp
- proof-automation
- rocq
- rocq-prover
+2 stars
from 29 · score 1.10
+2 stars
from 26 · score 1.10
29.CertiGraph / CertiGraph
A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
- coq
- vst
- compcert
- graph-algorithms
+2 stars
from 19 · score 1.10
30.GeoCoq / GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
+1 stars
from 209 · score 0.69
31.rocq-community / math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
- coq-library
- typeclasses
- mathematics
- coq
- coq-ci
- coq-platform
+1 stars
from 168 · score 0.69
32.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
33.AU-COBRA / ConCert
A framework for smart contract verification in Coq
- blockchain
- coq
- smart-contracts
- verification
+1 stars
from 128 · score 0.69
+1 stars
from 95 · score 0.69
+1 stars
from 57 · score 0.69
36.math-comp / finmap
Finite sets, finite maps, multisets and generic sets
- coq
- ssreflect
- mathcomp
- finite-sets
+1 stars
from 50 · score 0.69
37.math-comp / algebra-tacticsArchived
The repository host gives no description.
+1 stars
from 38 · score 0.69