Комментарии 7
Сегодня поговорим про общие теоретические аспекты формальной верификации, проблемы SAT и SMT и закрепим все это
Для последовательности изложения хорошо бы хотя бы дать хотя бы расшифровку аббревиатур. В идеале - краткое и емкое описание неизвестных терминов.
Можете сообщить стоимость вашего аудита марта?
Отправляйте запрос в форму в конце страницы, его передадут в нужные руки.
Или написать на почту web3@ptsecurity.com.
А в чем отличие инструмента формальной верификации от инвариантного тестирования, которое у Foundry из коробки? То есть, что дает инструмент формальной верификации в для аудита смарт-контракта, чего не может дать инвариантное тестирование с Foundry?
Инвариантное тестирование относится к фаззингу, а при формальной верификации инвариант разворачивается в математическое утверждение, которое затем доказывается. Это существенно влияет на глубину анализа: фаззинг, несмотря на свою эффективность, не может покрыть все возможные варианты состояний. Однако он всё равно может быть очень эффективным и иногда даже более эффективным, чем формальные методы.
Формальные методы проверки смарт-контрактов. Certora Prover