Quint looks like _exactly_ what I’ve been looking for. It’s all the good parts of TLA+, but with sensible types, and a focus on executability.

I understand that executability makes the language much less _powerful_ in a mathematical sense. But it’s such a benefit in all other ways that I think we should focus on the specification that we can write that are also executable.