Abella
Abella is an interactive theorem prover developed by Andrew Gacek while a PhD student at the University of Minnesota and a postdoc within the Parsifal project. This system include declarative support for λ-tree syntax (an approach to syntax with bindings), the two-level approach to reasoning about logic specifications, the ∇-quantification, and nominal abstractions. Many examples in the meta-theory of the lambda-calculus and π-calculus have been developed.
Bedwyr
Bedwyr is a model checker that allows for reasoning directly on syntactic expressions (even those contining bindings). The earlier Level 0/1 prover was rewritten into OCaml by David Baelde and Axelle Zeigler and then greatly extended by David Baelde and Andrew Gacek during the summer of 2006. Currently (2012/2013), Quentin Heath is improving and extending Bedwyr. The system is being developed on the INRIA Gforge open source platform. See the Bedwyr page in the Slimmer GForge project.
Psyche
Psyche is a modular proof-search engine for automated or interactive theorem proving, developed in OCaml by Stéphane Graham-Lengrand and the PSI project. Its specificity is to use modularity to provide both trust and efficiency, experimenting for this a new version of Milner’s LCF architecture that is based on focusing: A trustable kernel is isolated in the source code and only applies straightforward proof-search mechanisms, while proof-search heuristics are implemented outside the kernel thanks to Psyche’s modular interface. This gives high confidence in the tool’s output, while its efficiency is currently tested by simulating standard SMT-solving techniques such as DPLL(T).
Profound
Profound is an experiment in interactive theorem proving without the use of formal proof languages. The user builds proofs by manipulating the text of the theorem using popular interaction devices like mice and touchscreens and popular interaction metaphors such as pointing, selecting, and drag-and-dropping. The system nevertheless guarantees correctness of every user action. One of the features of this system is a lightweight history mechanism that lets users revisit earlier actions and fork the “timeline” without the risk of losing work; this history is persistent and can be reused across sessions.
Teyjus
Teyjus is an implementation of λProlog carried out by a team led by Gopalan Nadathur. Teyjus is a commonly used prototyping tool for this team.
Older systems
Tac
Tac is an interactive and automatic theorem prover for an intuitionistic logic extended with fixed points and generic (∇) quantification. Tac is based on recent research work by David Baelde and others. It has been implemented by David Baelde and Alexandre Viel (INRIA & LIX/Ecole Polytechnique) and Zach Snow (University of Minnesota – Minneapolis). See the Tac page in the Slimmer GForge project.
Level 0/1
Alwen Tiu has a prototype implementation of a logic system that can reason on “levels 0 and 1”. The system integrates finite success and finite failure as proof search for a single logic.
