Unsupported TLA+ features

Poorly Supported TLA+ Features

While the following features are supported, the back-end provers do not provide much automatic proving and require a lot of guidance.

Known Limitations and Problems

The following limitations and problems of TLAPS and its backends are known to us and will hopefully be removed in a future version. We welcome your feedback on problems that you encounter. Why not subscribe to the Google TLA+ group where such issues are discussed?