СПОСОБ ВЫПОЛНЕНИЯ СМАРТ-КОНТРАКТА В СИСТЕМЕ РАСПРЕДЕЛЕННОГО РЕЕСТРА

1. Способ повышения надежности системы распределенного реестра, содержащий:
составление смарт-контракта на предметно-ориентированном языке, для которого реализована формальная семантика на языке системы компьютерной логики HOL4;
осуществление трансляции смарт-контракта с предметно-ориентированного языка на язык HOL4;
осуществление верификации полученного смарт-контракта на языке HOL4 посредством обращения к блоку верификации программного обеспечения, связанного с библиотекой доказательств и тактик;
осуществление трансляции верифицированного смарт-контракта с языка HOL4 в абстрактное синтаксическое дерево функционального языка программирования CakeML;
осуществление передачи абстрактного синтаксического дерева смарт-контракта в компилятор языка CakeML для трансляции смарт-контракта в машинный код узла СРР, при этом верификацию процесса компиляции смарт-контракта осуществляют путем повторного использования предварительно формально-верифицированного компилятора языка CakeML;
осуществление передачи скомпилированного смарт-контракта в подсистему исполнения смарт-контрактов, подсистему сетевых взаимодействий и выполнение скомпилированного смарт-контракта в каждом узле системы распределенного реестра;
причем в основе реализации и функционирования узла СРР лежит формально-верифицированная операционная система seL4, а  узел СРР реализуется на языке CakeML, алгоритмы функционирования узла формально верифицируются с использованием системы компьютерной логики HOL4, машинный код узла СРР генерируется с использованием формально-верифицированного компилятора языка CakeML;
взаимодействие между узлом и остальными узлами СРР осуществляется посредством протокола консенсуса, верифицированного при помощи библиотеки доказательств и тактик в системе HOL4.
2. Способ повышения надежности системы распределенного реестра по п.1, отличающийся тем, что протокол консенсуса дополнительно верифицирован  при помощи метода Model checking.
3. Способ повышения надежности системы распределенного реестра по п.1, отличающийся тем, что взаимодействие узлов системы распределенного реестра с внешними системами и базами данных осуществляется через подсистему взаимодействия, реализованную на фреймворке Erlang/OTP.