Top 153 coq open source projects

The Vellvm (Verified LLVM) coq development.

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

FSCQ is a certified file system written and proven in Coq

A Learning Environment for Theorem Proving with the Coq proof assistant

Metaprogramming in Coq

Randomized Property-Based Testing Plugin for Coq

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

🐣 A blog engine written and proven in Coq

Recipe for FPGA cooking

A function definition package for Coq

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

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

A Visual Studio Code extension for Coq [[email protected],@fakusb]

A work-in-progress language and compiler for verified low-level programming

Advent of Code 2018, in Coq! (https://adventofcode.com/2018)

A library for formalizing Haskell types and functions in Coq

A selection of formal proofs in Coq.

A library of abstract interfaces for mathematical structures in Coq [[email protected]]

A Library for Representing Recursive and Impure Programs in Coq

formalization of the Dependent Object Types (DOT) calculus

A formalization of geometry in Coq based on Tarski's axiom system

Mostly Automated Synthesis of Correct-by-Construction Programs

Import OCaml programs to Coq 🐓 🐫

Coq formalizations of functional languages.

A curated set of links to formal methods involving provable code.

Interactive Coq Proofs in Vim

The Language for Smart Legal Contracts

Verified hash-based AMQ structures in Coq

Mindless, verified (erasably) coding using dependent types

A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]

PeaCoq is a pretty Coq, isn't it?

A SuperCompiler for Martin-Löf's Type Theory

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Formal proof of the Four Color Theorem

Coq Support for Visual Studio Code

The mathematical study of type theories, in univalent foundations

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Formalising Type Theory in a modular way for translations between type theories

A Verified Compiler for Gallina, Written in Gallina

SoftwareFoundations(Ja)

A Coq-based synthesis of Scala programs which are correct-by-construction

RISC-V Specification in Coq

Collapsing Towers of Interpreters

A compiler plug-in to control object lifetimes in Scala

Verifying concurrent crash-safe systems

Formal specification and verification of hardware, especially for security and privacy.

The Penn Locally Nameless Metatheory Library

A blog about Coq

Porn browser formally-verified in Coq

A framework for implementing and certifying impure computations in Coq

A Certified Interpreter for ML with Structural Polymorphism

Total Parser Combinators in Coq

The CompCert formally-verified C compiler

Coq plugin for parametricity [[email protected]]

Implementation of Nuprl's type theory in Coq

Bidirectional programming in Haskell with monadic profunctors