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

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

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

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

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

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

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

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

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

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

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

Recipe for FPGA cooking

A minimalistic blockchain consensus implemented and verified in Coq

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

Formalization of the basic actuarial mathematics using Coq

A library for formalizing Haskell types and functions in Coq

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

Archive for all Coq related OPAM packages organized in various repositories

formalization of the Dependent Object Types (DOT) calculus

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

Goose converts a small subset of Go to Coq

Mostly Automated Synthesis of Correct-by-Construction Programs

Coq formalizations of functional languages.

The Vellvm (Verified LLVM) coq development.

Interactive Coq Proofs in Vim

Verified hash-based AMQ structures in Coq

🐣 A blog engine written and proven in Coq

Reference sheet for the Coq language.

A function definition package for Coq

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

FSCQ is a certified file system written and proven in Coq

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

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

Coq plugin embedding elpi

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

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

Proof of concept to generate safe and fast JavaScript

A selection of formal proofs in Coq.

Formalization of Typed Assembly Language (TAL) in Coq

A Library for Representing Recursive and Impure Programs in Coq

A mechanisation of Wasm in Coq

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

Import OCaml programs to Coq 🐓 🐫

PeaCoq is a pretty Coq, isn't it?

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

A core language for rule-based hardware design 🦑

The Language for Smart Legal Contracts

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

Mindless, verified (erasably) coding using dependent types

Convert Haskell source code to Coq source code.

A Learning Environment for Theorem Proving with the Coq proof assistant

Stable sort algorithms and their stability proofs in Coq

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

Metaprogramming in Coq

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

Formal proof of the Four Color Theorem

Randomized Property-Based Testing Plugin for Coq

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

Formalization of the polymorphic lambda calculus and its parametricity theorem