Skip to content

Trending repositories

Find what repositories the GitHub community is most excited about this month.

  1. uwplse / verdi

    A framework for formally verifying distributed systems implementations in Coq

    Coq • 17 stars this month • Built by @dwoos @wilcoxjay @Anxuiz @ztatlock @palmskog

  2. UniMath / UniMath

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

    Coq • 7 stars this month • Built by @DanGrayson @benediktahrens @cathlelay @vladimirias @mortberg

  3. HoTT / HoTT

    Homotopy type theory

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

  4. AbsInt / CompCert

    The CompCert C verified compiler

    Coq • Built by @bschommer @xavierleroy @fpottier @m-schmidt @clarus

  5. vladimirias / Foundations

    Development of the univalent foundations of mathematics in Coq

    Coq • Built by @vladimirias @DanGrayson

  6. jscert / jscert

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

  7. clarus / coq-chick-blog

    A blog engine written and proven in Coq.

    Coq • Built by @clarus @alokmenghrajani

  8. jwiegley / coq-pipes

    Coq • Built by @jwiegley

  9. namin / dot

    formalization of the Dependent Object Types (DOT) calculus

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

  10. mit-pdos / fscq-impl

    FSCQ is a certified file system written and proven in Coq

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

  11. jonleivent / mindless-coding

    Mindless, verified (erasably) coding using dependent types

    Coq • Built by @jonleivent

  12. clarus / falso

    A proof of false.

    Coq • Built by @clarus

  13. robbertkrebbers / ch2o

    Coq • Built by @robbertkrebbers

  14. jwiegley / category-theory

    A formalization of category theory in Coq for personal study

    Coq • Built by @jwiegley @ekmett

  15. sfja / sfja


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

  16. math-classes / math-classes

    A library of abstract interfaces for mathematical structures in Coq.

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

  17. jwiegley / coq-haskell

    A library for formalizing Haskell types and functions in Coq

    Coq • Built by @jwiegley

  18. tcarstens / verlang

    Coq • Built by @tcarstens

  19. coq-concurrency / pluto

    A web server written in Coq.

    Coq • Built by @clarus

  20. cmeiklejohn / distributed-data-structures

    Distributed Data Structures in Coq

    Coq • Built by @cmeiklejohn

  21. coq-ext-lib / coq-ext-lib

    A library of Coq definitions, theorems, and tactics.

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

  22. c-corn / corn

    Coq Repository at Nijmegen

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

  23. QuickChick / QuickChick

    Randomized Property-Based Testing Plugin for Coq

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

  24. DDCSF / iron

    Coq formalizations of functional languages.

    Coq • Built by @benl23x5

  25. aa755 / ROSCoq

    Robots powered by Constructive Reals

    Coq • Built by @aa755 @aa755msr


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