152 Open source projects that are alternatives of or similar to odd-order

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Multinomials for the Mathematical Components library.

Finite sets, finite maps, multisets and generic sets

Stable sort algorithms and their stability proofs in Coq

Formalization of the basic actuarial mathematics using Coq

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

A proof of Abel-Ruffini theorem.

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

The Vellvm (Verified LLVM) coq development.

A Learning Environment for Theorem Proving with the Coq proof assistant

Metaprogramming in Coq

Goose converts a small subset of Go to Coq

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

FSCQ is a certified file system written and proven in Coq

Template project for program verification in Coq

🐣 A blog engine written and proven in Coq

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

Recipe for FPGA cooking

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

Partial Commutative Monoids

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

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

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

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

No description or website provided.

A library for formalizing Haskell types and functions in Coq

A mechanisation of Wasm in Coq

Convert Haskell source code to Coq source code.

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

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

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

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

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

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

Randomized Property-Based Testing Plugin for Coq

Formalization of Typed Assembly Language (TAL) in Coq

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

Formalization of the polymorphic lambda calculus and its parametricity theorem

A minimalistic blockchain consensus implemented and verified in Coq

formalization of the Dependent Object Types (DOT) calculus

A function definition package for Coq

A core language for rule-based hardware design 🦑

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

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

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

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

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

A selection of formal proofs in Coq.

Reference sheet for the Coq language.

A Library for Representing Recursive and Impure Programs in Coq

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

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

Coq plugin embedding elpi

Mostly Automated Synthesis of Correct-by-Construction Programs

Import OCaml programs to Coq 🐓 🐫

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

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

Coq formalizations of functional languages.

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

Proof of concept to generate safe and fast JavaScript