/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Primary LanguageScalaApache License 2.0Apache-2.0

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.

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/informalsystems/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.

Getting started

Website

Our current website is served at https://apalache.informal.systems .

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.

Our old website is still available at https://forsyte.at/research/apalache/ .

Community

Help wanted

Want to contribute? Here is a list of issues that could be solved without knowing too much about the internals of Apalache. Solving these issues would improve usability! Please comment in the relevant issue, if you are going to solve it.

  • Writing annotations in the JSON format: #804
  • Add support for VIEW in the TLC config: #851
  • Translate \E x \in STRING: P and \A x \in STRING: P: #844
  • Interval analysis for a..b: #446

Industrial examples

Talks

Performance

We are collecting apalache benchmarks. See the Apalache performance when checking inductive invariants and running bounded model checking. Versions 0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version reported at OOPSLA19).

Academic papers

To read an academic paper about the theory behind Apalache, check our paper at OOPSLA19. For the details of our novel encoding using SMT arrays, check our paper at TACAS23. Related reports and publications can be found at the Apalache page at TU Wien.


Apalache is developed at Informal Systems.

With additional funding from
the Vienna Business Agency.

Past funding from Der Wiener Wissenschafts-, Forschungs- und Technologiefonds.