LLMs as verification oracles for Solidity

## Контекст Smart contracts — автоматизированные контракты, выполняющиеся в блокчейн-средах — широко используются в децентрализованных финансах, торговле и хранении активов. Однако, их корректность является критически важной, так как неточности в бизнес-логике могут привести к угадыванию финансовых потерь. Несмотря на наличие инструментов, нацеленных на обнаружение типичных уязвимостей, большинство реальных уязвимостей связаны с ошибками в бизнес-логике. Для решения этой проблемы используются формальные методы проверки, такие как SolCMC и Certora Prover. Однако, эти инструменты имеют высокую сложность в освоении и ограниченную языковую мощность. Недавние исследования показали, что бо LLM (большие языковые модели) могут успешно применяться в других областях безопасности, например, в обнаружении уязвимостей. В данной работе мы задаемся вопросом: могут ли бо быть использованы в качестве формальных оркестров, способных оценивать любые свойства конкретных контрактов? ## Метод Мы использовали GPT-5, современный бо LLM, для оценки его эффективности в качестве формального оркестра. Для этого, мы создали большую выборку задач формальной проверки контрактов Solidity. Каждая задача включала формальную спецификацию и код контракта. Мы сравнили выводы GPT-5 с результатами опытных формальных инструментов, а также проанализировали возможности GPT-5 в реальной среде аудита контрактов. Для оценки точности использовались как квантитативные метрики (например, доля правильных ответов), так и качественный анализ (качество доказательств и понятность выводов). ## Результаты Наши эксперименты показали, что GPT-5 демонстрирует очень высокую точность в выполнении задач проверки. Он успешно определил ошибки в бизнес-логике, даже в сложных случаях, где инструменты SolCMC и Certora Prover столкнулись с ограничениями. Бо LLM также продемонстрировал значительную выгоду в скорости обработки задач и понятности выводов. Однако, мы также обнаружили некоторые ограничения. Например, GPT-5 мог выдать некорректные ответы при неоднозначности спецификации или недостаточной качественности входных данных. ## Значимость Наша работа открывает новые возможности для использования бо в области формальной проверки смарт-контрактов. Использование LLMs может упростить процесс аудита и сделать его доступным для широкой аудитории, не имеющей технических навыков в формальных методах. Это открывает путь к более широкому применению формальных методов в блокчейн-индустрии. Будущие исследования будут направлены на улучшение точности и уменьшение ограничений GPT-5, а также на и