Формальная верификация смарт-контрактов на платформе Ethereum

Блокчейн называют самой прорывной областью на рубеже компьютер- ных, финансовых и юридических наук XXI века. У технологии насчи- тывается множество приложений, в том числе - умные контракты. Са- мым популярной платформой для проектирование и выполнения смарт- контрактов является Ethereum. Смарт-контракты можно использовать для самых разных целей, к примеру в системах по организации выбо- ров, разделении наследства, аренда недвижимости и торговля акциями. Другими словами их используют для обмена и передачи активов, сто- имость которых может достигать огромных значений. По этой причине последствия ошибки в умном контракте могут быть критическими. По этой причине проблема написания безопасного и эффективного контрак- та является трудоемкой и важной. В силу некоторых особенностей ар- хитектуры блокчейн систем, применение классического тестирования не подходит для отлаживания поведения умных контрактов. В данной ди- пломной работе мы поговорим об одном из подходов по доказательству корректности программ - формальной верификации, рассмотрим меха- низм работы технологии блокчейн в целом и проекта Ethereum, а также рассмотрим возможность применения формальной верификации к ум- ным контрактам на этой платформе. Ключевые слова: Формальная верификация, умный контракт, крип- товалюта, проверка моделей, Blockchain, Ethereum, Isabelle.