diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md
index 9c2197170e..7687c50036 100644
--- a/tests/difference/core/quint_model/README.md
+++ b/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.