在过去几周中，@dnkolegov（以及@asymmetric_re团队）将Minimmit翻译成了可执行规范（用Quint编写）。 为什么？我们现在可以自动化搜索Minimmit的不健全性，以便与Apalache符号模型检查器进行对比 🤖。