Skip to content

Trending in open source

See what the GitHub community is most excited about this week.

  1. AbsInt / CompCert

    The CompCert C verified compiler

    Coq • 5 stars this week • Built by @bschommer @xavierleroy @fpottier @m-schmidt @jhjourdan

  2. PrincetonUniversity / VST

    Verified Software Toolchain

    Coq • Built by @andrew-appel @gstew5 @QinxiangCao @jldodds @mmcgil

  3. HoTT / HoTT

    Homotopy type theory

    Coq • Built by @JasonGross @mikeshulman @andrejbauer @spitters @peterlefanulumsdaine

  4. uwplse / verdi

    A framework for formally verifying distributed systems implementations in Coq

    Coq • Built by @dwoos @wilcoxjay @Anxuiz @ztatlock @palmskog

  5. vladimirias / Foundations

    Development of the univalent foundations of mathematics in Coq

    Coq • Built by @vladimirias @DanGrayson

  6. UniMath / UniMath

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

    Coq • Built by @DanGrayson @benediktahrens @cathlelay @mortberg @vladimirias

  7. jscert / jscert

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

    Coq • Built by @Mbodin @brabalan @da319 @edgemaster @dfilaretti

  8. clarus / coq-chick-blog

    A blog engine written and proven in Coq.

    Coq • Built by @clarus @alokmenghrajani

  9. jwiegley / coq-pipes

    Coq • Built by @jwiegley

  10. namin / dot

    formalization of the Dependent Object Types (DOT) calculus

    Coq • Built by @namin @adriaanm @lindydonna @smarter

  11. mit-pdos / fscq-impl

    FSCQ is a certified file system written and proven in Coq

    Coq • Built by @zeldovich @kaashoek @tchajed @haogang @daniel-ziegler

  12. jonleivent / mindless-coding

    Mindless, verified (erasably) coding using dependent types

    Coq • Built by @jonleivent

  13. robbertkrebbers / ch2o

    Coq • Built by @robbertkrebbers

  14. clarus / falso

    A proof of false.

    Coq • Built by @clarus

  15. jwiegley / category-theory

    A formalization of category theory in Coq for personal study

    Coq • Built by @jwiegley @ekmett

  16. jwiegley / coq-haskell

    A library for formalizing Haskell types and functions in Coq

    Coq • Built by @jwiegley

  17. sfja / sfja

    SoftwareFoundations(Ja)

    Coq • Built by @ummr @katayamak @mzp @yoshihiro503 @leque

  18. math-classes / math-classes

    A library of abstract interfaces for mathematical structures in Coq.

    Coq • Built by @robbertkrebbers @Eelis @tomprince @spitters @wires

  19. coq-concurrency / pluto

    A web server written in Coq.

    Coq • Built by @clarus

  20. tcarstens / verlang

    Coq • Built by @tcarstens

  21. cmeiklejohn / distributed-data-structures

    Distributed Data Structures in Coq

    Coq • Built by @cmeiklejohn

  22. c-corn / corn

    Coq Repository at Nijmegen

    Coq • Built by @robbertkrebbers @Eelis @spitters @EvgenyMakarov @wires

  23. coq-ext-lib / coq-ext-lib

    A library of Coq definitions, theorems, and tactics.

    Coq • Built by @gmalecha @davdar @thinkmoore @jesper-bengtson @clarus

  24. QuickChick / QuickChick

    Randomized Property-Based Testing Plugin for Coq

    Coq • Built by @catalin-hritcu @zoep @maximedenes @lemonidas @arthuraa

  25. aa755 / ROSCoq

    Robots powered by Constructive Reals

    Coq • Built by @aa755 @aa755msr

ProTip! Looking for recently updated Coq repositories? Try this search
Something went wrong with that request. Please try again.