Comment by mavelikara

Everything that can be expressed in TLA+ can’t be expressed in Quint. But everything useful for specifying programs, I believe, can be expressed in both languages.