Thread by @informalinc

1/ Apalache is Informal’s symbolic checker for #tlaplus that checks your specifications by solving constraints instead of enumerating states. informal.systems/2021/03/08/apa…

2/ How does it work? Apalache translates TLA+ specs using SMT solvers to reason about states & transitions in terms of logic, rather than in terms of individual states & transitions. apalache.informal.systems

3/ Our main goal has been to improve the usability of the model checker by testing the tool with internal customers, which saw 3 issues come up consistently:
- How do I write TLA+?
- Why is Apalache complaining about types?
- Why is Apalache complaining about assignments?

4/ We recognize that learning TLA+ can produce confusion for newcomers and complicate the on-boarding process which is why we’ve started to write a new TLA+ manual for engineers and collect TLA+ idioms. apalache.informal.systems/docs/lang/inde…

5/ The old type checker hid type inference and types from users which produced challenges for tools that use SMT and for users who want types as an independent analysis tool. We developed Snowcat which is a new type checker for TLA+.

6/ Snowcat is a new approach to type annotations that helps systems engineers write type annotations and quickly check types when writing TLA+ specifications. Our goal is to completely automate type inference for TLA+. apalache.informal.systems//docs/apalache…

7/ TLA+ does not have assignments by design since the user focuses on logical constraints versus statements. The new version of Apalache uses TLC to find assignments statically which improves understanding of error messages. Discover assignments here! apalache.informal.systems/docs/apalache/…

8/ We are preparing for the first Alpha release of Apalache dubbed Alpha Centauri which will introduce stability to the tool. Track our progress here: github.com/informalsystem…

9/ If you are new to TLA+, check out our TLA+ manual for engineers apalache.informal.systems/docs/lang/inde…

10/ Lastly, don’t hesitate to take @ApalacheTLA for a spin and let us know what you think! informal-systems.zulipchat.com/login/#narrow/… /end