Команда Microsoft Azure Blockchain Services недавно объявила о своем новом решении VeriSol, основанном на технологии Blockchain.
VeriSol уже был интегрирован в собственное решение Microsoft для цепочки блоков, и теперь компания открыла сервис с открытым исходным кодом.
Verisol, сокращение от Verifier for Solidity — это инструмент формальной проверки с открытым исходным кодом, который был разработан для улучшения качества умных контрактов, написанных на подмножестве языка Solidity, с помощью цепочки инструментов проверки Boogie. Умные контракты — это программы, которые работают поверх блокчейна в качестве прозрачного уровня проверки.
К сожалению, из-за подвигов в смарт-контрактах клиенты теряют миллионы долларов в криптовалюте. Это значительно снижает доверие к технологиям блокчейна. Кроме того, умные контракты не легко управляются, особенно с точки зрения решения проблем.
VeriSol позволяет выполнять более быстрые итерации благодаря автоматической и непрерывной проверке, позволяя разработчикам гораздо быстрее обнаруживать ошибки, не беспокоясь о влиянии на клиентов.
В одном приложении группа VeriSol использовала верификатор для формализации и проверки спецификаций смарт-контрактов, которыми руководствуются члены консорциума в Ethereum в Azure и Azure Blockchain Service. Интеллектуальные контракты по управлению предназначены для эффективного управления членством в условиях консорциума, где, в отличие от общедоступных блокчейнов, бухгалтерская книга ограничена группой участников, которые осведомлены о личности других участников ».
Несмотря на то, что VeriSol все еще является прототипом, исследователи ставят перед собой высокие цели в отношении инструмента верификации и поощряют открытое сотрудничество, чтобы помочь добиться прогресса в формальной верификации для основной разработки умных контрактов.
