正如 @VitalikButerin 所說，我們需要對安全屬性進行形式驗證。

但是，由於 EVM 對內存的處理方式——一個大型的單一數組，沒有明確的分配，擴展以太坊智能合約的形式驗證一直是一個挑戰。這給 SMT 求解器帶來了困難，因爲這要求求解器推斷出關於內存的複雜不變性。

那麼，Certora 是如何解決這個問題的呢？讓我們來詳細分析一下 🧵👇