@VitalikButerin'in dediği gibi, güvenlik özelliklerinin resmi doğrulamasına ihtiyacımız var.

Ancak, Ethereum akıllı sözleşmeleri için resmi doğrulamayı ölçeklendirmek, EVM'nin belleği nasıl işlediği nedeniyle her zaman bir zorluk olmuştur; çünkü EVM, açık bir tahsisat olmaksızın tek bir büyük, monolitik dizi kullanır. Bu durum, SMT çözücülerinin bellekle ilgili karmaşık invariant'ları çıkarmasını gerektirdiği için zorluklar yaratmaktadır.

Peki, Certora bunu nasıl aştı? Hadi bunu inceleyelim 🧵👇