abella-prover/abella

An interactive theorem prover based on lambda-tree syntax

OCaml

101

1,388 commits

updated Sep 9, 2026

See the code

README

Quick Start

The easiest way to install Abella is using OPAM (version 2.1+).

  1. Go to the topmost directory of the clone of this repository, i.e., the location of this very README.md file.
  2. Run: opam pin abella . (note the final period)
  3. When prompted by OPAM, say yes to install Abella.
  4. Whenever you do a git pull, also do: opam reinstall abella.

To uninstall Abella using OPAM, do:

  1. Run: opam remove abella.
  2. Then run: opam unpin abella.

More Information

Use the following walkthrough for an introduction to using Abella:

https://abella-prover.org/walkthrough.html

More information on Abella is available at

https://abella-prover.org/

Bugs, Feature Requests, and Issues

Please report all bugs, feature requests, and issues on the GitHub issue tracker for Abella, available from:

https://github.com/abella-prover/abella/issues

Discussion of Abella and its uses happens on this mailing list.

http://groups.google.com/group/abella-theorem-prover

interactive-theorem-proving
lambda-calculus
meta-theory

Contributors

agacek

883 commits

chaudhuri

417 commits

yvting

60 commits

robblanco

20 commits

abella-prover/abella

An interactive theorem prover based on lambda-tree syntax

OCaml

101

1,388 commits

updated Sep 9, 2026

See the code

README

Quick Start

The easiest way to install Abella is using OPAM (version 2.1+).

  1. Go to the topmost directory of the clone of this repository, i.e., the location of this very README.md file.
  2. Run: opam pin abella . (note the final period)
  3. When prompted by OPAM, say yes to install Abella.
  4. Whenever you do a git pull, also do: opam reinstall abella.

To uninstall Abella using OPAM, do:

  1. Run: opam remove abella.
  2. Then run: opam unpin abella.

More Information

Use the following walkthrough for an introduction to using Abella:

https://abella-prover.org/walkthrough.html

More information on Abella is available at

https://abella-prover.org/

Bugs, Feature Requests, and Issues

Please report all bugs, feature requests, and issues on the GitHub issue tracker for Abella, available from:

https://github.com/abella-prover/abella/issues

Discussion of Abella and its uses happens on this mailing list.

http://groups.google.com/group/abella-theorem-prover

interactive-theorem-proving
lambda-calculus
meta-theory

Contributors

agacek

883 commits

chaudhuri

417 commits

yvting

60 commits

robblanco

20 commits

Languages

OCaml

91.9%

Standard ML

3.1%

TypeScript

2.9%

Emacs Lisp

1.1%