**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.