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

Coq plugin for plain dependency extraction

Fun plugin to play with the Gallina AST.

Proofbox : 2022 A tool to serve smt solvers (and some other formal verification tools) jobs

An interpreter for an imperative language and a Hoare logic prover

Parse Coq log files and plot resolution trees

Tools for working with Verified Software Units

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.

Dead-Simple Build System for Coq

A simple first order logic theorem prover using tableaux

Custom tactic named "ij_injectfalse" injects False into the hypothesis

Prettify the output of coq makefiles

A Coq plugin for Codewars

Script to remove unnecessary module imports from Coq sourcess

A experimental compiler from Kind (Core) to Coq

Useful utility functions for writing Coq plugins

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

Pure Demand Operational Semantics

Coq plugin for printing term abstract syntax trees and their digests

Modification to Coq to record intermediate proof states encountered during a proof