Nelle ultime settimane, @dnkolegov (e il team di @asymmetric_re) hanno tradotto Minimmit in una specifica eseguibile (scritta in Quint). Perché? Ora possiamo automatizzare la ricerca dell'inadeguatezza di Minimmit rispetto al controllore 🤖 del modello simbolico Apalache.