Update README.md and features.md (#489)

* update the readme

* note about liveness

README.md

@@ -44,13 +44,20 @@ To try the latest cool features, check out the [unstable branch].
 - Consult the (WIP) [Idioms for writing better TLA+][idioms].
 - Consult the (WIP) [TLA+ language manual for engineers][language-manual].
 
+## Website
+
+[apalache.informal.systems][] is the main website of the project.
+
 ## Community
 
 - Join the chat in the [Apalache zulip stream].
 - [Contribute](./CONTRIBUTING.md) to the development of Apalache.
 
 ## Industrial examples
 
+- Check [Light client specs] and [Model-based testing] of the Tendermint
+  light client.
+
 - Check [Tendermint specs] to see how we use TLA+ and Apalache at Informal to
   design and specify protocols for the [Tendermint blockchain].
 
@@ -126,3 +133,6 @@ Our old website is still available at https://forsyte.at/research/apalache/ .
 [user-manual-docker]: https://apalache.informal.systems/docs/apalache/installation/docker.html
 [language-manual]: https://apalache.informal.systems/docs/lang/index.html
 [idioms]: https://apalache.informal.systems//docs/idiomatic/index.html
+[Light client specs]: https://github.com/tendermint/spec/tree/master/rust-spec/lightclient/verification
+[Model-based testing]: https://github.com/informalsystems/tendermint-rs/tree/master/light-client/tests/support/model_based#light-client-model-based-testing-guide
+[apalache.informal.systems]: https://apalache.informal.systems

docs/src/apalache/features.md

@@ -1,5 +1,13 @@
 Here is the list of the TLA+ language features that are currently supported by Apalache, following the [Summary of TLA+][cheat].
 
+## Safety vs. Liveness
+
+At the moment, Apalache is able to check invariants and inductive invariants.
+It means that you can only check safety with Apalache, unless you employ
+[liveness-to-safety] transformation in your spec. It does not support
+liveness properties.  If you really like to see liveness implemented, upvote
+the [liveness feature].
+
 ## Language
 
 ### Module-Level constructs
@@ -166,3 +174,6 @@ Not supported, not a priority
 
 
 [cheat]: https://lamport.azurewebsites.net/tla/summary.pdf
+[liveness-to-safety]: https://www.sciencedirect.com/science/article/pii/S1571066104804109?via%3Dihub
+[liveness feature]: https://github.com/informalsystems/apalache/issues/488
+