156 Open source projects that are alternatives of or similar to coqeal

The formal proof of the Odd Order Theorem

Formalization of the basic actuarial mathematics using Coq

A proof of Abel-Ruffini theorem.

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

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

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

Multinomials for the Mathematical Components library.

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

Finite sets, finite maps, multisets and generic sets

Stable sort algorithms and their stability proofs in Coq

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

A Library for Representing Recursive and Impure Programs in Coq

A Learning Environment for Theorem Proving with the Coq proof assistant

Proof of concept to generate safe and fast JavaScript

Import OCaml programs to Coq 🐓 🐫

Randomized Property-Based Testing Plugin for Coq

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

The Language for Smart Legal Contracts

🐣 A blog engine written and proven in Coq

Mindless, verified (erasably) coding using dependent types

Reference sheet for the Coq language.

A mechanisation of Wasm in Coq

A function definition package for Coq

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

Formal proof of the Four Color Theorem

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

FSCQ is a certified file system written and proven in Coq

formalization of the Dependent Object Types (DOT) calculus

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

Mostly Automated Synthesis of Correct-by-Construction Programs

Metaprogramming in Coq

Coq formalizations of functional languages.

No description or website provided.

Interactive Coq Proofs in Vim

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

Verified hash-based AMQ structures in Coq

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

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

Recipe for FPGA cooking

PeaCoq is a pretty Coq, isn't it?

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

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

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

Goose converts a small subset of Go to Coq

Coq Support for Visual Studio Code

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

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

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

A minimalistic blockchain consensus implemented and verified in Coq

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

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

A Verified Compiler for Gallina, Written in Gallina

SoftwareFoundations(Ja)

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

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

RISC-V Specification in Coq

The Vellvm (Verified LLVM) coq development.