Custom tactic named "ij_injectfalse" injects False into the hypothesis

Tools for working with Verified Software Units

A verified(?) TCP client/server chat application

Dead-Simple Build System for Coq

Coq plugin to generate type inequality axioms for inductive definitions

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

OCaml module of Nijn to generate coq scripts for checking termination proofs of higher-order rewriting systems.

Coq plugin for printing term abstract syntax trees and their digests

A simple first order logic theorem prover using tableaux

A formatter/linter for Coq source

Fun plugin to play with the Gallina AST.

Pure Demand Operational Semantics

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

A experimental compiler from Kind (Core) to Coq

Parse Coq log files and plot resolution trees

A proof tree viewer that works with Coq through Proof General

Coq plugin for plain dependency extraction

Translate Rust 🦀 LLBC code (generated by https://github.com/AeneasVerif/charon) to Coq 🐓

Prettify the output of coq makefiles

Useful utility functions for writing Coq plugins