The Rocq Prover is an interactive theorem prover, or proof assistant. 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.

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

A Seamless, Interactive Tactic Learner and Prover for Coq

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Code resources from John Harrison's "Handbook of Practical Logic and Automated Reasoning"

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

A prototypical proof checker and programming language based on illative combinatory logic

HOL-Light Library for Modal Systems

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

An imperative language, logic parser and simple theorem prover designed to function via a CLI.

Toy theorem prover based on the calculus of constructions

A simple first order logic theorem prover using tableaux

A logic-based library for correct-by-construction process modelling and composition.

A kernel using inference rules in order to compute the three of proves.

Project for CSEEE6863_001_2016_3 - FORMAL VERIF HW SW SYSTEMS