Применение Certora Prover для формальной верификации смарт-контрактов: методология и кейс-стади

В докладе представлен опыт нашей команды в применении методов формальной верификации с акцентом на использование Certora Prover — передового инструмента для полуавтоматического анализа и повышения безопасности смарт-контрактов. Мы детально рассмотрим ключевые функции и преимущества Certora Prover, методологию верификации и поделимся практическими результатами его применения на примере реальных смарт-контрактов. Особое внимание будет уделено выявлению и устранению потенциальных уязвимостей с акцентом на важность формальной верификации для укрепления доверия к блокчейн-технологиям — как в финансовом секторе, так и за его пределами. Сергей Соболев Positive Technologies