158 Open source projects that are alternatives of or similar to mcoq

A Learning Environment for Theorem Proving with the Coq proof assistant

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

A core language for rule-based hardware design 🦑

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

A Library for Representing Recursive and Impure Programs in Coq

SigProfilerMatrixGenerator creates mutational matrices for all types of somatic mutations. It allows downsizing the generated mutations only to parts for the genome (e.g., exome or a custom BED file). The tool seamlessly integrates with other SigProfiler tools.

🐣 A blog engine written and proven in Coq

Intermediate Memory Model (IMM) and compilation correctness proofs for it

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

Reference sheet for the Coq language.

A mechanisation of Wasm in Coq

Import OCaml programs to Coq 🐓 🐫

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

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

Template project for program verification in Coq

Randomized Property-Based Testing Plugin for Coq

Formalization of Typed Assembly Language (TAL) in Coq

A function definition package for Coq

Partial Commutative Monoids

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

Stable sort algorithms and their stability proofs in Coq

A selection of formal proofs in Coq.

Formalization of the polymorphic lambda calculus and its parametricity theorem

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

Coq plugin embedding elpi

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

Coq formalizations of functional languages.

Convert Haskell source code to Coq source code.

Goose converts a small subset of Go to Coq

A library of mechanised undecidability proofs in the Coq proof assistant.

The Vellvm (Verified LLVM) coq development.

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

FSCQ is a certified file system written and proven in Coq

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

Metaprogramming in Coq

Formalization of the basic actuarial mathematics using Coq

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

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Recipe for FPGA cooking

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

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

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

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

Coq to OCaml FFI made easy [maintainer=@lthms]

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

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

A library for formalizing Haskell types and functions in Coq

No description or website provided.

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

A formally verified high-level synthesis tool based on CompCert and written in Coq.

formalization of the Dependent Object Types (DOT) calculus

A minimalistic blockchain consensus implemented and verified in Coq

Mostly Automated Synthesis of Correct-by-Construction Programs

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

Descartes supports developers to improve their test suites by reporting weak spots in covered code

Gallina to Bedrock2 compilation toolkit

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

Archive for all Coq related OPAM packages organized in various repositories

Proof of concept to generate safe and fast JavaScript