awesome-coq

A curated list of awesome Coq frameworks, libraries and software.

• Learning and Reference
  • Tutorials and Books
  • Examples and Exercises
• Language and Tooling
  • Compilers and Interpreters
• Networking and Distributed
  • Distributed Systems
• User Interface
  • Applications and End User Tools
• Utilities
  • General Purpose Libraries
• Science and Math
  • Mathematics
  • Formal Methods and Proofs
• Other

Learning and Reference

Tutorials and Books

• rocq-community/rocq-tricks - Tricks you wish the Coq manual told you [maintainer=@tchajed]
• ilyasergey/pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.
• xavierleroy/cdf-mech-sem - Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
• tchajed/iris-simp-lang - We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
• philzook58/nand2coq - Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
• rocq-community/semantics - A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
• anton-trunov/coq-lecture-notes - Coq Lecture Notes (WIP)
• tchajed/ltac2-tutorial - Ltac2 tutorial
• arthuraa/poleiro - A blog about Coq
• choukh/Baby-Set-Theory - Coq集合论中文教程
• xavierleroy/cdf-program-logics - Companion Coq development for Xavier Leroy's 2021 lectures on program logics
• vlopezj/coq-course - Coq course at Chalmers CSE
• codyroux/broad-coq-tutorial - Some unstructured notes concerning the Broad tutorial to take place in March 2020
• rocq-prover/platform-docs - A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
• xavierleroy/cdf-sem-meca - Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
• mgrabovsky/fm-notes - Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on (archived)
• rocq-community/hoare-tut - A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]

Examples and Exercises

• Lysxia/advent-of-coq-2018 - Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
• rocq-community/coq-art - Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
• marshall-lee/software_foundations - My solutions to Software Foundations course in Coq proof assistant.
• rocq-community/rocq-program-verification-template - Template project for program verification in the Rocq Prover, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
• mmcco/verified-parser-example - A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend.

Language and Tooling

Compilers and Interpreters

• AbsInt/CompCert - The CompCert formally-verified C compiler
• jasmin-lang/jasmin - Language for high-assurance and high-speed cryptography
• antalsz/hs-to-coq - Convert Haskell source code to Coq source code (archived)
• mit-plv/koika - A core language for rule-based hardware design 🦑
• CertiRocq/certirocq - A Verified Compiler for Gallina, Written in Gallina
• ymherklotz/vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
• plclub/hs-to-rocq - Convert Haskell source code to Coq source code.
• INRIA/velus - A Lustre compiler in Coq
• mit-plv/rupicola - Gallina to Bedrock2 compilation toolkit
• sigurdschneider/lvc - LVC verified compiler
• formal-land/rocq-of-python - Translate Python code to Rocq code for formal verification. Applied to the reference implementation of the Ethereum VM in Python (WIP, in pause)
• pedrotst/coquedille - A Coq to Cedille compiler written in Coq
• peregrine-project/peregrine-tool - Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml
• coq-ext-lib/coq-compile - A compiler for Coq (archived)
• AU-COBRA/coq-rust-extraction - Coq plugin for extracting Rust code
• smorimoto/coq-to-ocaml-to-js - Proof of concept to generate safe and fast JavaScript

Networking and Distributed

Distributed Systems

• uwplse/verdi - A framework for formally verifying distributed systems implementations in Coq
• mit-pdos/perennial - Verifying concurrent storage and distributed systems
• uwplse/verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
• AU-COBRA/ConCert - A framework for smart contract verification in Coq
• verse-lab/toychain - A minimalistic blockchain consensus implemented and verified in Coq
• DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
• sec-bit/tokenlibs-with-proofs - Correctness proofs of Ethereum token contracts
• cmeiklejohn/distributed-data-structures - Distributed Data Structures in Coq
• pirapira/evmverif - An EVM code verification framework in Coq
• logsem/aneris - Program logic for developing and verifying distributed systems
• vrahli/Velisarios - A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
• rocq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
• novifinancial/LibraChain - A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover (archived)
• tezos/tezoscoq - working with coq and tezos
• Zilliqa/scilla-coq - State-Transition Systems for Smart Contracts (archived)
• AU-COBRA/PoS-NSB - A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq

User Interface

Applications and End User Tools

• clarus/coq-chick-blog - 🐣 A blog engine written and proven in Coq
• MichaelBurge/pornview - Porn browser formally-verified in Coq
• formal-land/coq-bonsai - 🌳 Generate a fresh bonsai in your terminal
• rocq-community/coqoban - Sokoban (in Coq) [maintainer=@erikmd]
• thery/T2048 - a version of the 2048 game for Coq
• rocq-community/sudoku - A certified Sudoku solver in Coq [maintainers=@siraben,@thery]

Utilities

General Purpose Libraries

• rocq-community/coq-ext-lib - A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
• coq-io/io - A library for effects in Coq.
• mit-plv/coqutil - Coq library for tactics, basic definitions, sets, maps
• math-comp/finmap - Finite sets, finite maps, multisets and generic sets
• tchajed/coq-record-update - Library to create Coq record update functions
• charguer/tlc - Library for Classical Coq
• arthuraa/extructures - Finite sets and maps for Coq with extensional equality
• vafeiadis/hahn - Hahn: A Coq library
• uwplse/StructTact - Coq utility and tactic library.
• rocq-community/bits - A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Science and Math

Mathematics

• HoTT/Coq-HoTT - A Coq library for Homotopy Type Theory
• UniMath/UniMath - This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
• jwiegley/category-theory - An axiom-free formalization of category theory in Coq for personal study and practical work
• math-comp/math-comp - Mathematical Components
• stepchowfun/proofs - My personal repository of formally verified mathematics.
• rocq-community/fourcolor - Formal proof of the Four Color Theorem [maintainer=@ybertot]
• UniMath/Foundations - Voevodsky's original development of the univalent foundations of mathematics in Coq
• math-comp/analysis - Mathematical Components compliant Analysis Library
• LogicalAtomist/principia-rewrite - The Principia Rewrite
• GeoCoq/GeoCoq - A formalization of geometry in Coq based on Tarski's axiom system
• rocq-community/math-classes - A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
• uds-psl/coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
• rocq-community/corn - Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
• amintimany/Categories - A formalization of category theory in the Coq proof assistant.
• rocq-community/hydra-battles - Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
• affeldt-aist/infotheo - A Rocq formalization of information theory and linear error-correcting codes
• rocq-community/coqeal - The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
• rocq-community/coq-100-theorems - Statements of famous theorems proven in Coq [maintainer=@jmadiot]
• meithecatte/busycoq - Busy Beaver deciders backed by Coq proof
• choukh/Set-Theory - A formalization of the textbook Elements of Set Theory
• vladimirias/Foundations - Voevodsky's original development of the univalent foundations of mathematics in Coq
• jtassarotti/coq-proba - A Probability Theory Library for the Coq Theorem Prover
• geohot/coq-hardy - Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
• damien-pous/relation-algebra - Relation algebra library for Coq
• rocq-community/topology - General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
• rocq-community/dedekind-reals - A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
• rocq-community/reglang - Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
• dschepler/coq-sequent-calculus - Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
• rocq-community/graph-theory - Graph Theory [maintainers=@chdoc,@damien-pous]
• thery/coqprime - Prime numbers for Coq
• math-comp/Coq-Combi - Algebraic Combinatorics in Coq
• math-comp/odd-order - The formal proof of the Odd Order Theorem
• langston-barrett/coq-big-o - A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
• artagnon/bonak - 🧊 An indexed construction of semi-simplicial and semi-cubical sets
• bmsherman/topology - Formal topology (and some probability) in Coq
• math-comp/Abel - A proof of Abel-Ruffini theorem.
• rocq-archive/zfc - An encoding of Zermelo-Fraenkel Set Theory in Coq
• rocq-community/gaia - Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
• rocq-community/goedel - Archived since the contents have been moved to the Hydras & Co. repository (archived)
• llee454/functional-algebra - 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.
• rocq-community/alea - Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
• rocq-community/apery - A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
• thery/hanoi - Hanoi tower in Coq
• rocq-community/bignums - Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
• sudgy/math-from-nothing - Developing mathematics in Rocq from the ground up
• Coq-Polyhedra/Coq-Polyhedra - Formalizing convex polyhedra in Coq
• Yosuke-Ito-345/Actuary - Formalization of the basic actuarial mathematics using Coq
• choukh/CategoryTheory - A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
• kai-qu/linear-logic - An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
• rocq-community/HighSchoolGeometry - Geometry in Coq for French high school [maintainer=@thery]
• styzystyzy/Axiomatic_Set_Theory - Formalization of Axiomatic Set Theory in Coq
• hivert/Coq-Combi - Algebraic Combinatorics in Coq

Formal Methods and Proofs

• formal-land/rocq-of-rust - Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
• magmide/magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
• uwdb/Cosette - Cosette is an automated SQL solver.
• MetaRocq/metarocq - Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
• PrincetonUniversity/VST - Verified Software Toolchain
• vellvm/vellvm - The Vellvm (Verified LLVM) coq development.
• DeepSpec/InteractionTrees - A Library for Representing Recursive and Impure Programs in Coq
• rocq-prover/equations - A function definition package for Rocq
• sifive/Kami - 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 - A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
• barry-jay-personal/tree-calculus - Proofs in Coq for the book Reflective Programs in Tree Calculus
• LPCIC/coq-elpi - Rocq plugin embedding Elpi
• jwiegley/coq-haskell - A library for formalizing Haskell types and functions in Coq
• smtcoq/smtcoq - Communication between Coq and SAT/SMT solvers
• mit-plv/kami - A Platform for High-Level Parametric Hardware Specification and its Modular Verification
• discus-lang/iron - Coq formalizations of functional languages.
• neelsomani/vericuda - A pipeline that translates Rust GPU code into formal Coq models, as a foundation for memory model proofs
• project-oak/silveroak - Formal specification and verification of hardware, especially for security and privacy. (archived)
• verse-lab/ceramist - Verified hash-based AMQ structures in Coq
• WasmCert/WasmCert-Coq - A mechanisation of Wasm in Rocq
• mit-plv/riscv-coq - RISC-V Specification in Coq
• SkyLabsAI/BRiCk - Formalization of C++ for verification purposes.
• clarus/falso - A proof of false in Coq.
• math-comp/hierarchy-builder - High level commands to declare a hierarchy based on packed classes
• SSProve/ssprove - A foundational framework for modular cryptographic proofs in Coq
• imdea-software/htt - Hoare Type Theory
• pi8027/lambda-calculus - A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
• affeldt-aist/monae - Monadic effects and equational reasoning in Rocq
• rocq-archive/coq-in-coq - A formalisation of the Calculus of Constructions
• rocq-community/autosubst - Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
• mit-plv/bedrock - Coq library for verified low-level programming
• snu-sf/paco - A Coq library for parametric coinduction
• lthms/FreeSpec - A framework for implementing and certifying impure computations in Coq
• 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.
• rocq-community/fav-ssr - Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
• uwplse/pumpkin-pi - An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
• CertiRocq/VeriFFI - VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
• foreverbell/verified - Coq formalizations and proofs of (data) structures and algorithms.
• vrahli/NuprlInCoq - Implementation of Nuprl's type theory in Coq
• wouter-swierstra/xmonad - xmonad in Coq
• rocq-community/paramcoq - Old Coq plugin for parametricity [maintainer=@ppedrot]
• snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
• logsem/clutch - Probabilistic separation logics for verifying higher-order probabilistic programs.
• takanuva/cps - A formalization of continuation-passing style calculi in Coq [WIP]
• EasyCrypt/certicrypt - CertiCrypt Coq Framework
• Lysxia/system-F - Formalization of the polymorphic lambda calculus and its parametricity theorem
• math-comp/algebra-tactics - Ring, field, lra, nra, and psatz tactics for Mathematical Components
• Blaisorblade/dot-iris - Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
• fblanqui/color - Coq library on rewriting theory and termination
• gangtan/CPUmodels - GoNative project: formal machines models in Coq
• imdea-software/fcsl-pcm - Partial Commutative Monoids
• CoqHott/logrel-coq - Logical Relation for MLTT in Coq
• VeriNum/vcfloat - VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
• reynir/Brainfuck - Brainfuck formalized in Coq
• huynhtrankhanh/CoqCP - We combat sloppy arguments in competitive programming and raise the standard of rigor
• math-comp/mczify - Micromega tactics for Mathematical Components
• rocq-community/dblib - Coq library for working with de Bruijn indices [maintainer=@KevOrr]
• rocq-community/trocq - A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx,@MysaaJava]
• weakmemory/imm - Intermediate Memory Model (IMM) and compilation correctness proofs for it
• acorrenson/SATurne - Tiny verified SAT-solver
• pa-ba/calc-comp - Coq proofs for the paper "Calculating Correct Compilers"
• rafaelcgs10/W-in-Coq - This is a Coq formalization of Damas-Milner type system and its algorithm W.
• dboulytchev/miniKanren-coq - A certified semantics for relational programming workout.
• rocq-community/lemma-overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
• arthuraa/deriving - Class instances for Coq inductive types with little boilerplate
• damien-pous/coinduction - coinduction library for Coq
• rocq-community/atbr - Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
• lastland/ClairvoyanceMonad - The Coq formalization of the paper Reasoning about the garden of forking paths.
• pi8027/stablesort - Stable sort algorithms and their stability proofs in Rocq
• sweirich/graded-haskell - Graded Dependent Type systems
• verif-scop/PolCert - A verified polyhedral scheduling validator in Coq. Vibing proving in progress: https://github.com/Hughshine/PolCert/tree/artifact/cpp27-anonymous-v10. Codex dev doc: https://github.com/verif-scop/polcert-dev/
• bobatkey/system-f-parametricity-model - A Model of Relationally Parametric System F in Coq
• dunnl/tealeaves - A Coq library for abstract syntactical reasoning
• CertiKOS/coqrel - Binary logical relations library for the Coq proof assistant
• jwiegley/coq-cds4ltl - A formal verification of Linear Temporal Logic in Coq
• Matafou/LibHyps - A Coq library providing tactics to deal with hypothesis
• sifive/ProcKami - Kami based processor implementations and specifications
• xavierleroy/canonical-binary-tries - Coq development accompanying the paper "Efficient Extensional Binary Tries"
• charguer/formalmetacoq - Arthur's Formal Metatheory in Coq
• rems-project/islaris - isla coq infrastructure
• Huxpro/WasmCert - A (in-development) Coq mechanization of WebAssembly specification.
• jwiegley/coq-lattice - A reflection-based proof tactic for lattices in Coq
• LS-Lab/Coq-dL - A formally verified implementation of differential dynamic logic in Coq
• rodrigogribeiro/unification - Formalisation of a type unification algorithm in Coq proof assistant.
• aslanix/SmallStepNI - Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq
• CertiGraph/CertiGraph - A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
• micro-policies/micro-policies-coq - Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
• heades/System-F-Coq - System F in coq.
• Ptival/HaysTac - A pile of Ltac tactics that might contain the needle you're looking for...
• aspiwack/cosa - A thing about Coq-verified Shape Analysis

Other

• gustavo-depaula/stalin-sort - Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
• hazelgrove/hazel - Hazel, a live functional programming environment with typed holes
• mit-plv/fiat-crypto - Cryptographic Primitive Code Generation by Fiat
• achlipala/frap - Formal Reasoning About Programs
• rocq-prover/vsrocq - Visual Studio Code extension for Rocq
• princeton-vl/CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
• ccz181078/Coq-BB5
• mit-plv/bedrock2 - A work-in-progress language and compiler for verified low-level programming
• QuickChick/QuickChick - Randomized Property-Based Testing Plugin for Coq
• lulinchen/cnn_open - A hardware implementation of CNN, written by Verilog and synthesized on FPGA
• mit-pdos/fscq - FSCQ is a certified file system written and proven in Coq
• hacspec/hacspec - Please see https://github.com/hacspec/hax (archived)
• accordproject/ergo - Programming Language for Smart Legal Contracts (archived)
• mit-plv/fiat - Mostly Automated Synthesis of Correct-by-Construction Programs
• rocq-archive/coq-serapi - Coq Protocol Playground with Se(xp)rialization of Internal Structures.
• fraunhoferfokus/acsl-by-example - Public snapshots of "ACSL by Example"
• uds-psl/MPCTT - Modeling and Proving in Computational Type Theory
• UniMath/TypeTheory - The mathematical study of type theories, in univalent foundations
• PrimeMHD/FPGA_ThreeLevelStorage - 【原创，已被编入官方教材】Three-level storage subsystem(SD+DDR2 SDRAM+Cache), based on Nexys4 FPGA board. 同济大学计算机系统结构课程设计，FPGA三级存储子系统。
• inQWIRE/QWIRE - A quantum circuit language and formal verification tool
• jonleivent/mindless-coding - Mindless, verified (erasably) coding using dependent types
• Ptival/PeaCoq - PeaCoq is a pretty Coq, isn't it?
• inQWIRE/SQIR - A Small Quantum Intermediate Representation
• logsem/iris-tutorial
• jwiegley/coq-pipes
• rocq-community/coq-dpdgraph - Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
• TheoWinterhalter/formal-type-theory - Formalising Type Theory in a modular way for translations between type theories
• TiarkRompf/collapsing-towers - Collapsing Towers of Interpreters
• EugeneLoy/coq_jupyter - Jupyter kernel for Coq
• UniMath/Schools
• DeepSpec/dsss17 - Lecture material for DeepSpec Summer School 2017
• robbertkrebbers/ch2o
• TiarkRompf/minidot - Dependent Object Types (DOT), bottom up
• coq-concurrency/pluto - A web server written in Coq.
• IBM/FormalML - Formalization of Machine Learning Theory with Applications to Program Synthesis
• ml4tp/gamepad - A Learning Environment for Theorem Proving
• NVlabs/ptxmemorymodel
• plclub/metalib - The Penn Locally Nameless Metatheory Library
• gtjennings1/UPDuino_v2_0 - UPDuino v2.0 - PCB Design Files, Designs, Documentation
• awslabs/aws-lc-verification - This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
• plclub/sf-in-lean - Development repo for translating Software Foundations to Lean
• sfja/sfja - SoftwareFoundations(Ja)
• codyroux/name-the-biggest-number
• samuelgruetter/dot-calculus - Formalization of the Dependent Object Types (DOT) calculus
• TiarkRompf/scala-escape - A compiler plug-in to control object lifetimes in Scala
• sweirich/corespec - A Specification for Dependent Types in Haskell (Core)
• querycert/qcert - Compilation and Verification of Data-Centric Languages
• peterlefanulumsdaine/general-type-theories - A (formalised) general definition of type theories
• sipa/safegcd-bounds - Bounds on divsteps iterations in safegcd
• TiarkRompf/reachability
• adampetcher/fcf - Foundational Cryptography Framework for machine-checked proofs of cryptography.
• Mtac2/Mtac2
• tcarstens/verlang
• rocq-community/parseque - Total Parser Combinators in Coq [maintainer=@womeier]
• Lysxia/profunctor-monad - Bidirectional programming in Haskell with monadic profunctors
• sweirich/replib - Replib: generic programming & Unbound: generic treatment of binders
• Veridise/Coda
• ChezJrk/verified-scheduling
• garrigue/certint - A Certified Interpreter for ML with Structural Polymorphism
• yugithub/OFDM-baseband - Verilog实现OFDM基带
• Lysxia/advent-of-coq-2021
• QinxiangCao/QualifiedCProgramming - QCP (Qualified C Programming), a C program verification tool
• UCSD-PL/proverbot9001
• plclub/cis670-16fa - Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016
• dbp/howtoproveacompiler - Writeup that goes along with this:
• inQWIRE/QuantumLib - Coq library for reasoning about quantum programs
• pirapira/dry-analyzer - Dr. Y's Ethereum Contract Analyzer
• rocq-prover/stdlib - Stdlib for the Rocq Prover
• HIPERFIT/contracts - Symbolic financial contract EDSL
• liufengyun/stoic - a capability-based system
• OUPL/MLCert - Certified Machine Learning
• RSPwFPGAs/opae-xilinx - OPAE porting to Xilinx FPGA devices.
• rems-project/archsem - Rocq framework to define the semantics of CPU architectures
• smtcoq/sniper
• rocq-archive/stdlib2
• tlringer/proof-demos - Repository where I'll collect some demos of proof assistants that I show to various people in order to spread the magic
• bit-mips/bitmips_experiments - 北京理工大学 MIPS 指令集 CPU 设计系列教学实验
• uds-psl/coq-library-complexity
• vzaliva/helix - Formally verified operator language and rewriting engine for high-performance computing
• aa755/ROSCoq - Robots powered by Constructive Reals
• formal-land/garden - Make your zero-knowledge circuits safe with formal verification. 🍀
• jwiegley/bytestring-fiat - An implementation of the Haskell ByteString library using the Fiat system from MIT
• Lysxia/rocq-simple-io - IO for Gallina
• vellvm/vellvm-legacy
• pedagand/MPRI-2.4-DTP - MPRI-2.4 Dependently-typed Functional Programming
• Beluga-lang/McTT - Building A Correct-By-Construction Proof Checkers For Type Theories
• KevinHexin/FPGA-Bicubic-interpolation - use Verilog HDL implemente bicubic interpolation in FPGA
• mit-frap/spring23 - Problem Sets for MIT 6.512 Formal Reasoning About Programs, Spring 2023
• tchajed/coq-tla
• 0xf3cd/CPU54-Pipeline - CPU based on MIPS with 5-stage pipeline and cache, working with DDR2 memory and SD card.
• affeldt-aist/robot-rocq - Mathematics of Robotic Manipulation using Rocq and MathComp
• coq-quantum/CoqQ
• mit-plv/bbv - Bedrock Bit Vector Library
• fredfeng/CS292C
• ichistmeinname/free-proving - Resources for "One Monad to Prove Them All"
• rocqetry/rocqet - Rocqet proof language
• barry-jay-personal/typed_tree_calculus - types for various combinatory systems, especialy tree calculi
• mit-plv/rewriter - Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
• PrincetonUniversity/DeepSpecDB
• Agnishom/lregex - Verified and Efficient Matching of Regular Expressions with Lookaround
• logsem/cerise - Formalisation of a capability machine and principles for reasoning about security properties
• runtimeverification/algorand-verification - Formal verification of the Algorand consensus protocol
• CategoricalData/HoTT-categories - A category theory library built on top of Homotopy Type Theory, by Jason Gross
• CharlesCNorton/intel-4004-verified - Formalizing the Intel 4004 microprocessor
• konne88/bagpipe - BGP Policy Verification
• LLM4Rocq/miniF2F-rocq - A Rocq version of the miniF2F dataset
• max2468tw/IC_Lab - NCTU 2018 Spring Integrated Circuit Design Laboratory
• QinxiangCao/UnifySL
• ynot-harvard/ynot - The Ynot Project source code.
• dricketts/teaching-concurrency - Specifications and safety proofs in different tools of a simple concurrent algorithm
• Javran/Thinking-dumps - This repo keeps track of my codes, answers and thinkings when exploring books.
• kcrary/istari
• kunalg123/riscv_workshop_collaterals - This repository is created for conducting RISC-V 5-day workshops
• MudroadWhite/Neo-Principia - Continuation on formalizing Principia Mathematica
• RiccardoBiosas/LeanGPT - Experiments with interactive theorem provers, LLMs and formal systems
• rocq-archive/automata - Beginning of formal language theory
• uwplse/cheerios - Formally verified Coq serialization library with support for extraction to OCaml
• ankitku/TAL0 - Based on paper by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety.
• coq-io/system - Library of Unix effects for Coq.
• mit-frap/spring18 - Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2018
• ropas/zooberry - A software framework for global sparse analyzers and their verified validators
• vellvm/ctrees - An itree-like data-structure to additionally support internal non-determinism
• fplaunchpad/cs6225_s25_iitm - Programs and Proofs -- Spring 2025 -- IITM
• katydid/regex-deriv-coq
• picodma/picodma-fpga
• robbertkrebbers/compcert - Fork of http://compcert.inria.fr/
• rocq-archive/ltl - Linear Temporal Logic
• uds-psl/autosubst-ocaml
• braibant/Synthesis
• inQWIRE/VyZX - Verifying the ZX Calculus
• JasonGross/autoformalization-transpilation - Using LLMs to transpile from Coq to Lean (public version, may be out of date)
• jonsterling/coq-guarded-computational-type-theory
• joscoh/why3-semantics - Formal Semantics for Why3
• mozow01/A1-2024-vill
• tymmym/software-foundations - Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
• arthuraa/memory-safe-language - A formalization of properties of a simple imperative, memory-safe language.
• atungare/coq-software-foundations
• bloomberg/game-trees - Functions and proofs about game trees in Rocq, implemented as rose trees.
• daniellustig/pipecheck
• dongjaelee1/refinement-tutorial - Tutorial for refinement based verification
• julesjacobs/cgraphs - Deadlock freedom by type checking
• katamaran-project/katamaran - Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.
• l2ctsinghua/l2c
• Lysxia/coq-ceres - Coq library for serialization to S-expressions
• maximedenes/coq-amd64
• mit-frap/spring17 - Problem Sets for MIT 6.887 Formal Reasoning About Programs, Spring 2017
• mit-frap/spring22 - Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2022
• uds-psl/coq-synthetic-computability