Trending in open source
See what the GitHub community is most excited about this week.
Sign up for free to get started
-
AbsInt / CompCert
The CompCert C verified compiler
-
PrincetonUniversity / VST
Verified Software Toolchain
-
HoTT / HoTT
Homotopy type theory
-
uwplse / verdi
A framework for formally verifying distributed systems implementations in Coq
-
vladimirias / Foundations
Development of the univalent foundations of mathematics in Coq
-
UniMath / UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
jscert / jscert
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
-
clarus / coq-chick-blog
A blog engine written and proven in Coq.
-
jwiegley / coq-pipes
-
namin / dot
formalization of the Dependent Object Types (DOT) calculus
-
mit-pdos / fscq-impl
FSCQ is a certified file system written and proven in Coq
-
jonleivent / mindless-coding
Mindless, verified (erasably) coding using dependent types
-
robbertkrebbers / ch2o
-
clarus / falso
A proof of false.
-
jwiegley / category-theory
A formalization of category theory in Coq for personal study
-
jwiegley / coq-haskell
A library for formalizing Haskell types and functions in Coq
-
sfja / sfja
SoftwareFoundations(Ja)
-
math-classes / math-classes
A library of abstract interfaces for mathematical structures in Coq.
-
coq-concurrency / pluto
A web server written in Coq.
-
tcarstens / verlang
-
cmeiklejohn / distributed-data-structures
Distributed Data Structures in Coq
-
c-corn / corn
Coq Repository at Nijmegen
-
coq-ext-lib / coq-ext-lib
A library of Coq definitions, theorems, and tactics.
-
QuickChick / QuickChick
Randomized Property-Based Testing Plugin for Coq
-
aa755 / ROSCoq
Robots powered by Constructive Reals