152 Open source projects that are alternatives of or similar to regex-reexamined-coq

FSCQ is a certified file system written and proven 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

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

Goose converts a small subset of Go to Coq

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

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

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

Template project for program verification in Coq

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

No description or website provided.

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

Mostly Automated Synthesis of Correct-by-Construction Programs

Archive for all Coq related OPAM packages organized in various repositories

The Vellvm (Verified LLVM) coq development.

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

Metaprogramming in Coq

Formalization of the basic actuarial mathematics using Coq

Recipe for FPGA cooking

Gallina to Bedrock2 compilation toolkit

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

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

A library for formalizing Haskell types and functions in Coq

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

formalization of the Dependent Object Types (DOT) calculus

A minimalistic blockchain consensus implemented and verified in Coq

Proof of concept to generate safe and fast JavaScript

Import OCaml programs to Coq 🐓 🐫

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

A mechanisation of Wasm in Coq

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

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

Convert Haskell source code to Coq source code.

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

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

A Learning Environment for Theorem Proving with the Coq proof assistant

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

Randomized Property-Based Testing Plugin for Coq

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

🐣 A blog engine written and proven in Coq

Formalization of Typed Assembly Language (TAL) in Coq

A function definition package for Coq

The formal proof of the Odd Order Theorem

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

A core language for rule-based hardware design 🦑

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

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

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

Stable sort algorithms and their stability proofs in Coq

A selection of formal proofs in Coq.

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

A Library for Representing Recursive and Impure Programs in Coq

Reference sheet for the Coq language.

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

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

Coq plugin embedding elpi

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

Mutation analysis tool for Coq verification projects

Partial Commutative Monoids

Formalization of the polymorphic lambda calculus and its parametricity theorem

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