@VitalikButerinが言うように、私たちはセキュリティ特性の形式的検証が必要です。

しかし、Ethereumスマートコントラクトの形式的検証をスケーリングすることは、EVMがメモリをどのように扱うかのために常に課題でした—明示的な割り当てがない大きな単一配列です。これは、ソルバーがメモリに関する複雑な不変量を推測する必要があるため、SMTソルバーにとって困難をもたらします。

では、Certoraはこれをどのように克服したのでしょうか？詳しく見ていきましょう🧵👇