I also like to explicately state in the prompt that, "the work is not complete until all Quint specifications pass 'quint verify'." If the model just uses "quint run" it still might miss issues.