Add model checking to README

tests/difference/core/quint_model/README.md

@@ -50,6 +50,12 @@ with a timestamp >= t + UnbondingPeriod on that consumer.
 - [X] EventuallyMatureOnProviderInv: If we send a VSCPacket, this is eventually responded to by all consumers
 that were running at the time the packet was sent (and are still running).
 
+Invariants can also be model-checked by Apalache, using this command:
+```
+quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv --main CCVDefaultState
+Machine ccv_statemachine.qnt
+```
+
 ### Sanity Checks
 
 Sanity checks verify that certain patterns of behaviour can appear in the model.