Trending Coq Projects

Top 29 Trending Coq Projects

1. Coq-BB5

   1 303 37.0%

   

2. coq-of-rust

   2 906 5.5%

   Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

   

3. koika

   3 153 3.9%

   A core language for rule-based hardware design 🦑

   

4. fourcolor

   4 207 2.9%

   Formal proof of the Four Color Theorem [maintainer=@ybertot]

   

5. math-comp

   5 626 2.9%

   Mathematical Components

   

6. riscv-coq

   6 114 2.6%

   RISC-V Specification in Coq

   

7. analysis

   7 219 1.8%

   Mathematical Components compliant Analysis Library (by math-comp)

   

8. jasmin

   8 292 1.7%

   Language for high-assurance and high-speed cryptography (by jasmin-lang)

   

9. coq-library-undecidability

   9 117 1.7%

   A library of mechanised undecidability proofs in the Coq proof assistant.

   

10. CompCert

    10 1,984 1.6%

    The CompCert formally-verified C compiler

    

11. coq-serapi

    11 130 1.5%

    Coq Protocol Playground with Se(xp)rialization of Internal Structures.

    

12. fiat-crypto

    12 759 1.5%

    Cryptographic Primitive Code Generation by Fiat

    

13. proofs

    13 299 1.3%

    My personal repository of formally verified mathematics.

    

14. kami

    14 153 1.3%

    A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)

    

15. Coq-Equations

    15 230 1.3%

    A function definition package for Coq

    

16. Coq-HoTT

    16 1,312 1.0%

    A Coq library for Homotopy Type Theory

    

17. stalin-sort

    17 1,589 0.9%

    Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

    

18. UniMath

    18 983 0.9%

    This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

    

19. corn

    19 115 0.9%

    Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

    

20. ConCert

    20 119 0.8%

    A framework for smart contract verification in Coq

    

21. verdi

    21 606 0.8%

    A framework for formally verifying distributed systems implementations in Coq

    

22. fiat

    22 152 0.7%

    Mostly Automated Synthesis of Correct-by-Construction Programs

    

23. InteractionTrees

    23 218 0.5%

    A Library for Representing Recursive and Impure Programs in Coq

    

24. toychain

    24 111 0.0%

    A minimalistic blockchain consensus implemented and verified in Coq

    

25. verdi-raft

    25 187 0.0%

    An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

    

26. advent-of-coq-2018

    26 140 0.0%

    Advent of Code 2018, in Coq! (https://adventofcode.com/2018)

    

27. CoqGym

    27 397 0.0%

    A Learning Environment for Theorem Proving with the Coq proof assistant

    

28. magmide

    28 821 0.0%

    A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    

29. tree-calculus

    29 165 0.0%

    Proofs in Coq for the book Reflective Programs in Tree Calculus

    

Index