152 Open source projects that are alternatives of or similar to Metacoq

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

A blog about Coq

The Language for Smart Legal Contracts

Bidirectional programming in Haskell with monadic profunctors

Import OCaml programs to Coq 🐓 🐫

Verifying concurrent crash-safe systems

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

Total Parser Combinators in Coq

The mathematical study of type theories, in univalent foundations

A Hello World program in Coq.

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

A Verified Compiler for Gallina, Written in Gallina

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

Collapsing Towers of Interpreters

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

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

A function definition package for Coq

A framework for implementing and certifying impure computations in Coq

Mindless, verified (erasably) coding using dependent types

Coq plugin for parametricity [[email protected]]

A selection of formal proofs in Coq.

Implementation of sprintf for Coq

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

Coq Support for Visual Studio Code

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

formalization of the Dependent Object Types (DOT) calculus

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

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

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

Mostly Automated Synthesis of Correct-by-Construction Programs

SoftwareFoundations(Ja)

Recipe for FPGA cooking

RISC-V Specification in Coq

Coq formalizations of functional languages.

A compiler plug-in to control object lifetimes in Scala

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

Interactive Coq Proofs in Vim

The Penn Locally Nameless Metatheory Library

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

Porn browser formally-verified in Coq

Verified hash-based AMQ structures in Coq

A Certified Interpreter for ML with Structural Polymorphism

A library for formalizing Haskell types and functions in Coq

The CompCert formally-verified C compiler

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

Implementation of Nuprl's type theory in 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

Homotopy type theory

PeaCoq is a pretty Coq, isn't it?

Verified vector clocks, with Coq!

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

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

Randomized Property-Based Testing Plugin for Coq

🐣 A blog engine written and proven in Coq

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

A Library for Representing Recursive and Impure Programs in Coq

Formal proof of the Four Color Theorem