Skip to content

apalache-mc/apalache

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Apalache Logo

A symbolic model checker for TLA+

main badge

Apalache translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3. Apalache can check inductive invariants (for fixed or bounded parameters) and check safety of bounded executions (bounded model checking). To see the list of supported TLA+ constructs, check the supported features. In general, Apalache runs under the same assumptions as TLC. However, Apalache benefits from constraint solving and can handle potentially larger state-spaces, e.g., involving integer clocks and Byzantine faults.

To learn more about TLA+, visit Leslie Lamport's page on TLA+ and his Video course.

Releases

Check the releases page for our latest release.

For a stable release, we recommend that you pull the latest docker image with docker pull ghcr.io/apalache-mc/apalache:main, use the jar from the most recent release, or checkout the source code from the most recent release tag.

To try the latest cool features, check out the head of the main branch.

You can also find Apalache packaged via Nix at cosmos.nix

For more information on installation options, see the manual.

Success stories

Check Apalache examples that demonstrate how to use the strengths of Apalache. Also, check the standard repository of TLA+ examples.

Getting started

Community

Funding and Sponsorship

Currently, Apalache is not funded by any organization. As a result, it is de-facto funded by its current maintainers and contributors, including Igor Konnov, Jure Kukovec, and Thomas Pani. If you would like to sponsor the project, please contact us, or simply sponsor us on GitHub by clicking the "Sponsor" button!

Reloading Apalache

We are grateful for the past financial support in the form of grants or employment from the following organizations:

More details on the Funding page.

Website

Our current website is served at https://apalache-mc.org .

The site is hosted by github, and changes can be made through PRs into the gh-pages branch of this repository. See the README.md on that branch for more information.

The user documentation is automatically deployed to the website branch as per the CI configuration.