Open source projects in Coq

  • AbsInt/CompCert

    The CompCert formally-verified C compiler

    ☕Coq   ★479 stars   ⚠14 open issues   ⚭6 contributors   ☯about 4 years old  
  • UniMath/UniMath

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

    ☕Coq   ★341 stars   ⚠114 open issues   ⚭9 contributors   ☯almost 5 years old  
  • sfja/sfja

    SoftwareFoundations(Ja)

    ☕Coq   ★52 stars   ⚠19 open issues   ⚭10 contributors   ☯about 7 years old  
  • clarus/falso

    A proof of false.

    ☕Coq   ★59 stars   ⚠0 open issues   ⚭1 contributors   ☯over 3 years old  
  • robbertkrebbers/ch2o

    ☕Coq   ★71 stars   ⚠0 open issues   ⚭1 contributors   ☯over 6 years old  
  • jonleivent/mindless-coding

    Mindless, verified (erasably) coding using dependent types

    ☕Coq   ★102 stars   ⚠0 open issues   ⚭1 contributors   ☯over 4 years old  
  • mit-pdos/fscq-impl

    FSCQ is a certified file system written and proven in Coq

    ☕Coq   ★136 stars   ⚠8 open issues   ⚭12 contributors   ☯over 3 years old  
  • namin/dot

    formalization of the Dependent Object Types (DOT) calculus

    ☕Coq   ★95 stars   ⚠0 open issues   ⚭4 contributors   ☯almost 7 years old  
  • jwiegley/coq-pipes

    ☕Coq   ★101 stars   ⚠1 open issues   ⚭1 contributors   ☯over 3 years old  
  • clarus/coq-chick-blog

    A blog engine written and proven in Coq.

    ☕Coq   ★138 stars   ⚠1 open issues   ⚭2 contributors   ☯almost 4 years old  
  • jscert/jscert

    A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

    ☕Coq   ★158 stars   ⚠4 open issues   ⚭13 contributors   ☯almost 5 years old  
  • vladimirias/Foundations

    Voevodsky's original development of the univalent foundations of mathematics in Coq

    ☕Coq   ★2 stars   ⚠0 open issues   ⚭2 contributors   ☯about 1 year old  
  • HoTT/HoTT

    Homotopy type theory

    ☕Coq   ★545 stars   ⚠77 open issues   ⚭22 contributors   ☯over 7 years old  
  • uwplse/verdi

    A framework for formally verifying distributed systems implementations in Coq

    ☕Coq   ★357 stars   ⚠2 open issues   ⚭4 contributors   ☯about 4 years old  
  • jwiegley/coq-haskell

    A library for formalizing Haskell types and functions in Coq

    ☕Coq   ★97 stars   ⚠0 open issues   ⚭1 contributors   ☯over 4 years old  
  • aa755/ROSCoq

    Robots powered by Constructive Reals

    ☕Coq   ★27 stars   ⚠0 open issues   ⚭2 contributors   ☯over 3 years old  
  • PrincetonUniversity/VST

    Verified Software Toolchain

    ☕Coq   ★89 stars   ⚠15 open issues   ⚭9 contributors   ☯about 4 years old  
  • DDCSF/iron

    Coq formalizations of functional languages.

    ☕Coq   ★59 stars   ⚠0 open issues   ⚭1 contributors   ☯about 5 years old  
  • achlipala/frap

    Formal Reasoning About Programs

    ☕Coq   ★218 stars   ⚠0 open issues   ⚭3 contributors   ☯almost 3 years old  
  • amintimany/Categories

    ☕Coq   ★78 stars   ⚠0 open issues   ⚭1 contributors   ☯about 3 years old  
  • math-comp/math-comp

    Mathematical Components

    ☕Coq   ★129 stars   ⚠47 open issues   ⚭11 contributors   ☯almost 4 years old  
  • jwiegley/category-theory

    A formalization of category theory in Coq for personal study and practical work

    ☕Coq   ★299 stars   ⚠1 open issues   ⚭2 contributors   ☯over 4 years old  
  • pi8027/lambda-calculus

    A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2

    ☕Coq   ★33 stars   ⚠1 open issues   ⚭1 contributors   ☯almost 6 years old  
  • math-classes/math-classes

    A library of abstract interfaces for mathematical structures in Coq.

    ☕Coq   ★77 stars   ⚠5 open issues   ⚭7 contributors   ☯over 7 years old  
  • coq-concurrency/pluto

    A web server written in Coq.

    ☕Coq   ★62 stars   ⚠2 open issues   ⚭1 contributors   ☯about 4 years old  
  • coq-ext-lib/coq-ext-lib

    A library of Coq definitions, theorems, and tactics.

    ☕Coq   ★45 stars   ⚠11 open issues   ⚭8 contributors   ☯over 6 years old  
  • c-corn/corn

    Coq Repository at Nijmegen

    ☕Coq   ★53 stars   ⚠2 open issues   ⚭11 contributors   ☯over 7 years old  
  • cmeiklejohn/distributed-data-structures

    Distributed Data Structures in Coq

    ☕Coq   ★40 stars   ⚠0 open issues   ⚭1 contributors   ☯over 5 years old  
  • vellvm/vellvm-legacy

    ☕Coq   ★32 stars   ⚠10 open issues   ⚭3 contributors   ☯over 4 years old  
  • Karmaki/coq-dpdgraph

    Build dependency graphs between COQ objects

    ☕Coq   ★33 stars   ⚠3 open issues   ⚭3 contributors   ☯almost 5 years old