A modern proof language
SRI Yices SMT Solver
ACL2 System and Books as Maintained by the Community
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Links to tools by subject
A repository to store Z3-python scripts you can use as examples, reminders, whatever.
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
My sandbox for experimenting with solver algorithms.
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
VSCode extension that is designed to help automate writing of Coq proofs.
Cicada Language (solo version)
Large Scale Type Systems: ML/C Hybrid Programming Language
Tableau-based Theorem Prover for Natural Logic and Language
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
Resolution theorem proving for predicate logic in pure Python.
Cicada Language (PLCT little team)
GCLC is a mathematical software tool for producing high-quality mathematical illustrations, for teaching mathematics, and for automated proving of geometry theorems.
To associate your repository with the theorem-prover topic, visit your repo's landing page and select "manage topics."