Как говорит @VitalikButerin, нам необходима формальная верификация свойств безопасности.
Однако масштабирование формальной верификации для смарт-контрактов Ethereum всегда было проблемой из-за особенностей работы EVM с памятью — это один большой, монолитный массив без явного выделения. Это создает трудности для SMT-солверов, так как им приходится выводить сложные инварианты о памяти.
Итак, как же Certora справилась с этой задачей? Давайте разберем подробнее 🧵👇