awesome-coq
Coq toolkit
A curated collection of tools and libraries for formal verification and development in the Coq proof assistant
A curated list of awesome Coq frameworks, libraries and software.
235 stars
22 watching
16 forks
last commit: 2 months ago
Linked from 1 awesome list
awesome-coq | |||
| AbsInt/CompCert | 1,901 | 2 months ago | The CompCert formally-verified C compiler |
| HoTT/Coq-HoTT | 1,262 | 2 months ago | A Coq library for Homotopy Type Theory |
| UniMath/UniMath | 964 | 2 months ago | This coq library aims to formalize a substantial body of mathematics using the univalent point of view |
| magmide/magmide | 810 | 11 months ago | A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers |
| jwiegley/category-theory | 759 | 3 months ago | An axiom-free formalization of category theory in Coq for personal study and practical work |
| uwplse/verdi | 595 | 9 months ago | A framework for formally verifying distributed systems implementations in Coq |
| math-comp/math-comp | 593 | 2 months ago | Mathematical Components |
| coq-community/coq-tricks | 507 | 6 months ago | Tricks you wish the Coq manual told you [maintainer=@tchajed] |
| PrincetonUniversity/VST | 444 | 2 months ago | Verified Software Toolchain |
| formal-land/coq-of-rust | 437 | 2 months ago | Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦 |
| MetaCoq/metacoq | 396 | 3 months ago | Metaprogramming, verified meta-theory and implementation of Coq in Coq |
| princeton-vl/CoqGym | 388 | over 1 year ago | A Learning Environment for Theorem Proving with the Coq proof assistant |
| stepchowfun/proofs | 292 | 2 months ago | My personal repository of formally verified mathematics |
| antalsz/hs-to-coq | 279 | over 4 years ago | Convert Haskell source code to Coq source code |
| jasmin-lang/jasmin | 275 | 2 months ago | Language for high-assurance and high-speed cryptography |
| QuickChick/QuickChick | 259 | 2 months ago | Randomized Property-Based Testing Plugin for Coq |
| UniMath/Foundations | 241 | over 10 years ago | Voevodsky's original development of the univalent foundations of mathematics in Coq |
| mit-pdos/fscq | 237 | over 2 years ago | FSCQ is a certified file system written and proven in Coq |
| mattam82/Coq-Equations | 223 | 3 months ago | A function definition package for Coq |
| math-comp/analysis | 210 | 2 months ago | Mathematical Components compliant Analysis Library |
| DeepSpec/InteractionTrees | 206 | 4 months ago | A Library for Representing Recursive and Impure Programs in Coq |
| sifive/Kami | 198 | over 4 years ago | Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT |
| jscert/jscert | 196 | about 1 year ago | A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter |
| uwplse/verdi-raft | 186 | about 1 year ago | An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework |
| GeoCoq/GeoCoq | 186 | 9 months ago | A formalization of geometry in Coq based on Tarski's axiom system |
| clarus/coq-chick-blog | 178 | about 5 years ago | 🐣 A blog engine written and proven in Coq |
| coq-community/fourcolor | 174 | 3 months ago | Formal proof of the Four Color Theorem [maintainer=@ybertot] |
| jwiegley/coq-haskell | 168 | over 1 year ago | A library for formalizing Haskell types and functions in Coq |
| mit-pdos/perennial | 165 | 2 months ago | Verifying concurrent crash-safe systems |
| coq-community/math-classes | 162 | 4 months ago | A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia] |
| ilyasergey/pnp | 160 | over 3 years ago | Lecture notes for a short course on proving/programming in Coq via SSReflect |
| mit-plv/koika | 143 | 4 months ago | A core language for rule-based hardware design 🦑 |
| mit-plv/kami | 143 | 5 months ago | A Platform for High-Level Parametric Hardware Specification and its Modular Verification |
| barry-jay-personal/tree-calculus | 143 | over 3 years ago | Proofs in Coq for the book Reflective Programs in Tree Calculus |
| discus-lang/iron | 142 | over 4 years ago | Coq formalizations of functional languages |
| Lysxia/advent-of-coq-2018 | 140 | about 6 years ago | Advent of Code 2018, in Coq! ( ) |
| CertiCoq/certicoq | 137 | 6 months ago | A Verified Compiler for Gallina, Written in Gallina |
| coq-community/coq-ext-lib | 129 | 2 months ago | A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai] |
| rocq-archive/coq-serapi | 128 | 3 months ago | Coq Protocol Playground with Se(xp)rialization of Internal Structures |
| project-oak/silveroak | 123 | almost 3 years ago | Formal specification and verification of hardware, especially for security and privacy |
| verse-lab/ceramist | 121 | almost 5 years ago | Verified hash-based AMQ structures in Coq |
| coq-community/coq-art | 114 | 7 months ago | Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran] |
| AU-COBRA/ConCert | 114 | 3 months ago | A framework for smart contract verification in Coq |
| verse-lab/toychain | 111 | almost 5 years ago | A minimalistic blockchain consensus implemented and verified in Coq |
| uds-psl/coq-library-undecidability | 111 | 5 months ago | A library of mechanised undecidability proofs in the Coq proof assistant |
| coq-community/corn | 111 | 3 months ago | Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia] |
| mit-plv/riscv-coq | 110 | 7 months ago | RISC-V Specification in Coq |
| Ptival/PeaCoq | 106 | over 3 years ago | PeaCoq is a pretty Coq, isn't it? |
| WasmCert/WasmCert-Coq | 100 | 4 months ago | A mechanisation of Wasm in Coq |
| sec-bit/tokenlibs-with-proofs | 97 | over 5 years ago | Correctness proofs of Ethereum token contracts |
| DistributedComponents/disel | 95 | 7 months ago | Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq |
| amintimany/Categories | 94 | 4 months ago | A formalization of category theory in the Coq proof assistant |
| clarus/falso | 93 | over 5 years ago | A proof of false in Coq |
| ymherklotz/vericert | 88 | 8 months ago | A formally verified high-level synthesis tool based on CompCert and written in Coq |
| coq-community/coq-dpdgraph | 87 | 3 months ago | Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot] |
| coq-concurrency/pluto | 86 | over 8 years ago | A web server written in Coq |
| inQWIRE/SQIR | 80 | 6 months ago | A Small Quantum Intermediate Representation |
| plclub/hs-to-coq | 79 | 6 months ago | Convert Haskell source code to Coq source code |
| pi8027/lambda-calculus | 78 | over 4 years ago | A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2 |
| ml4tp/gamepad | 72 | over 2 years ago | A Learning Environment for Theorem Proving |
| bluerock-io/BRiCk | 72 | 2 months ago | Formalization of C++ for verification purposes |
| imdea-software/htt | 70 | 5 months ago | Hoare Type Theory |
| affeldt-aist/monae | 70 | 2 months ago | Monadic effects and equational reasonig in Coq |
| coq-community/hydra-battles | 69 | about 1 year ago | Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran] |
| coq-community/coqeal | 67 | 2 months ago | The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01] |
| rocq-archive/coq-in-coq | 66 | 7 months ago | A formalisation of the Calculus of Constructions |
| xavierleroy/cdf-mech-sem | 64 | 11 months ago | Coq development for the course "Mechanized semantics", Collège de France, 2019-2020 |
| coq-io/io | 64 | over 2 years ago | A library for effects in Coq |
| affeldt-aist/infotheo | 64 | 3 months ago | A Coq formalization of information theory and linear error-correcting codes |
| INRIA/velus | 63 | 3 months ago | A Lustre compiler in Coq |
| choukh/Set-Theory | 59 | over 3 years ago | A formalization of the textbook Elements of Set Theory |
| sigurdschneider/lvc | 57 | over 6 years ago | LVC verified compiler |
| mit-plv/bedrock | 57 | over 7 years ago | Coq library for verified low-level programming |
| SSProve/ssprove | 56 | 3 months ago | A foundational framework for modular cryptographic proofs in Coq |
| philzook58/nand2coq | 54 | about 3 years ago | Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools) |
| geohot/coq-hardy | 53 | almost 6 years ago | Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq |
| lthms/FreeSpec | 52 | about 1 year ago | A framework for implementing and certifying impure computations in Coq |
| coq-community/autosubst | 52 | 5 months ago | Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan] |
| mit-plv/rupicola | 51 | 2 months ago | Gallina to Bedrock2 compilation toolkit |
| MichaelBurge/pornview | 51 | over 7 years ago | Porn browser formally-verified in Coq |
| jtassarotti/coq-proba | 50 | over 1 year ago | A Probability Theory Library for the Coq Theorem Prover |
| anton-trunov/coq-lecture-notes | 50 | over 4 years ago | Coq Lecture Notes (WIP) |
| uwplse/pumpkin-pi | 49 | 5 months ago | An extension to PUMPKIN PATCH with support for proof repair across type equivalences |
| tchajed/iris-simp-lang | 49 | 9 months ago | We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic |
| cmeiklejohn/distributed-data-structures | 49 | over 11 years ago | Distributed Data Structures in Coq |
| damien-pous/relation-algebra | 48 | 3 months ago | Relation algebra library for Coq |
| math-comp/finmap | 47 | 9 months ago | Finite sets, finite maps, multisets and generic sets |
| coq-community/topology | 47 | 4 months ago | General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran] |
| arthuraa/poleiro | 47 | almost 3 years ago | A blog about Coq |
| foreverbell/verified | 46 | almost 7 years ago | Coq formalizations and proofs of (data) structures and algorithms |
| coq-community/semantics | 46 | about 3 years ago | A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik] |
| coq-community/paramcoq | 45 | 5 months ago | Coq plugin for parametricity [maintainer=@proux01] |
| coq-community/fav-ssr | 45 | 3 months ago | Functional Algorithms Verified in SSReflect [maintainer=@clayrat] |
| vrahli/NuprlInCoq | 44 | 3 months ago | Implementation of Nuprl's type theory in Coq |
| pirapira/evmverif | 44 | over 8 years ago | An EVM code verification framework in Coq |
| dschepler/coq-sequent-calculus | 44 | almost 9 years ago | Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic |
| wouter-swierstra/xmonad | 43 | over 12 years ago | xmonad in Coq |
| tchajed/ltac2-tutorial | 43 | over 2 years ago | Ltac2 tutorial |
| tchajed/coq-record-update | 43 | 6 months ago | Library to create Coq record update functions |
| snu-sf/paco | 43 | 4 months ago | A Coq library for parametric coinduction |
| coq-community/dedekind-reals | 43 | 7 months ago | A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer] |
| choukh/Baby-Set-Theory | 43 | about 3 years ago | Coq集合论中文教程 |
| mit-plv/coqutil | 42 | 2 months ago | Coq library for tactics, basic definitions, sets, maps |
| coq-community/parseque | 42 | about 1 year ago | Total Parser Combinators in Coq [maintainer=@womeier] |
| coq-community/reglang | 41 | 7 months ago | Regular Language Representations in Coq [maintainers=@chdoc,@palmskog] |
| xavierleroy/cdf-program-logics | 40 | almost 4 years ago | Companion Coq development for Xavier Leroy's 2021 lectures on program logics |
| meithecatte/busycoq | 39 | 7 months ago | Busy Beaver deciders backed by Coq proof |
| CertiCoq/VeriFFI | 39 | 7 months ago | VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project |
| vlopezj/coq-course | 38 | over 7 years ago | Coq course at Chalmers CSE |
| charguer/tlc | 38 | 3 months ago | Library for Classical Coq |
| thery/coqprime | 37 | 4 months ago | Prime numbers for Coq |
| math-comp/Coq-Combi | 37 | 3 months ago | Algebraic Combinatorics in Coq |
| takanuva/cps | 36 | 3 months ago | A formalization of continuation-passing style calculi in Coq [WIP] |
| gangtan/CPUmodels | 36 | over 7 years ago | GoNative project: formal machines models in Coq |
| langston-barrett/coq-big-o | 35 | almost 8 years ago | A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces |
| fblanqui/color | 35 | 4 months ago | Coq library on rewriting theory and termination |
| coq-community/graph-theory | 35 | 3 months ago | Graph Theory [maintainers=@chdoc,@damien-pous] |
| snu-sf/promising-coq | 33 | 4 months ago | The Coq development of A Promising Semantics for Relaxed-Memory Concurrency |
| pedrotst/coquedille | 33 | over 4 years ago | A Coq to Cedille compiler written in Coq |
| math-comp/algebra-tactics | 33 | 3 months ago | Ring, field, lra, nra, and psatz tactics for Mathematical Components |
| marshall-lee/software_foundations | 33 | 8 months ago | My solutions to Software Foundations course in Coq proof assistant |
| Lysxia/system-F | 33 | almost 6 years ago | Formalization of the polymorphic lambda calculus and its parametricity theorem |
| logsem/aneris | 33 | 2 months ago | Program logic for developing and verifying distributed systems |
| impermeable/coq-waterproof | 33 | 3 months ago | The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements |
| EasyCrypt/certicrypt | 33 | almost 9 years ago | CertiCrypt Coq Framework |
| inQWIRE/QuantumLib | 33 | 3 months ago | Coq library for reasoning about quantum programs |
| coq-community/chapar | 32 | about 1 year ago | A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog] |
| bmsherman/topology | 32 | about 6 years ago | Formal topology (and some probability) in Coq |
| Lysxia/coq-simple-io | 31 | 2 months ago | IO for Gallina |
| codyroux/broad-coq-tutorial | 31 | over 3 years ago | Some unstructured notes concerning the Broad tutorial to take place in March 2020 |
| vafeiadis/hahn | 30 | 8 months ago | Hahn: A Coq library |
| pa-ba/calc-comp | 30 | about 1 year ago | Coq proofs for the paper "Calculating Correct Compilers" |
| formal-land/coq-of-python | 30 | 5 months ago | Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python |
| coq-community/gaia | 30 | 6 months ago | Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery] |
| coq-community/dblib | 30 | over 3 years ago | Coq library for working with de Bruijn indices [maintainer=@KevOrr] |
| coq-community/coq-program-verification-template | 29 | 7 months ago | Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog] |
| arthuraa/extructures | 29 | 2 months ago | Finite sets and maps for Coq with extensional equality |
| vrahli/Velisarios | 28 | over 5 years ago | A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems |
| tezos/tezoscoq | 28 | over 7 years ago | working with coq and tezos |
| math-comp/Abel | 28 | 3 months ago | A proof of Abel-Ruffini theorem |
| llee454/functional-algebra | 28 | almost 6 years ago | This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs |
| coq-community/goedel | 28 | over 2 years ago | Archived since the contents have been moved to the Hydras & Co. repository |
| acorrenson/SATurne | 28 | about 3 years ago | Tiny verified SAT-solver |
| math-comp/odd-order | 27 | 4 months ago | The formal proof of the Odd Order Theorem |
| reynir/Brainfuck | 26 | almost 3 years ago | Brainfuck formalized in Coq |
| novifinancial/LibraChain | 26 | over 4 years ago | A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover |
| imdea-software/fcsl-pcm | 26 | 4 months ago | Partial Commutative Monoids |
| dboulytchev/miniKanren-coq | 26 | over 4 years ago | A certified semantics for relational programming workout |
| coq-ext-lib/coq-compile | 26 | almost 12 years ago | A compiler for Coq |
| coq-community/lemma-overloading | 26 | 3 months ago | Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov] |
| affeldt-aist/coq-robot | 26 | 9 months ago | Mathematics of Rigid Body Transformationss using Coq and MathComp |
| rafaelcgs10/W-in-Coq | 25 | over 4 years ago | This is a Coq formalization of Damas-Milner type system and its algorithm W |
| coq-community/alea | 25 | over 3 years ago | Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka] |
| AU-COBRA/PoS-NSB | 25 | about 4 years ago | A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq |
| Zilliqa/scilla-coq | 24 | over 4 years ago | State-Transition Systems for Smart Contracts |
| VeriNum/vcfloat | 24 | 7 months ago | VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations |
| thery/hanoi | 24 | over 1 year ago | Hanoi tower in Coq |
| sweirich/graded-haskell | 24 | over 1 year ago | Graded Dependent Type systems |
| math-comp/mczify | 24 | 3 months ago | Micromega tactics for Mathematical Components |
| lastland/ClairvoyanceMonad | 24 | 8 months ago | The Coq formalization of the paper Reasoning about the garden of forking paths |
| formal-land/coq-bonsai | 24 | over 3 years ago | 🌳 Generate a fresh bonsai in your terminal |
| arthuraa/deriving | 24 | 3 months ago | Class instances for Coq inductive types with little boilerplate |
| uwplse/cheerios | 23 | over 1 year ago | Formally verified Coq serialization library with support for extraction to OCaml |
| dunnl/tealeaves | 23 | 5 months ago | A Coq library for abstract syntactical reasoning |
| coq-io/system | 23 | over 5 years ago | Library of Unix effects for Coq |
| coq-community/atbr | 23 | 4 months ago | Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed] |
| thery/T2048 | 22 | over 1 year ago | a version of the 2048 game for Coq |
| sifive/ProcKami | 22 | over 4 years ago | Kami based processor implementations and specifications |
| rocq-archive/zfc | 22 | about 2 years ago | An encoding of Zermelo-Fraenkel Set Theory in Coq |
| pi8027/stablesort | 22 | 5 months ago | Stable sort algorithms and their stability proofs in Coq |
| huynhtrankhanh/CoqCP | 22 | 2 months ago | We combat sloppy arguments in competitive programming and raise the standard of rigor |
| Coq-Polyhedra/Coq-Polyhedra | 22 | 8 months ago | Formalizing convex polyhedra in Coq |
| coq-community/bits | 22 | 7 months ago | A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov] |
| coq-community/bignums | 22 | 2 months ago | Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd] |
| bobatkey/system-f-parametricity-model | 22 | over 9 years ago | A Model of Relationally Parametric System F in Coq |
| Yosuke-Ito-345/Actuary | 21 | 2 months ago | Formalization of the basic actuarial mathematics using Coq |
| xavierleroy/cdf-sem-meca | 21 | 10 months ago | Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020 |
| weakmemory/imm | 21 | 6 months ago | Intermediate Memory Model (IMM) and compilation correctness proofs for it |
| uwplse/StructTact | 21 | about 1 year ago | Coq utility and tactic library |
| mgrabovsky/fm-notes | 21 | about 1 year ago | Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on |
| kai-qu/linear-logic | 21 | about 3 years ago | An encoding of linear logic in Coq with minimal Sokoban and blocks world examples |
| Huxpro/WasmCert | 21 | over 3 years ago | A (in-development) Coq mechanization of WebAssembly specification |
| coq-community/coqoban | 21 | about 2 years ago | Sokoban (in Coq) [maintainer=@erikmd] |
| mmcco/verified-parser-example | 20 | almost 10 years ago | A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend |
| Matafou/LibHyps | 20 | 3 months ago | A Coq library providing tactics to deal with hypothesis |
| jwiegley/coq-lattice | 20 | over 1 year ago | A reflection-based proof tactic for lattices in Coq |
| CoqHott/logrel-coq | 20 | 2 months ago | Logical Relation for MLTT in Coq |
| coq-community/sudoku | 20 | over 2 years ago | A certified Sudoku solver in Coq [maintainers=@siraben,@thery] |
| CertiKOS/coqrel | 20 | 4 months ago | Binary logical relations library for the Coq proof assistant |
| LPCIC/coq-elpi | 141 | 2 months ago | Coq plugin embedding elpi |
| bedrocksystems/BRiCk | 72 | 2 months ago | Formalization of C++ for verification purposes |
| ejgallego/coq-serapi | 128 | 3 months ago | Coq Protocol Playground with Se(xp)rialization of Internal Structures |
| coq-contribs/coq-in-coq | 66 | 7 months ago | A formalisation of the Calculus of Constructions |
| coq-contribs/zfc | 22 | about 2 years ago | An encoding of Zermelo-Fraenkel Set Theory in Coq |
| tchajed/coq-tricks | 507 | 6 months ago | Tricks you wish the Coq manual told you |
| andrejbauer/dedekind-reals | 43 | 7 months ago | A formalization of the Dedekind reals in Coq |
| vellvm/vellvm | 405 | 2 months ago | The Vellvm (Verified LLVM) coq development |
| gallais/parseque | 42 | about 1 year ago | Total Parser Combinators in Coq |
| palmskog/coq-program-verification-template | 29 | 7 months ago | Template project for program verification in Coq |
| Blaisorblade/dot-iris | 30 | 4 months ago | Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization |
| LogicalAtomist/principia | 208 | 2 months ago | The Principia Rewrite |
| certichain/toychain | 111 | almost 5 years ago | A minimalistic blockchain consensus implemented and verified in Coq |
| coq-community/coq-100-theorems | 57 | 11 months ago | Statements of famous theorems proven in Coq [maintainer=@jmadiot] |
| smtcoq/smtcoq | 157 | 5 months ago | Communication between Coq and SAT/SMT solvers |
| smorimoto/coq-to-ocaml-to-js | 24 | over 2 years ago | Proof of concept to generate safe and fast JavaScript |
| certichain/ceramist | 121 | almost 5 years ago | Verified hash-based AMQ structures in Coq |
| math-comp/fourcolor | 174 | 3 months ago | Formal proof of the Four Color Theorem |
| foobar-land/coq-bonsai | 24 | over 3 years ago | 🌳 Generate a fresh bonsai in your terminal |
| bedrocksystems/cpp2v | 72 | 2 months ago | Formalization of C++ for verification purposes |
| hivert/Coq-Combi | 1 | almost 2 years ago | Algebraic Combinatorics in Coq |
| Karmaki/coq-dpdgraph | 87 | 3 months ago | Build dependency graphs between COQ objects |
| CoqEAL/CoqEAL | 67 | 2 months ago | CoqEAL -- The Coq Effective Algebra Library |
| heades/System-F-Coq | 19 | about 10 years ago | System F in coq |
| math-comp/hierarchy-builder | 97 | 2 months ago | High level commands to declare a hierarchy based on packed classes |
| project-oak/oak-hardware | 123 | almost 3 years ago | Formal specification and verification of hardware, especially for security and privacy |
| coq-community/coq100 | 57 | 11 months ago | Statements of famous theorems proven in Coq [maintainer=@jmadiot] |
| ANSSI-FR/FreeSpec | 52 | about 1 year ago | A framework for implementing and certifying impure computations in Coq |
| uds-psl/autosubst | 52 | 5 months ago | Automation for de Bruijn syntax and substitution in Coq |
| uwplse/ornamental-search | 49 | 5 months ago | DEVOID: Ornaments for Proof Reuse in Coq |
| coq-ext-lib/coq-ext-lib | 129 | 2 months ago | A library of Coq definitions, theorems, and tactics |
| siddharthist/coq-big-o | 35 | almost 8 years ago | A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces |
| hazelgrove/hazel | 808 | 2 months ago | Hazel, a live functional programming environment with typed holes |
| Template-Coq/template-coq | 396 | 3 months ago | Reflection library for Coq |
| math-classes/math-classes | 162 | 4 months ago | A library of abstract interfaces for mathematical structures in Coq |
| c-corn/corn | 111 | 3 months ago | Coq Repository at Nijmegen |
| stepchowfun/coq-fun | 292 | 2 months ago | A selection of Coq developments |
| uwdb/Cosette | 668 | about 3 years ago | Cosette is an automated SQL solver powered by Coq and Rosette |
| DDCSF/iron | 142 | over 4 years ago | Coq formalizations of functional languages |
| vladimirias/Foundations | 53 | over 10 years ago | Development of the univalent foundations of mathematics in Coq |
| aspiwack/cosa | 4 | over 10 years ago | Coq-verified Shape Analysis |
| Ptival/HaysTac | 5 | over 6 years ago | A pile of Ltac tactics that might contain the needle you're looking for. Oriented around nameless tactics programming |
| EugeneLoy/coq_jupyter | 94 | 6 months ago | Jupyter Notebook kernel for Coq |
xgrommx/awesome-functional-programming
coq-community/comp-dec-modal
thery/mathcomp-extra
williamdemeo/typefunc
engineeringsoftware/roosterize
runtimeverification/verified-smart-contracts
pirapira/eth-isabelle
lukaszcz/coqhammer
ethereum/tests