{"id":443219,"date":"2024-12-26T06:25:21","date_gmt":"2024-12-26T06:25:21","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=443219"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=443219","title":{"rendered":"<span>\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 IBFT: \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u043e\u0433\u043e \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435<\/span>"},"content":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/ddd\/82d\/bce\/ddd82dbcee7a5cf54cb626f7aaea7676.JPG\" width=\"2428\" height=\"1368\"\/><\/figure>\n<p>\u0414\u043e\u0431\u0440\u044b\u0439 \u0434\u0435\u043d\u044c! \u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u041a\u0438\u0440\u0438\u043b\u043b \u0417\u0438\u0431\u043e\u0440\u043e\u0432, \u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u044e \u043e\u0442\u0434\u0435\u043b \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c Positive Technologies. \u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0443 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0434\u043b\u044f \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0449\u0435\u043d\u0438\u044f \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439 \u0432 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043a\u043e\u043c\u043f\u043e\u043d\u0435\u043d\u0442\u0430\u0445 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430. \u0420\u0430\u043d\u0435\u0435 <a href=\"https:\/\/habr.com\/en\/companies\/pt\/articles\/804861\/\">\u043c\u044b \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c \u043c\u0435\u0442\u043e\u0434\u043e\u043c<\/a>. \u0412 \u044d\u0442\u043e\u0442 \u0440\u0430\u0437 \u0440\u0435\u0447\u044c \u043f\u043e\u0439\u0434\u0435\u0442 \u043e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430\u0445 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u2014 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u0430\u0445 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f \u0443\u0437\u043b\u0430\u043c\u0438 \u043d\u043e\u0432\u044b\u0445 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439 \u0432 \u0446\u0435\u043f\u043e\u0447\u043a\u0443, \u0430 \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u0431 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 Istanbul Byzantine Fault Tolerant \u0438 \u0432 \u0446\u0435\u043b\u043e\u043c \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u0435\u0442\u043e\u0434\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439.\u00a0<\/p>\n<h2>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430<\/h2>\n<p>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u2014 \u043e\u0434\u043d\u0430 \u0438\u0437 \u0444\u0443\u043d\u0434\u0430\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0430\u0441\u0442\u0435\u0439 \u043b\u044e\u0431\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044e\u0449\u0430\u044f \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c \u0438 \u0446\u0435\u043b\u043e\u0441\u0442\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u043e\u0433\u043e \u0440\u0435\u0435\u0441\u0442\u0440\u0430 \u0431\u0435\u0437 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e\u0441\u0442\u0438 \u0432 \u0446\u0435\u043d\u0442\u0440\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438. \u0422\u0430\u043a\u043e\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u0443 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432 \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442\u044c \u043a \u0441\u043e\u0433\u043b\u0430\u0441\u0438\u044e \u043e \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044f \u043d\u0435\u0438\u0437\u043c\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u0438 \u043f\u0440\u043e\u0437\u0440\u0430\u0447\u043d\u043e\u0441\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0445 \u0434\u0430\u0436\u0435 \u0432 \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u0445 \u043f\u043e\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e \u043d\u0435\u043d\u0430\u0434\u0435\u0436\u043d\u043e\u0439 \u0438\u043b\u0438 \u0437\u043b\u043e\u043d\u0430\u043c\u0435\u0440\u0435\u043d\u043d\u043e\u0439 \u0441\u0440\u0435\u0434\u044b, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043a\u0430\u0436\u0434\u044b\u0439 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a \u043c\u043e\u0436\u0435\u0442 \u0434\u0435\u0439\u0441\u0442\u0432\u043e\u0432\u0430\u0442\u044c \u0432 \u043f\u0435\u0440\u0432\u0443\u044e \u043e\u0447\u0435\u0440\u0435\u0434\u044c \u0438\u0441\u0445\u043e\u0434\u044f \u0438\u0437 \u043c\u0430\u043a\u0441\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0439 \u0432\u044b\u0433\u043e\u0434\u044b.<\/p>\n<p>\u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0440\u0430\u0437\u043d\u043e\u0432\u0438\u0434\u043d\u043e\u0441\u0442\u0435\u0439 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u044b\u0445 \u0434\u043b\u044f \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u0435\u043d\u0438\u044f \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u0439 \u043a \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438, \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0438 \u043c\u0430\u0441\u0448\u0442\u0430\u0431\u0438\u0440\u0443\u0435\u043c\u043e\u0441\u0442\u0438 \u0441\u0435\u0442\u0438. \u041d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b\u0435 \u0438\u0437 \u043d\u0438\u0445 \u2014 Proof of Work (PoW), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0432 Bitcoin, \u0433\u0434\u0435 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0438 \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u043c\u043e\u0449\u043d\u043e\u0441\u0442\u0438 \u0434\u043b\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0441\u043b\u043e\u0436\u043d\u044b\u0445 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0437\u0430\u0434\u0430\u0447 \u0434\u043b\u044f \u043f\u043e\u0434\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u0438 Proof of Stake (PoS), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0441\u0435\u0439\u0447\u0430\u0441 \u0432 Ethereum (\u0440\u0430\u043d\u0435\u0435 \u0442\u0430\u043c \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0441\u044f PoW), \u0433\u0434\u0435 \u043f\u0440\u0430\u0432\u043e \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u043d\u043e\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0430 \u0432\u044b\u0434\u0430\u0435\u0442\u0441\u044f \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0443 \u0441 \u043d\u0430\u0438\u0431\u043e\u043b\u044c\u0448\u0438\u043c \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e\u043c \u043d\u0430\u0442\u0438\u0432\u043d\u044b\u0445 \u0442\u043e\u043a\u0435\u043d\u043e\u0432.\u00a0<\/p>\n<p>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u044b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0437\u0434\u0435\u043b\u0438\u0442\u044c \u043d\u0430 \u0434\u0432\u0435 \u0433\u0440\u0443\u043f\u043f\u044b \u043f\u043e \u0442\u0438\u043f\u0443 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u0441\u0435\u0442\u0438, \u043a \u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043e\u043d\u0438 \u0443\u0441\u0442\u043e\u0439\u0447\u0438\u0432\u044b. \u041d\u0435\u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0435 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432\u043e\u0437\u043d\u0438\u043a\u0430\u044e\u0442, \u043a\u043e\u0433\u0434\u0430 \u0443\u0437\u043b\u044b \u0432\u044b\u0445\u043e\u0434\u044f\u0442 \u0438\u0437 \u0441\u0442\u0440\u043e\u044f \u0438\u0437-\u0437\u0430 \u0430\u043f\u043f\u0430\u0440\u0430\u0442\u043d\u044b\u0445 \u0441\u0431\u043e\u0435\u0432 \u0438\u043b\u0438 \u0441\u0435\u0442\u0435\u0432\u044b\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c, \u043d\u043e \u043d\u0435 \u0432\u0435\u0434\u0443\u0442 \u0441\u0435\u0431\u044f \u0437\u043b\u043e\u043d\u0430\u043c\u0435\u0440\u0435\u043d\u043d\u043e. \u0412\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0435 \u043e\u0448\u0438\u0431\u043a\u0438, \u0441 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u044e\u0442 \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0432\u0440\u0435\u0434\u043e\u043d\u043e\u0441\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u043e \u0438\u043b\u0438 \u0443\u043c\u044b\u0448\u043b\u0435\u043d\u043d\u043e \u0432\u0440\u0435\u0434\u0438\u0442\u044c \u0441\u0435\u0442\u0438, \u043f\u0435\u0440\u0435\u0434\u0430\u0432\u0430\u044f \u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0440\u0435\u0447\u0438\u0432\u0443\u044e \u0438\u043b\u0438 \u043b\u043e\u0436\u043d\u0443\u044e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e. \u041b\u0435\u0441\u043b\u0438 \u041b\u044d\u043c\u043f\u043e\u0440\u0442 \u0438 \u0420\u043e\u0431\u0435\u0440\u0442 \u0428\u043e\u0441\u0442\u0430\u043a <a href=\"https:\/\/lamport.azurewebsites.net\/pubs\/reaching.pdf\">\u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438<\/a>, \u0447\u0442\u043e \u0434\u043b\u044f \u0434\u043e\u0441\u0442\u0438\u0436\u0435\u043d\u0438\u044f \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0441 <em>N<\/em> \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0445 \u0443\u0437\u043b\u043e\u0432 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u0430\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u0434\u043e\u043b\u0436\u043d\u0430 \u0441\u043e\u0441\u0442\u043e\u044f\u0442\u044c \u043a\u0430\u043a \u043c\u0438\u043d\u0438\u043c\u0443\u043c \u0438\u0437 <em>3N\u202f+\u202f1<\/em> \u0443\u0437\u043b\u043e\u0432 \u0438 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0430\u0442\u044c \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0443\u0441\u0442\u043e\u0439\u0447\u0438\u0432\u044b\u0439 \u043a \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c \u043e\u0448\u0438\u0431\u043a\u0430\u043c (Byzantine Fault Tolerant, BFT).<\/p>\n<p>\u0420\u043e\u043b\u044c \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430\u0445 \u043a\u0440\u0438\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0432\u0430\u0436\u043d\u0430 \u0434\u043b\u044f \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0438 \u0434\u0435\u0446\u0435\u043d\u0442\u0440\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u0435\u0442\u0438. \u0412\u044b\u0431\u043e\u0440 \u043d\u0435\u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0441\u0435\u0442\u0435\u0432\u044b\u043c \u0440\u0430\u0437\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u043c, \u043f\u0440\u0438 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0440\u0430\u0437\u043d\u044b\u0435 \u0443\u0437\u043b\u044b \u0431\u0443\u0434\u0443\u0442 \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0440\u0430\u0437\u043d\u044b\u0435 \u0446\u0435\u043f\u043e\u0447\u043a\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u0438\u043b\u0438 \u043a \u043f\u043e\u043b\u043d\u043e\u0439 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435 \u0441\u0435\u0442\u0438. \u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432 \u0430\u0442\u0430\u043a \u043d\u0430 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u044b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u0421\u0430\u043c\u0430\u044f \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u0430\u044f \u0438\u0437 \u043d\u0438\u0445 \u2014 <a href=\"https:\/\/academy.binance.com\/ru\/glossary\/51-percent-attack\">\u0430\u0442\u0430\u043a\u0430 51%<\/a> \u043d\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u044b PoW, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0449\u0430\u044f \u0437\u043b\u043e\u0443\u043c\u044b\u0448\u043b\u0435\u043d\u043d\u0438\u043a\u0443 \u0441 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0439 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u043c\u043e\u0449\u043d\u043e\u0441\u0442\u044c\u044e \u043a\u043e\u043d\u0442\u0440\u043e\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u0435\u0442\u044c \u0438 \u0441\u043e\u0432\u0435\u0440\u0448\u0430\u0442\u044c \u0434\u0432\u043e\u0439\u043d\u044b\u0435 \u0442\u0440\u0430\u0442\u044b.\u00a0<\/p>\n<h2>\u041a\u0430\u043a \u043e\u0431\u0435\u0437\u043e\u043f\u0430\u0441\u0438\u0442\u044c \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d \u043e\u0442 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0435<\/h2>\n<p><a href=\"https:\/\/habr.com\/en\/companies\/pt\/articles\/804861\/\">\u041a\u0430\u043a \u043c\u044b \u0443\u0436\u0435 \u0437\u043d\u0430\u0435\u043c<\/a>, \u043c\u0435\u0442\u043e\u0434\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u044b \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u041e\u043d\u0438 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u044b \u0438 \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044f \u0438\u0445 \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0441\u0442\u043e\u044f\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u043c \u0442\u0438\u043f\u0430\u043c \u0430\u0442\u0430\u043a \u0438 \u043e\u0442\u043a\u0430\u0437\u043e\u0432.<\/p>\n<p>\u0412 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u043b \u0434\u0432\u0430 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u043f\u043e\u0434\u0445\u043e\u0434\u0430 \u043a \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c: \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u0443\u044e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e \u0438 model checking. \u0414\u043b\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u0430 \u044d\u0442\u0438\u0445 \u043c\u0435\u0442\u043e\u0434\u0430, \u043e\u0434\u043d\u0430\u043a\u043e \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u0435\u043d \u043c\u0435\u0442\u043e\u0434 model checking. \u042d\u0442\u043e \u0441\u0432\u044f\u0437\u0430\u043d\u043e \u0441 \u0442\u0435\u043c, \u0447\u0442\u043e \u043e\u0431\u044b\u0447\u043d\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043f\u0440\u0435\u0437\u0435\u043d\u0442\u0443\u0435\u0442\u0441\u044f \u0432 \u0430\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043d\u0430 \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0438\u043b\u0438 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0430, \u0438 \u0443\u0436\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u044d\u0442\u0438\u0445 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0440\u0435\u0430\u043b\u0438\u0437\u0443\u0435\u0442\u0441\u044f \u043d\u0430 \u0432\u044b\u0431\u0440\u0430\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f.\u00a0<\/p>\n<p>\u041c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0434\u043e\u0431\u043d\u043e \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0442\u044c \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0430, \u0430 \u0432\u044b\u0440\u0430\u0437\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u044f\u0437\u044b\u043a\u043e\u0432 \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0438 \u043e\u0431\u044b\u0447\u043d\u043e \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0434\u043b\u044f \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u0438\u044f \u0442\u0430\u043a\u0438\u0445 \u043c\u043e\u0434\u0435\u043b\u0435\u0439. \u041e\u0434\u043d\u0430\u043a\u043e \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0442\u043e\u0436\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u041e\u0434\u0438\u043d \u0438\u0437 \u0443\u0441\u043f\u0435\u0448\u043d\u044b\u0445 \u043a\u0435\u0439\u0441\u043e\u0432 \u2014 \u044d\u0442\u043e <a href=\"https:\/\/github.com\/uwplse\/verdi-raft\">\u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 Raft \u0432\u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435 Verdi<\/a>, \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0432 Coq.\u00a0<\/p>\n<h2>TLA+<\/h2>\n<p>\u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u044e\u0441\u044c \u043d\u0430 \u043c\u0435\u0442\u043e\u0434\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0438 \u0431\u0443\u0434\u0443 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u044f\u0437\u044b\u043a TLA+ \u0432\u043c\u0435\u0441\u0442\u0435 \u0441 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0438 TLC. TLA+ \u2014 \u044d\u0442\u043e \u044f\u0437\u044b\u043a \u0434\u043b\u044f \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c \u0438 \u043f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432. \u041e\u043d \u043e\u0441\u043d\u043e\u0432\u0430\u043d \u043d\u0430 \u0442\u0435\u043e\u0440\u0438\u0438 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432, \u043b\u043e\u0433\u0438\u043a\u0435 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u0438 \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u043e\u0439 \u043b\u043e\u0433\u0438\u043a\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439 (TLA, temporal logic of actions). \u041f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0435 \u043d\u0430 TLA+, \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u043c \u043a\u0430\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043d\u0430 \u043e\u0431\u044b\u0447\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f: \u043e\u043d\u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u044e\u0442\u0441\u044f \u0447\u0435\u0440\u0435\u0437 \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439. \u0421\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 (model checker) \u2014 \u044d\u0442\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u044b. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0437\u0430\u0434\u0430\u0435\u0442 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e, \u0430 model checker \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442, \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u044b \u043b\u0438 \u043e\u043d\u0438 \u0434\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0438 \u0438\u043b\u0438 \u043d\u0435\u0442. \u0412 \u0441\u043b\u0443\u0447\u0430\u0435 \u0435\u0441\u043b\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f, \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u0438\u0442 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440.<\/p>\n<p>\u041c\u043e\u0434\u0435\u043b\u044c \u0432 TLA+ \u2014 \u044d\u0442\u043e<strong> <\/strong>\u043d\u0430\u0431\u043e\u0440 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0438 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u044d\u0442\u0438\u043c\u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0437\u0430\u0434\u0430\u044e\u0442\u0441\u044f \u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432 \u0438 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439. \u041c\u043e\u0434\u0435\u043b\u044c \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0441\u0438\u0441\u0442\u0435\u043c\u044b \u043a\u0430\u043a \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439, \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0449\u0438\u0445 \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c \u0438 \u0438\u0437\u043c\u0435\u043d\u044f\u044e\u0449\u0438\u0445\u0441\u044f \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439. \u0414\u043b\u044f \u0442\u043e\u0433\u043e \u0447\u0442\u043e\u0431\u044b \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u043d\u0430 TLA+, \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0437\u0430\u0434\u0430\u0442\u044c \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0438 \u0441\u0438\u0441\u0442\u0435\u043c\u0443 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432. \u041f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u043c\u043e\u0436\u043d\u043e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0432 \u044d\u0442\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432 \u0438 \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0432 model checker.<\/p>\n<p>\u0421 \u043f\u043e\u043c\u043e\u0449\u044c\u044e TLA+ \u0431\u044b\u043b\u043e \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u043e \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043e \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430: <a href=\"https:\/\/github.com\/tlaplus\/Examples\/tree\/master\/specifications\/Paxos\">Paxos<\/a>, <a href=\"https:\/\/github.com\/ongardie\/raft.tla\/blob\/master\/raft.tla\">Raft<\/a>, <a href=\"https:\/\/arxiv.org\/pdf\/1807.04938\">Tendermint<\/a>, <a href=\"https:\/\/www.mais-journal.ru\/jour\/article\/view\/1436\/1091\">HotStuff<\/a> \u0438 \u0434\u0440\u0443\u0433\u0438\u0435.<\/p>\n<h2>\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c IBFT<\/h2>\n<p><a href=\"https:\/\/pmg.csail.mit.edu\/papers\/osdi99.pdf\">\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c Practical Byzantine Fault Tolerant (pBFT)<\/a> \u0431\u044b\u043b \u043f\u0435\u0440\u0432\u044b\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u043c, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044e\u0449\u0438\u043c \u0434\u043e\u0441\u0442\u0438\u0436\u0435\u043d\u0438\u0435 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0447\u0430\u0441\u0442\u0438\u0447\u043d\u043e \u0441\u0438\u043d\u0445\u0440\u043e\u043d\u043d\u044b\u0445 \u0441\u0435\u0442\u044f\u0445 \u0441 \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c\u0438 \u043e\u0448\u0438\u0431\u043a\u0430\u043c\u0438, \u0433\u0434\u0435 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c \u043d\u0435 \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u042d\u0442\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u0438\u043b\u0430 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432, \u0443\u043b\u0443\u0447\u0448\u0430\u044e\u0449\u0438\u0445 \u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u044f\u044e\u0449\u0438\u0445 pBFT, \u0441\u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 \u043e\u0434\u043d\u043e\u0439 \u0438 \u0442\u043e\u0439 \u0436\u0435 <a href=\"https:\/\/groups.csail.mit.edu\/tds\/papers\/Lynch\/jacm88.pdf\">\u0447\u0430\u0441\u0442\u0438\u0447\u043d\u043e \u0441\u0438\u043d\u0445\u0440\u043e\u043d\u043d\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0438<\/a>, \u0433\u0434\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0432 \u0442\u0435\u0447\u0435\u043d\u0438\u0435 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/42a\/300\/9c5\/42a3009c5babff14d2e5d61bd20b8cb6.png\" alt=\"\u0420\u0438\u0441\u0443\u043d\u043e\u043a 1. \u0420\u0430\u0431\u043e\u0442\u0430 pBFT\" title=\"\u0420\u0438\u0441\u0443\u043d\u043e\u043a 1. \u0420\u0430\u0431\u043e\u0442\u0430 pBFT\" width=\"552\" height=\"413\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/42a\/300\/9c5\/42a3009c5babff14d2e5d61bd20b8cb6.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441\u0443\u043d\u043e\u043a 1. \u0420\u0430\u0431\u043e\u0442\u0430 pBFT<\/figcaption><\/div>\n<\/figure>\n<p>\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c IBFT (Istanbul Byzantine Fault Tolerant) \u0442\u0430\u043a\u0436\u0435 \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u043b\u0435\u043d pBFT \u0438 \u0431\u044b\u043b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 <a href=\"https:\/\/github.com\/ethereum\/EIPs\/issues\/650\">EIP650<\/a> (Ethereum Improvement Proposals). \u0421\u043e\u0437\u0434\u0430\u043d\u0438\u0435 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0431\u044b\u043b\u043e \u043c\u043e\u0442\u0438\u0432\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u0442\u0435\u043c, \u0447\u0442\u043e pBFT \u0432 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u043c \u0432\u0438\u0434\u0435 \u043d\u0435 \u043f\u043e\u0434\u0445\u043e\u0434\u0438\u0442 \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0441\u0435\u0442\u044f\u0445. \u042d\u0442\u043e \u0441\u0432\u044f\u0437\u0430\u043d\u043e \u043f\u043e\u043f\u0440\u043e\u0441\u0442\u0443 \u0441 \u0442\u0435\u043c, \u0447\u0442\u043e \u043e\u043d \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u043b\u0441\u044f \u0432 \u0434\u0430\u043b\u0435\u043a\u043e\u043c 1999 \u0433\u043e\u0434\u0443, \u0437\u0430 10 \u043b\u0435\u0442 \u0434\u043e \u043f\u043e\u044f\u0432\u043b\u0435\u043d\u0438\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430 Bitcoin. \u0412 pBFT, \u043a\u0430\u043a \u0432\u0438\u0434\u043d\u043e \u0438\u0437 \u0435\u0433\u043e \u0441\u0445\u0435\u043c\u044b, \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u0442\u0441\u044f \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u00ab\u043a\u043b\u0438\u0435\u043d\u0442\u0430\u00bb, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0437\u0430\u043f\u0440\u043e\u0441\u044b \u0438 \u0436\u0434\u0435\u0442 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432. \u041e\u0434\u043d\u0430\u043a\u043e \u0432 \u043a\u043e\u043d\u0442\u0435\u043a\u0441\u0442\u0435 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430 \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u0432\u0441\u0435\u0445 \u0432\u0430\u043b\u0438\u0434\u0430\u0442\u043e\u0440\u043e\u0432 \u043a\u0430\u043a \u00ab\u043a\u043b\u0438\u0435\u043d\u0442\u043e\u0432\u00bb. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0446\u0435\u043f\u043e\u0447\u043a\u0430 \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0438\u0440\u043e\u0432\u0430\u043b\u0430, \u0432 \u043a\u0430\u0436\u0434\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435 \u0434\u043e\u043b\u0436\u0435\u043d \u043f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u043e \u0432\u044b\u0431\u0438\u0440\u0430\u0442\u044c\u0441\u044f \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u0442\u044c \u0431\u043b\u043e\u043a-\u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u0422\u0430\u043a\u0436\u0435 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u0440\u0430\u0431\u043e\u0442\u044b \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u0433\u043e pBFT \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 \u0447\u0442\u0435\u043d\u0438\u044f \u0438 \u0437\u0430\u043f\u0438\u0441\u0438 \u0432 \u0444\u0430\u0439\u043b\u043e\u0432\u043e\u0439 \u0441\u0438\u0441\u0442\u0435\u043c\u0435, \u0430 \u043e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435 \u043c\u044b \u043e\u0436\u0438\u0434\u0430\u0435\u043c \u0432\u044b\u0431\u043e\u0440 \u043d\u043e\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0430 \u0434\u043b\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0432 \u0446\u0435\u043f\u043e\u0447\u043a\u0443.<\/p>\n<p>IBFT \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0441\u0435\u0442\u044f\u0445 \u0441 \u0440\u0430\u0437\u0440\u0435\u0448\u0435\u043d\u0438\u044f\u043c\u0438 (permissioned blockchains), \u0433\u0434\u0435 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0438 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b \u0438 \u0438\u0434\u0435\u043d\u0442\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u044b. \u041e\u043d \u0431\u044b\u043b \u043f\u0435\u0440\u0432\u043e\u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d \u043a\u0430\u043a \u0447\u0430\u0441\u0442\u044c \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c\u044b Quorum, \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u043e\u0439 \u043a\u043e\u043c\u043f\u0430\u043d\u0438\u0435\u0439 JPMorgan Chase. \u041e\u0434\u043d\u0430\u043a\u043e \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u043e\u0448\u0435\u043b \u0434\u043e\u043b\u0433\u0438\u0439 \u043f\u0443\u0442\u044c \u0447\u0435\u0440\u0435\u0437 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0434\u043e\u0440\u0430\u0431\u043e\u0442\u043e\u043a \u043f\u0435\u0440\u0435\u0434 \u043f\u043e\u043b\u043d\u043e\u0446\u0435\u043d\u043d\u044b\u043c \u0432\u043d\u0435\u0434\u0440\u0435\u043d\u0438\u0435\u043c \u0432 Quorum.<\/p>\n<p>\u041f\u0435\u0440\u0432\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u044f IBFT \u043d\u0435 \u0432\u0441\u0435\u0433\u0434\u0430 \u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e: \u0434\u0432\u0430 \u0447\u0435\u0441\u0442\u043d\u044b\u0445 \u0443\u0437\u043b\u0430 \u043c\u043e\u0433\u043b\u0438 \u0432\u044b\u0431\u0440\u0430\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f. \u0412 \u043e\u0431\u043d\u043e\u0432\u043b\u0435\u043d\u043d\u043e\u043c \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0435 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0431\u044b\u043b\u0438 \u0440\u0435\u0448\u0435\u043d\u044b, \u043d\u043e \u043f\u043e\u044f\u0432\u0438\u043b\u0438\u0441\u044c <a href=\"https:\/\/github.com\/jpmorganchase\/quorum\/issues\/305\">\u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0441 \u0436\u0438\u0432\u0443\u0447\u0435\u0441\u0442\u044c\u044e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430<\/a>: \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043c\u043e\u0433\u043b\u0438 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0432\u0437\u0430\u0438\u043c\u043d\u043e\u043c\u0443 \u043e\u0436\u0438\u0434\u0430\u043d\u0438\u044e \u0438 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435 (deadlock). \u0412 \u043e\u0442\u0432\u0435\u0442 \u043d\u0430 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0431\u044b\u043b\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043e \u0434\u0432\u0430 \u0440\u0435\u0448\u0435\u043d\u0438\u044f. <a href=\"https:\/\/arxiv.org\/pdf\/1901.07160\">\u041f\u0435\u0440\u0432\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435<\/a> \u2014 \u0438\u0437\u0431\u0430\u0432\u0438\u0442\u044c\u0441\u044f \u043e\u0442 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u0430 \u0431\u043b\u043e\u043a\u0438\u0440\u043e\u0432\u043a\u0438 \u0443\u0437\u043b\u043e\u0432 \u0438 \u0434\u043e\u0431\u0430\u0432\u0438\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u043e\u0432, \u043f\u043e\u0445\u043e\u0436\u0438\u0439 \u043d\u0430 \u0442\u043e\u0442, \u0447\u0442\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0432 pBFT. \u0412\u0442\u043e\u0440\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0431\u044b\u043b\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043e \u043a\u0430\u043a \u0440\u0430\u0437 \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 \u0440\u0430\u0431\u043e\u0442\u044b \u043d\u0430\u0434 Quorum, \u0438 \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u0431 \u044d\u0442\u043e\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043f\u043e\u0439\u0434\u0435\u0442 \u0440\u0435\u0447\u044c \u0434\u0430\u043b\u0435\u0435.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w780q1\/getpro\/habr\/upload_files\/042\/c1a\/2e8\/042c1a2e8731852ad4fca78cfd729566.jpeg\" alt=\"https:\/\/user-images.githubusercontent.com\/1516485\/41951806-4824998c-79ff-11e8-99f0-153fca7708a4.jpg\" title=\"\u0420\u0438\u0441\u0443\u043d\u043e\u043a 2. \u0420\u0430\u0431\u043e\u0442\u0430 IBFT\" width=\"1600\" height=\"1055\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/042\/c1a\/2e8\/042c1a2e8731852ad4fca78cfd729566.jpeg\" data-blurred=\"true\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441\u0443\u043d\u043e\u043a 2. <a href=\"https:\/\/github.com\/ethereum\/EIPs\/issues\/650\">\u0420\u0430\u0431\u043e\u0442\u0430 IBFT<\/a><\/figcaption><\/div>\n<\/figure>\n<h2>\u041c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 IBFT \u043d\u0430 TLA+<\/h2>\n<p>\u041a\u0430\u043a \u044f \u0443\u0436\u0435 \u043e\u0442\u043c\u0435\u0442\u0438\u043b, \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0434\u043e\u0431\u043d\u043e \u0441\u0442\u0440\u043e\u0438\u0442\u044c \u043f\u043e \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0443 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u0418\u043c\u0435\u043d\u043d\u043e \u0442\u0430\u043a\u043e\u0439 \u043f\u043e\u0434\u0445\u043e\u0434 \u044f \u0438\u0437\u0431\u0440\u0430\u043b \u0434\u043b\u044f IBFT, \u0432\u0437\u044f\u0432 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 <a href=\"https:\/\/arxiv.org\/pdf\/2002.03613\">\u0438\u0437 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0439 \u043f\u0443\u0431\u043b\u0438\u043a\u0430\u0446\u0438\u0438 Quorum \u043e\u0431 \u044d\u0442\u043e\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435<\/a>.\u00a0<\/p>\n<p>\u041a\u0430\u0436\u0434\u044b\u0439 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u0442 \u043f\u043e \u0440\u0430\u0443\u043d\u0434\u0430\u043c. \u0412 \u043a\u0430\u0436\u0434\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435 \u043e\u0434\u0438\u043d \u0438\u0437 \u0443\u0437\u043b\u043e\u0432 \u0432\u0435\u0434\u0435\u0442 \u0441\u0435\u0431\u044f \u043a\u0430\u043a \u043b\u0438\u0434\u0435\u0440, \u0447\u0442\u043e\u0431\u044b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u0442\u044c \u043e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u043c \u0443\u0437\u043b\u0430\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f. \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0432\u044b\u0431\u043e\u0440\u0430 \u043b\u0438\u0434\u0435\u0440\u0430 \u043d\u0430 TLA+ \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c: <code>Leader == [v \\in 0..MaxView |-&gt; v % N],<\/code> \u0433\u0434\u0435 <code>MaxView<\/code><em> <\/em>\u2014 \u043d\u043e\u043c\u0435\u0440 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0433\u043e \u0440\u0430\u0443\u043d\u0434\u0430, \u0430 <code>N<\/code><em> <\/em>\u2014 \u043e\u0431\u0449\u0435\u0435 \u0447\u0438\u0441\u043b\u043e \u0443\u0437\u043b\u043e\u0432.<\/p>\n<p>\u041a\u0430\u043a \u0443\u0436\u0435 \u0431\u044b\u043b\u043e \u0441\u043a\u0430\u0437\u0430\u043d\u043e \u0432\u044b\u0448\u0435, \u043c\u043e\u0434\u0435\u043b\u044c \u0432 TLA+ \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0438 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u044d\u0442\u0438\u043c\u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u043c\u0438. \u0421\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0435\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445. \u0414\u043b\u044f \u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432 TLA+ \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043a\u043b\u044e\u0447\u0435\u0432\u043e\u0435 \u0441\u043b\u043e\u0432\u043e <code>VARIABLES<\/code>.<\/p>\n<pre><code class=\"bash\">VARIABLES        messages,       \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u044b\u0445 \u0443\u0437\u043b\u0430\u043c\u0438     RCmessages      \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u0441\u0435\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u043e \u0441\u043c\u0435\u043d\u0435 \u0440\u0430\u0443\u043d\u0434\u0430       processState,   \\* \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0443\u0437\u043b\u043e\u0432 IBFT     decision\u00a0 \u00a0 \u00a0 \u00a0 \\* \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u0430\u044f \u2013 \u0445\u0440\u0430\u043d\u0438\u0442 \u043f\u0440\u0438\u043d\u044f\u0442\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435<\/code><\/pre>\n<p>\u0412 IBFT \u0435\u0441\u0442\u044c \u0447\u0435\u0442\u044b\u0440\u0435 \u0442\u0438\u043f\u0430 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u0443\u0437\u043b\u044b: <code>PRE-PREPARE<\/code>, <code>PREPARE<\/code>, <code>COMMIT<\/code> \u0438 <code>ROUND-CHANGE<\/code>. \u041f\u0435\u0440\u0432\u044b\u0435 \u0442\u0440\u0438 \u0438\u043c\u0435\u044e\u0442 \u0432\u0438\u0434 <code>&lt;message-type, \u03bb, r, value&gt;<\/code>, \u0433\u0434\u0435 <code>\u03bb<\/code> \u2014 \u043d\u043e\u043c\u0435\u0440 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430, <code>r<\/code> \u2014 \u0442\u0435\u043a\u0443\u0449\u0438\u0439 \u0440\u0430\u0443\u043d\u0434, \u0430 <code>value<\/code> \u2014 \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435; \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u0441\u0435\u0445 \u0442\u0430\u043a\u0438\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0431\u0443\u0434\u0435\u043c \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0432 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 messages. \u0421\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 <code>ROUND-CHANGE<\/code> \u043f\u0440\u0435\u0434\u043d\u0430\u0437\u043d\u0430\u0447\u0435\u043d\u044b \u0434\u043b\u044f \u0441\u043b\u0443\u0447\u0430\u044f \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u0430 \u0438 \u0438\u043c\u0435\u044e\u0442 \u0432\u0438\u0434 <code>&lt;ROUND-CHANGE, \u03bb, r, pr, pv&gt;<\/code>, \u0433\u0434\u0435, \u043f\u043e\u043c\u0438\u043c\u043e \u043d\u043e\u043c\u0435\u0440\u043e\u0432 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0438 \u0440\u0430\u0443\u043d\u0434\u0430, \u043f\u0435\u0440\u0435\u0434\u0430\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435: <code>pr<\/code> (prepared round) \u2014 \u043d\u043e\u043c\u0435\u0440 \u0440\u0430\u0443\u043d\u0434\u0430, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0443\u0437\u0435\u043b \u043f\u043e\u043b\u0443\u0447\u0438\u043b \u043a\u0432\u043e\u0440\u0443\u043c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 <code>PREPARE<\/code>, \u0438 <code>pv<\/code> (prepared value) \u2014 \u0432\u0435\u043b\u0438\u0447\u0438\u043d\u0430, \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u043d\u0430\u044f \u0432 \u044d\u0442\u0438\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f\u0445.<\/p>\n<p>\u0412 \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 IBFT \u0435\u0441\u0442\u044c \u043f\u044f\u0442\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f: \u043d\u043e\u043c\u0435\u0440 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430, \u043e\u0442\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0438\u0437 \u043d\u043e\u043c\u0435\u0440\u0430 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0430 \u0432 \u043d\u043e\u043c\u0435\u0440\u0435 \u0442\u0435\u043a\u0443\u0449\u0435\u0433\u043e \u0440\u0430\u0443\u043d\u0434\u0430, <code>pr<\/code>, <code>pv<\/code>, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435. \u0421\u0442\u043e\u0438\u0442 \u0443\u043f\u043e\u043c\u044f\u043d\u0443\u0442\u044c, \u0447\u0442\u043e \u044f \u0441\u0442\u0440\u043e\u0438\u043b \u043c\u043e\u0434\u0435\u043b\u044c \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043d\u043e\u043c\u0435\u0440\u0430 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u043e\u0432 \u0432\u0435\u0437\u0434\u0435 \u0431\u0443\u0434\u0443\u0442 \u043e\u043f\u0443\u0449\u0435\u043d\u044b.<\/p>\n<p>\u041e\u043f\u0438\u0448\u0435\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430. \u0412\u0441\u0435 \u0443\u0437\u043b\u044b \u043d\u0430\u0445\u043e\u0434\u044f\u0442\u0441\u044f \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435, \u0430 \u043b\u0438\u0434\u0435\u0440 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>PRE-PREPARE<\/code> \u0441 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c<em> <\/em><code>v<\/code>.<\/p>\n<pre><code>Init ==    \/\\ \\E v \\in Values:     \/\\ messages = {[type |-&gt; \"PRE-PREPARE\", view_num |-&gt; 1,                               cmd |-&gt; v, from |-&gt; Leader[1]]}     \/\\ processState = [p \\in Corr |-&gt;                         [view_num |-&gt; 1,                          inputValue |-&gt; v,                          pr |-&gt; NilView,                          pv |-&gt; NilValue]]     \/\\ decision = [p \\in Corr |-&gt; NilValue]     \/\\ RCmessages = {}<\/code><\/pre>\n<p>\u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0440\u0430\u0431\u043e\u0442\u0443 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0432 \u00ab\u0445\u043e\u0440\u043e\u0448\u0435\u043c\u00bb \u0441\u043b\u0443\u0447\u0430\u0435, \u043a\u043e\u0433\u0434\u0430 \u043b\u0438\u0434\u0435\u0440 \u043d\u0435 \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0439 \u0438 \u0432 \u0441\u0435\u0442\u0438 \u043d\u0435 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0441\u0431\u043e\u0435\u0432. \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u043a\u0430\u0436\u0434\u044b\u0439 \u0447\u0435\u0441\u0442\u043d\u044b\u0439 \u0443\u0437\u0435\u043b <code>p<\/code> \u0436\u0434\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f <code>PRE-PREPARE<\/code> \u043e\u0442 \u043b\u0438\u0434\u0435\u0440\u0430 \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0442 \u0435\u0433\u043e \u043d\u0430 \u0430\u043a\u0442\u0443\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u0430 <code>JustifyPrePrepare<\/code>. \u0415\u0441\u043b\u0438 \u0442\u0430\u043a\u043e\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u043e, \u0447\u0435\u0441\u0442\u043d\u044b\u0439 \u0443\u0437\u0435\u043b \u0434\u043e\u043b\u0436\u0435\u043d \u043e\u0442\u043f\u0440\u0430\u0432\u0438\u0442\u044c \u043f\u043e \u0441\u0435\u0442\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>PREPARE<\/code>.<\/p>\n<pre><code>UponPrePrepared(p) ==    \/\\ \\E msg \\in messages :      \/\\ msg.from = Leader[processState[p].view_num]     \/\\ msg.type = \"PRE-PREPARE\"     \/\\ msg.view_num = processState[p].view_num     \/\\ JustifyPrePrepare (msg)     \/\\ LET prepare_msg == [type |-&gt; \"PREPARE\",                             view_num |-&gt; processState[p].view_num,                            cmd |-&gt; msg.cmd, from |-&gt; p]        IN \/\\ prepare_msg \\notin messages           \/\\ sendMsg({prepare_msg})   \/\\ UNCHANGED &lt;&lt;processState, decision, RCmessages&gt;&gt;<\/code><\/pre>\n<p>\u041f\u0440\u0438 \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0438 \u043a\u0432\u043e\u0440\u0443\u043c\u0430 (<em>2F + 1<\/em>) \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0442\u0438\u043f\u0430 <code>PREPARE<\/code> \u0432 \u0442\u0435\u043a\u0443\u0449\u0435\u043c \u0440\u0430\u0443\u043d\u0434\u0435 <code>r<\/code> c \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c <code>v<\/code>, \u0447\u0435\u0441\u0442\u043d\u044b\u0439 \u0443\u0437\u0435\u043b \u043e\u0431\u043d\u043e\u0432\u043b\u044f\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f <code>pr<\/code> \u0438 <code>pv<\/code> \u043d\u0430 <code>r<\/code> \u0438 <code>v<\/code> \u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>COMMIT<\/code> \u0441 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u043c\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c.<\/p>\n<pre><code>UponPrepared(p) ==   \/\\ \\E v \\in Values:     \/\\ Cardinality(PrepareMessages(p, v)) &gt;= QUORUM     \/\\ LET commit_msg == [type |-&gt; \"COMMIT\",                            view_num |-&gt; processState[p].view_num,                           cmd |-&gt; v, from |-&gt; p]        IN \/\\ commit_msg \\notin messages           \/\\ processState' = [processState EXCEPT ![p].pr = processState[p].view_num,                                                   ![p].pv = v]           \/\\ sendMsg({commit_msg})    \/\\ UNCHANGED &lt;&lt;decision, RCmessages&gt;&gt;<\/code><\/pre>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446, \u043f\u0440\u0438 \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0438 \u043a\u0432\u043e\u0440\u0443\u043c\u0430 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0442\u0438\u043f\u0430 <code>COMMIT<\/code> \u0441 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c \u0440\u0430\u0443\u043d\u0434\u0430, \u0447\u0435\u0441\u0442\u043d\u044b\u0439 \u0443\u0437\u0435\u043b \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u043e\u0431\u043d\u043e\u0432\u043b\u044f\u044f \u0441\u0432\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 <code>decision<\/code>. \u0412 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u043c \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0438 \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u0435\u0442\u0441\u044f \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0432\u043d\u0435\u0448\u043d\u0435\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>DECIDE<\/code>, \u043a\u043e\u0442\u043e\u0440\u0443\u044e \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u0442 \u0443\u0437\u0435\u043b. \u0418\u043c\u0435\u043d\u043d\u043e \u0435\u0435 \u043c\u044b \u0438 \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u0435\u043c \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043e\u0442\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f <code>decision<\/code>.<\/p>\n<pre><code>UponCommit(p) ==   \/\\ decision[p] = NilValue   \/\\ \\E v \\in Values:     \/\\ Cardinality(CommitMessages(p, v)) &gt;= QUORUM     \/\\ decision' = [decision EXCEPT ![p] = v]   \/\\ UNCHANGED &lt;&lt;processState, messages, RCmessages&gt;&gt;<\/code><\/pre>\n<p>\u041e\u0434\u043d\u0430\u043a\u043e IBFT \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c \u0443\u0441\u0442\u043e\u0439\u0447\u0438\u0432 \u043a \u043e\u0442\u043a\u0430\u0437\u0430\u043c, \u0432 \u0442\u043e\u043c \u0447\u0438\u0441\u043b\u0435 \u0438 \u043a \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u043e\u043c\u0443 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044e. \u042d\u0442\u043e \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u0435\u0442 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0435 \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u043a\u0430\u043a \u043f\u0440\u043e\u0441\u0442\u043e \u043e\u0442\u043a\u043b\u044e\u0447\u0438\u0432\u0448\u0435\u0433\u043e\u0441\u044f \u043e\u0442 \u0441\u0435\u0442\u0438 \u043b\u0438\u0434\u0435\u0440\u0430, \u0442\u0430\u043a \u0438 \u0435\u0433\u043e \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u043e\u0435 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435, \u043a\u043e\u0433\u0434\u0430 \u0442\u0430\u043a\u043e\u0439 \u043b\u0438\u0434\u0435\u0440 \u043c\u043e\u0436\u0435\u0442 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u043b\u044e\u0431\u044b\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f, \u0432 \u0442\u043e\u043c \u0447\u0438\u0441\u043b\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u043c\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u043c\u0438 \u0434\u043b\u044f \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432. \u041c\u0435\u0445\u0430\u043d\u0438\u0437\u043c \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u043e\u0432 \u043a\u0430\u043a \u0440\u0430\u0437 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0442\u0438\u0442\u044c \u043d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0443\u044e \u0440\u0430\u0431\u043e\u0442\u0443 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0432 \u0442\u0430\u043a\u0438\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445.<\/p>\n<p>\u0420\u0435\u0430\u043b\u0438\u0437\u0443\u0435\u043c \u044d\u0442\u043e\u0442 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c \u0432 \u043d\u0430\u0448\u0435\u0439 \u043c\u043e\u0434\u0435\u043b\u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0434\u0432\u0443\u0445 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0435 <code>Timeout<\/code> \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u043e \u043b\u044e\u0431\u044b\u043c \u0443\u0437\u043b\u043e\u043c \u0438 \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u0435\u0442 \u043d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0443\u044e \u0440\u0430\u0431\u043e\u0442\u0443 \u0441\u0435\u0442\u0438. \u0412 \u044d\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0443\u0437\u0435\u043b \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u0438\u0442 \u0432 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0440\u0430\u0443\u043d\u0434 \u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>ROUND-CHANGE<\/code>, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0432 \u0441\u0435\u0431\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f <code>pv<\/code> \u0438 <code>pr<\/code>, \u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u043e\u0432\u044b\u0439 \u043d\u043e\u043c\u0435\u0440 \u0440\u0430\u0443\u043d\u0434\u0430. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0435 <code>UponQRC<\/code><em> <\/em>\u043e\u0442\u0432\u0435\u0447\u0430\u0435\u0442 \u0437\u0430 \u0432\u043e\u0437\u0432\u0440\u0430\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043a \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0440\u0430\u0431\u043e\u0442\u0435: \u043b\u0438\u0434\u0438\u0440\u0443\u044e\u0449\u0438\u0439 \u0443\u0437\u0435\u043b \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>PRE-PREPARE<\/code> \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u044f \u043a\u0432\u043e\u0440\u0443\u043c\u0430 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0442\u0438\u043f\u0430 <code>ROUND-CHANGE<\/code>.<\/p>\n<pre><code>Timeout(p) ==    \/\\ processState[p].view_num &lt; MaxView   \/\\ LET rcMsg == [type |-&gt; \"ROUND-CHANGE\",                     view_num |-&gt; processState[p].view_num + 1,                    pv |-&gt; processState[p].pv, pr |-&gt; processState[p].pr,                     from |-&gt; p]      IN \/\\ rcMsg \\notin RCmessages         \/\\ sendRC({rcMsg})   \/\\ processState' = [processState EXCEPT ![p].view_num = processState[p].view_num + 1]   \/\\ UNCHANGED &lt;&lt;decision, messages&gt;&gt;  RCsMessages(p) == {msg \\in RCmessages : \/\\ msg.type = \"ROUND-CHANGE\"                                          \/\\ Leader[msg.view_num] = p}  UponQRC(p) ==   \/\\ Cardinality(RCsMessages(p)) &gt;= QUORUM   \/\\ JustifyRoundChange(RCsMessages(p))    \/\\ LET q == RCsMessages(p)          v == IF HighestPrepared[q][2] \/= NilValue                THEN HighestPrepared[q][2]                ELSE processState[p].inputValue          ppMsg == [view_num |-&gt; processState[p].view_num,                     type |-&gt; \"PRE-PREPARE\",                    cmd |-&gt; v, from |-&gt; p]      IN \/\\ ppMsg \\notin messages         \/\\ sendMsg({ppMsg})   \/\\ UNCHANGED &lt;&lt;decision, processState, RCmessages&gt;&gt;<\/code><\/pre>\n<p>\u0421\u0442\u043e\u0438\u0442 \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0432\u0430\u0436\u043d\u044b\u0435 \u0448\u0430\u0433\u0438 \u043f\u0440\u0438 \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u0430 \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u043e\u0432. \u041e\u043d\u0438 \u0441\u0432\u044f\u0437\u0430\u043d\u044b \u0441 \u043f\u0440\u0438\u0440\u043e\u0434\u043e\u0439 \u0432\u044b\u0431\u0440\u0430\u043d\u043d\u043e\u0433\u043e \u043f\u043e\u0434\u0445\u043e\u0434\u0430: \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 TLC \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f \u043c\u043e\u0434\u0435\u043b\u0438. \u0412 \u0441\u0432\u044f\u0437\u0438 \u0441 \u044d\u0442\u0438\u043c \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0438\u0432\u0430\u0442\u044c \u0432\u0441\u0435 \u043a\u043e\u043d\u0441\u0442\u0430\u043d\u0442\u044b, \u0432 \u0442\u043e\u043c \u0447\u0438\u0441\u043b\u0435 \u0438 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0440\u0430\u0443\u043d\u0434\u043e\u0432. \u0422\u0430\u043a\u0436\u0435 \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 <code>processState[p].view_num &lt; MaxView<\/code><em>, <\/em>\u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0438\u0432\u0430\u044e\u0449\u0430\u044f \u0447\u0438\u0441\u043b\u043e \u0442\u0430\u0439\u043c-\u0430\u0443\u0442\u043e\u0432 \u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0430\u044f \u0432 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u043c \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0431\u044b\u043b\u043e \u043e\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u0434\u043b\u044f \u0438\u0437\u0431\u0435\u0436\u0430\u043d\u0438\u044f \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0442\u043e\u0440\u043d\u043e\u0433\u043e \u0432\u0437\u0440\u044b\u0432\u0430 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u043f\u0440\u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0435 \u043c\u043e\u0434\u0435\u043b\u0438. \u0412 \u043c\u043e\u0434\u0435\u043b\u0438 \u044f \u043a\u043e\u043c\u043f\u0435\u043d\u0441\u0438\u0440\u0443\u044e \u044d\u0442\u043e \u0442\u0435\u043c, \u0447\u0442\u043e \u0443\u0437\u0435\u043b \u043c\u043e\u0436\u0435\u0442 \u0443\u0439\u0442\u0438 \u0432 \u0442\u0430\u0439\u043c-\u0430\u0443\u0442 \u0432 \u043b\u044e\u0431\u043e\u043c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0438 (\u043a\u0440\u043e\u043c\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0433\u043e \u0440\u0430\u0443\u043d\u0434\u0430).\u00a0<\/p>\n<p>\u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u044b <code>JustifyRoundChange<\/code> \u0438 <code>JustifyPrePrepare<\/code> \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u044b \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u0438 \u043e\u0442\u0432\u0435\u0447\u0430\u044e\u0442 \u0437\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u043f\u0440\u0438 \u0441\u043c\u0435\u043d\u0435 \u0440\u0430\u0443\u043d\u0434\u0430 \u0438 \u0437\u0430 \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0449\u0435\u043d\u0438\u0435 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f \u0447\u0435\u0441\u0442\u043d\u044b\u043c\u0438 \u0443\u0437\u043b\u0430\u043c\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f, \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u043e\u0433\u043e \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c \u043b\u0438\u0434\u0435\u0440\u043e\u043c, \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0435\u043d\u043d\u043e.<\/p>\n<p>\u0422\u0430\u043a, \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u044b \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u043c\u043e\u0434\u0435\u043b\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c.<\/p>\n<pre><code>Steps(p) == IF p \\in Corr              THEN \\\/ UponPrePrepared(p) \\\/ UponPrepared(p) \\\/ UponCommit(p)                   \\\/ Timeout(p) \\\/ UponQRC(p)             ELSE ByzantineBehavior(p)  Next ==   \\\/ \\E p \\in AllProcs: Steps(p)   \\\/ UNCHANGED &lt;&lt;processState, messages, RCmessages, decision&gt;&gt;<\/code><\/pre>\n<p>\u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0435 <code>ByzantineBehaviour<\/code> \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u0435\u0442 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0445 \u0443\u0437\u043b\u043e\u0432: \u043e\u043d\u0438 \u043c\u043e\u0433\u0443\u0442 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u043b\u044e\u0431\u043e\u0433\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u044f \u043f\u0440\u0438 \u043b\u044e\u0431\u043e\u043c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430.<\/p>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u043c\u043e\u0436\u043d\u043e \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u0438\u0442\u044c \u043a \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0435 \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u043d\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0438. \u0412 \u0446\u0435\u043b\u043e\u043c \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e \u0440\u0435\u0448\u0430\u0435\u0442 \u0437\u0430\u0434\u0430\u0447\u0443 \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u043e\u0433\u043e \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043f\u0440\u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u0438 \u043d\u0430\u043b\u0438\u0447\u0438\u044f <em>2f + 1<\/em> \u0447\u0435\u0441\u0442\u043d\u044b\u0445 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u043e\u0432 \u0438 <em>f<\/em> \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0445, \u0435\u0441\u043b\u0438 \u043e\u043d \u043e\u0431\u043b\u0430\u0434\u0430\u0435\u0442 \u0442\u0440\u0435\u043c\u044f \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u043c\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430\u043c\u0438. \u0418\u043c\u0435\u043d\u043d\u043e \u044d\u0442\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043f\u0440\u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 BFT-\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430:<\/p>\n<ol>\n<li>\n<p>\u0421\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c: \u0432\u0441\u0435 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0438\u0435 \u0443\u0437\u043b\u044b \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u044e\u0442 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435.<\/p>\n<\/li>\n<li>\n<p>\u041a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c: \u043f\u0440\u0438\u043d\u044f\u0442\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0431\u044b\u043b\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043e \u043e\u0434\u043d\u0438\u043c \u0438\u0437 \u0438\u043c\u0435\u044e\u0449\u0438\u0445\u0441\u044f \u0443\u0437\u043b\u043e\u0432.<\/p>\n<\/li>\n<li>\n<p>\u0417\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u043c\u043e\u0441\u0442\u044c: \u0432\u0441\u0435 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0438\u0435 \u0443\u0437\u043b\u044b \u0432 \u043a\u043e\u043d\u0446\u0435 \u043a\u043e\u043d\u0446\u043e\u0432 \u0434\u043e\u0441\u0442\u0438\u0433\u0430\u044e\u0442 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f.<\/p>\n<\/li>\n<\/ol>\n<p>\u041f\u0435\u0440\u0432\u044b\u0435 \u0434\u0432\u0430 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u043e\u0442\u043d\u043e\u0441\u044f\u0442\u0441\u044f \u043a \u043a\u043b\u0430\u0441\u0441\u0443 safety, \u0442\u043e \u0435\u0441\u0442\u044c \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044e\u0442, \u0447\u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u043d\u0438\u043a\u043e\u0433\u0434\u0430 \u043d\u0435 \u043f\u0435\u0440\u0435\u0439\u0434\u0435\u0442 \u0432 \u043d\u0435\u0434\u043e\u043f\u0443\u0441\u0442\u0438\u043c\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435. \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c \u0438\u0445 \u043d\u0430 TLA+.<\/p>\n<pre><code>Agreement ==   \\A p, q \\in Corr:     (decision[p] \/= NilValue \/\\ decision[q] \/= NilValue) =&gt;      decision[p] = decision[q]  Validity == \\A p \\in Corr: decision[p] \\in ValuesOrNil<\/code><\/pre>\n<p>\u0417\u0434\u0435\u0441\u044c <code>ValuesOrNil<\/code> \u2014 \u043a\u043e\u043d\u0441\u0442\u0430\u043d\u0442\u043d\u043e\u0435 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u043c\u044b \u0437\u0430\u0434\u0430\u0435\u043c \u043f\u0435\u0440\u0435\u0434 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u043e\u0439. \u041e\u043d\u043e \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0438\u0437 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0445 \u043f\u0440\u0438\u043d\u044f\u0442\u044b\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0438 <code>NilValue<\/code> \u2014 \u043f\u0443\u0441\u0442\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f.<\/p>\n<p>\u0421\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u043c\u043e\u0441\u0442\u0438, \u0432 \u0441\u0432\u043e\u044e \u043e\u0447\u0435\u0440\u0435\u0434\u044c, \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0441\u044f \u043a \u043a\u043b\u0430\u0441\u0441\u0443 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 liveness (\u0436\u0438\u0432\u0443\u0447\u0435\u0441\u0442\u0438), \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044e\u0449\u0438\u0445, \u0447\u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u0440\u0430\u043d\u043e \u0438\u043b\u0438 \u043f\u043e\u0437\u0434\u043d\u043e \u0434\u043e\u0441\u0442\u0438\u0433\u043d\u0435\u0442 \u043d\u0443\u0436\u043d\u043e\u0433\u043e \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f. \u0422\u0430\u043a\u0438\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u043d\u0435\u0435 \u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0435, \u0430 \u0434\u043b\u044f \u0438\u0445 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0431\u044b\u0447\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440\u044b. \u0412 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435\u043c \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u044b\u0439 \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440 <code>&lt;&gt;<\/code> (eventually).\u00a0<\/p>\n<pre><code>Done == \\A p \\in Corr: decision[p] \\in Values Termination == &lt;&gt;Done<\/code><\/pre>\n<p>\u041f\u0440\u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0442\u0430\u043a\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0443\u0447\u0438\u0442\u044b\u0432\u0430\u0442\u044c, \u0447\u0442\u043e \u0432 TLA+ \u043f\u043e \u0443\u043c\u043e\u043b\u0447\u0430\u043d\u0438\u044e \u043b\u044e\u0431\u043e\u0435 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0434\u043e\u043f\u0443\u0441\u043a\u0430\u0435\u0442 stuttering, \u0442\u043e \u0435\u0441\u0442\u044c \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u043d\u0435 \u0438\u0437\u043c\u0435\u043d\u044f\u044e\u0442\u0441\u044f. \u0411\u043e\u043b\u0435\u0435 \u0442\u043e\u0433\u043e, TLA+ \u0434\u043e\u043f\u0443\u0441\u043a\u0430\u0435\u0442 \u0431\u0435\u0441\u043a\u043e\u043d\u0435\u0447\u043d\u043e\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0442\u0430\u043a\u0438\u0445 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432. \u042d\u0442\u043e \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0441\u0438\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u0443 \u0440\u0435\u0430\u043b\u044c\u043d\u044b\u0445 \u0441\u0435\u0442\u0435\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c\u0441\u044f \u0432 \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u044b\u0439 \u043c\u043e\u043c\u0435\u043d\u0442 \u0432\u0440\u0435\u043c\u0435\u043d\u0438. \u0412 \u0441\u0432\u044f\u0437\u0438 \u0441 \u044d\u0442\u0438\u043c \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0436\u0438\u0432\u0443\u0447\u0435\u0441\u0442\u0438 \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0434\u043e\u0431\u0430\u0432\u0438\u0442\u044c \u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u0447\u0435\u0441\u0442\u043d\u043e\u0441\u0442\u0438 (fairness condition), \u0442\u043e \u0435\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u043d\u0435 \u043e\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0435\u0442\u0441\u044f:<\/p>\n<ul>\n<li>\n<p>Weak fairness \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0432\u0441\u0435\u0433\u0434\u0430 \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0438\u0440\u043e\u0432\u0430\u0442\u044c, \u0442\u043e \u0432 \u043a\u043e\u043d\u0435\u0447\u043d\u043e\u043c \u0438\u0442\u043e\u0433\u0435 \u043e\u043d \u0431\u0443\u0434\u0435\u0442 \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0438\u0440\u043e\u0432\u0430\u0442\u044c.\u00a0<\/p>\n<\/li>\n<li>\n<p>Strong fairness \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0432\u0441\u0435\u0433\u0434\u0430 \u043c\u043e\u0436\u0435\u0442 <em>\u043f\u0435\u0440\u0438\u043e\u0434\u0438\u0447\u0435\u0441\u043a\u0438<\/em> \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0438\u0440\u043e\u0432\u0430\u0442\u044c (\u0442\u043e \u0435\u0441\u0442\u044c \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0442\u044c\u0441\u044f \u0438\u043b\u0438 \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0442\u044c\u0441\u044f), \u0442\u043e \u0432 \u043a\u043e\u043d\u0446\u0435 \u043a\u043e\u043d\u0446\u043e\u0432 \u043e\u043d \u0434\u043e\u0431\u044c\u0435\u0442\u0441\u044f \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0430.\u00a0<\/p>\n<\/li>\n<\/ul>\n<p>\u0414\u043e\u0431\u0430\u0432\u0438\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u0435 fairness \u0432 \u043d\u0430\u0448\u0443 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e. Weak fairness<em> <\/em>\u0432\u043b\u0435\u0447\u0435\u0442 \u0437\u0430 \u0441\u043e\u0431\u043e\u0439<em> <\/em>strong fairness, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0434\u043e\u0431\u0430\u0432\u0438\u043c \u044d\u0442\u043e \u0443\u0441\u043b\u043e\u0432\u0438\u0435<em>. <\/em>Weak fairness<em> <\/em>\u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u043a\u0430\u043a \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u0430\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0430 <code>WF_vars(Action)<\/code>, \u0433\u0434\u0435 <code>vars<\/code> \u2014 \u043a\u043e\u0440\u0442\u0435\u0436 \u0432\u0441\u0435\u0445 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043c\u043e\u0434\u0435\u043b\u0438.<\/p>\n<pre><code>Spec == Init          \/\\ [][Next]_vars         \/\\ \\A p \\in AllProcs: WF_vars(Steps(p))<\/code><\/pre>\n<p>\u0422\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u044b\u0439 \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440 <code>[]<\/code> (always) \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e <code>Next<\/code> \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0442\u044c\u0441\u044f \u0432\u0441\u0435\u0433\u0434\u0430. \u042d\u0442\u043e \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u044b\u0439 \u0432\u0438\u0434 \u0437\u0430\u043f\u0438\u0441\u0438 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438: \u043c\u044b \u0437\u0430\u0434\u0430\u043b\u0438 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e <code>Init<\/code>, \u0441\u0438\u0441\u0442\u0435\u043c\u0443 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e<em> <\/em><code>Next<\/code> \u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u0435 weak fairness \u0434\u043b\u044f \u0438\u0437\u0431\u0435\u0436\u0430\u043d\u0438\u044f \u0441\u0438\u043c\u0443\u043b\u044f\u0446\u0438\u0438 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0438 \u0441\u0438\u0441\u0442\u0435\u043c\u044b.<\/p>\n<h2>\u041f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430<\/h2>\n<p>\u041d\u0430\u0448\u0430 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0433\u043e\u0442\u043e\u0432\u0430 \u043a \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0435. \u041f\u0435\u0440\u0435\u0434 \u043d\u0430\u0447\u0430\u043b\u043e\u043c model checking \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0437\u0430\u0434\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0432\u0441\u0435\u0445 \u043a\u043e\u043d\u0441\u0442\u0430\u043d\u0442. \u0427\u0442\u043e\u0431\u044b \u0438\u0437\u0431\u0435\u0436\u0430\u0442\u044c \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0442\u043e\u0440\u043d\u043e\u0433\u043e \u0432\u0437\u0440\u044b\u0432\u0430 \u0447\u0438\u0441\u043b\u0430 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439, \u0431\u0443\u0434\u0435\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u0441 \u0442\u0440\u0435\u043c\u044f \u0447\u0435\u0441\u0442\u043d\u044b\u043c\u0438 \u0438 \u043e\u0434\u043d\u0438\u043c \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c \u0443\u0437\u043b\u043e\u043c, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0441 \u0434\u0432\u0443\u043c\u044f \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u043c\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u043c\u0438. \u041d\u0430\u0447\u043d\u0435\u043c \u0441 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043d\u0430 \u0434\u0432\u0443\u0445 \u0440\u0430\u0443\u043d\u0434\u0430\u0445.<\/p>\n<pre><code>CONSTANT       Corr = {1, 2, 3}      \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0447\u0435\u0441\u0442\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432   Byzantine = {0}       \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0445 \u0443\u0437\u043b\u043e\u0432   MaxView = 2           \\* \u0447\u0438\u0441\u043b\u043e \u0440\u0430\u0443\u043d\u0434\u043e\u0432   Values = {\"a\", \"b\"}   \\* \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f<\/code><\/pre>\n<p>\u0418\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c \u043a\u043e\u043d\u0441\u043e\u043b\u044c\u043d\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e TLC 2.19. \u041a\u0430\u043a \u0443\u0436\u0435 \u0431\u044b\u043b\u043e \u0441\u043a\u0430\u0437\u0430\u043d\u043e \u0432\u044b\u0448\u0435, TLC \u0430\u043d\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u0435\u0442 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f \u043c\u043e\u0434\u0435\u043b\u0438 \u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0437\u0430\u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0432\u043e\u0439\u0441\u0442\u0432; \u0432 \u043e\u0442\u043b\u0438\u0447\u0438\u0435 \u043e\u0442 \u0434\u0440\u0443\u0433\u0438\u0445 \u0441\u0440\u0435\u0434\u0441\u0442\u0432 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, <a href=\"https:\/\/apalache-mc.org\/\">Apalache<\/a>), \u043c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u0437\u0430\u0434\u0430\u0442\u044c \u0433\u043b\u0443\u0431\u0438\u043d\u0443 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438. \u0415\u0441\u043b\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f, \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 \u0432\u0435\u0440\u043d\u0435\u0442 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440 \u2014 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0438\u043b\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 (\u0434\u043b\u044f \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430), \u043d\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0449\u0443\u044e \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u043c\u0443 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0443.<\/p>\n<p>\u0412 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0438 \u0441 \u043c\u0430\u043a\u0441\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u043c \u0447\u0438\u0441\u043b\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u043e\u0432, \u0440\u0430\u0432\u043d\u044b\u043c 2, \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u0443\u0441\u043f\u0435\u0448\u043d\u044b\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442. \u0418\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0443 \u043f\u043e\u043d\u0430\u0434\u043e\u0431\u0438\u043b\u043e\u0441\u044c \u043e\u043a\u043e\u043b\u043e \u043c\u0438\u043d\u0443\u0442\u044b \u0434\u043b\u044f \u043f\u043e\u043b\u043d\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438.\u00a0<\/p>\n<p>\u041f\u0440\u0438 \u0443\u0432\u0435\u043b\u0438\u0447\u0435\u043d\u0438\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f <code>MaxView<\/code> \u0434\u043e 3 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u043e\u043a\u0430\u0437\u0430\u043b\u0441\u044f \u043d\u0435 \u0442\u0430\u043a\u0438\u043c \u0431\u044b\u0441\u0442\u0440\u044b\u043c (\u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043f\u0440\u043e\u0432\u043e\u0434\u0438\u043b\u0430\u0441\u044c \u0441 10 \u0432\u043e\u0440\u043a\u0435\u0440\u0430\u043c\u0438):<\/p>\n<p><code>Model checking completed. No error has been found.<br \/>The depth of the complete state graph search is 31.<br \/>Finished in 18d 19h<\/code><\/p>\n<p>\u042d\u0442\u043e \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0435\u0435 \u0443\u0432\u0435\u043b\u0438\u0447\u0435\u043d\u0438\u0435 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u0442 \u043a \u0440\u0430\u0437\u0440\u0430\u0441\u0442\u0430\u043d\u0438\u044e \u0447\u0438\u0441\u043b\u0430 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0438, \u043a\u0430\u043a \u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0435, \u043a \u0434\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u043c\u0443 \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438. \u0412 \u043f\u0435\u0440\u0432\u0443\u044e \u043e\u0447\u0435\u0440\u0435\u0434\u044c \u044d\u0442\u043e \u0441\u0432\u044f\u0437\u0430\u043d\u043e \u0441 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c\u044e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u043c\u043e\u0441\u0442\u0438. \u041f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u0442\u043e\u043b\u044c\u043a\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0438 \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u0438 \u043f\u0440\u0438 3, 4 \u0438 5 \u0440\u0430\u0443\u043d\u0434\u0430\u0445 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u044b\u0441\u0442\u0440\u0435\u0435.<\/p>\n<h2>\u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435<\/h2>\n<p>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0444\u0443\u043d\u0434\u0430\u043c\u0435\u043d\u0442\u043e\u043c \u043b\u044e\u0431\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044f \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0445 \u0432 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u043e\u0439 \u0441\u0435\u0442\u0438. \u042f \u043e\u043f\u0438\u0441\u0430\u043b \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 IBFT. \u041f\u043e \u043c\u043e\u0435\u043c\u0443 \u043c\u043d\u0435\u043d\u0438\u044e, \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0434\u043e\u043b\u0436\u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0442\u044c\u0441\u044f \u043a\u043e \u0432\u0441\u0435\u043c \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430\u043c \u0442\u0430\u043a\u043e\u0433\u043e \u0442\u0438\u043f\u0430, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u043c \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0441\u0435\u0442\u044f\u0445, \u0434\u0430\u0431\u044b \u0441\u0442\u0440\u043e\u0433\u043e \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043e\u0431\u0435\u0437\u043e\u043f\u0430\u0441\u0438\u0442\u044c \u0438\u0445 \u043e\u0442 \u0441\u0431\u043e\u0435\u0432.\u00a0<\/p>\n<p>\u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u0445\u043e\u0442\u0435\u043b \u043f\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u0430\u043a\u0442\u0443\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u043c\u0435\u0442\u043e\u0434\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u041e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u044f \u044d\u0442\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 \u043d\u0435 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u043c\u0438 \u0434\u043b\u044f \u0442\u0430\u043a\u0438\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432: \u043f\u043e\u0447\u0442\u0438 \u0432\u0441\u0435\u0433\u0434\u0430 \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043f\u043e\u0441\u0442\u0440\u043e\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u0438, \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u044e\u0449\u0438\u0435 \u0441 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u043e\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0438 \u0438\u0445 \u043d\u0435\u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u043c \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435\u043c. \u0413\u043b\u0430\u0432\u043d\u043e\u0439 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u043e\u0439 \u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u0441\u044f \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u0430\u044f \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0442\u0430\u043a\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430. \u041e\u0434\u043d\u0430\u043a\u043e, \u043a\u0430\u043a \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u0431\u043b\u044e\u0434\u0430\u0442\u044c, \u0434\u0430\u0436\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 TLC \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u0431\u0438\u0442\u044c\u0441\u044f \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0430 \u0437\u0430 \u0440\u0430\u0437\u0443\u043c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f, \u0430 \u0431\u043e\u043b\u0435\u0435 \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b (<a href=\"https:\/\/apalache-mc.org\/\">Apalache<\/a>, <a href=\"https:\/\/quint-lang.org\/\">Quint<\/a> \u0438 \u0434\u0440.) \u043c\u043e\u0433\u0443\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u0435\u0449\u0435 \u0431\u044b\u0441\u0442\u0440\u0435\u0435. IBFT \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0430\u0435\u0442 \u0434\u043b\u0438\u043d\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432, \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u043c model checking: \u043e\u0442 \u0441\u0442\u0430\u0432\u0448\u0438\u0445 \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438\u043c\u0438 <a href=\"https:\/\/github.com\/tlaplus\/Examples\/tree\/master\/specifications\/Paxos\">Paxos<\/a> \u0438 <a href=\"https:\/\/github.com\/ongardie\/raft.tla\/blob\/master\/raft.tla\">Raft<\/a> \u0434\u043e \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u043d\u043e\u0432\u044b\u0445 <a href=\"https:\/\/github.com\/afonsonf\/ceph-consensus-spec\">Ceph<\/a> \u0438 <a href=\"https:\/\/protocols-made-fun.com\/consensus\/matterlabs\/quint\/specification\/modelchecking\/2024\/07\/29\/chonkybft.html\">ChonkyBFT<\/a>.<\/p>\n<p>Positive Technologies \u0430\u043a\u0442\u0438\u0432\u043d\u043e \u0438\u0437\u0443\u0447\u0430\u0435\u0442 \u0438 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442 \u043c\u0435\u0442\u043e\u0434\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430\u0445, \u043c\u044b \u043f\u043e\u043d\u0438\u043c\u0430\u0435\u043c \u0438\u0445 \u0437\u043d\u0430\u0447\u0438\u043c\u043e\u0441\u0442\u044c \u0438 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0441\u0442\u044c. \u041c\u044b \u0442\u0430\u043a\u0436\u0435 \u0430\u043a\u0442\u0438\u0432\u043d\u043e \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u043c \u0438 \u0432\u043d\u0435\u0434\u0440\u044f\u0435\u043c \u0434\u0440\u0443\u0433\u0438\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0438 \u043c\u0435\u0442\u043e\u0434\u0438\u043a\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043f\u043e\u0432\u044b\u0441\u0438\u0442\u044c \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u043e \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0437\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u043c\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c. \u041e\u043d\u0438 \u0432\u043a\u043b\u044e\u0447\u0430\u044e\u0442 \u0432 \u0441\u0435\u0431\u044f \u043a\u0430\u043a \u043d\u043e\u0432\u0435\u0439\u0448\u0438\u0435 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0442\u0430\u043a \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u0435 \u0432\u0440\u0435\u043c\u0435\u043d\u0435\u043c \u043c\u0435\u0442\u043e\u0434\u0438\u043a\u0438 \u2014<a href=\"https:\/\/habr.com\/ru\/companies\/pt\/articles\/775074\/\"> \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u0430\u043d\u0430\u043b\u0438\u0437<\/a>, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0438 \u0444\u0430\u0437\u0437\u0438\u043d\u0433.\u00a0<\/p>\n<\/p>\n<\/div>\n<\/div>\n<\/div>\n<p><!----><!----><\/div>\n<p><!----><!----><br \/> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habr.com\/ru\/articles\/864754\/\"> https:\/\/habr.com\/ru\/articles\/864754\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<figure class=\"full-width\"><\/figure>\n<p>\u0414\u043e\u0431\u0440\u044b\u0439 \u0434\u0435\u043d\u044c! \u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u041a\u0438\u0440\u0438\u043b\u043b \u0417\u0438\u0431\u043e\u0440\u043e\u0432, \u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u044e \u043e\u0442\u0434\u0435\u043b \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c Positive Technologies. \u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0443 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0434\u043b\u044f \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0449\u0435\u043d\u0438\u044f \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439 \u0432 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043a\u043e\u043c\u043f\u043e\u043d\u0435\u043d\u0442\u0430\u0445 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430. \u0420\u0430\u043d\u0435\u0435 <a href=\"https:\/\/habr.com\/en\/companies\/pt\/articles\/804861\/\">\u043c\u044b \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c \u043c\u0435\u0442\u043e\u0434\u043e\u043c<\/a>. \u0412 \u044d\u0442\u043e\u0442 \u0440\u0430\u0437 \u0440\u0435\u0447\u044c \u043f\u043e\u0439\u0434\u0435\u0442 \u043e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430\u0445 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u2014 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u0430\u0445 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f \u0443\u0437\u043b\u0430\u043c\u0438 \u043d\u043e\u0432\u044b\u0445 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439 \u0432 \u0446\u0435\u043f\u043e\u0447\u043a\u0443, \u0430 \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u0431 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 Istanbul Byzantine Fault Tolerant \u0438 \u0432 \u0446\u0435\u043b\u043e\u043c \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u0435\u0442\u043e\u0434\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439.\u00a0<\/p>\n<h2>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430<\/h2>\n<p>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u2014 \u043e\u0434\u043d\u0430 \u0438\u0437 \u0444\u0443\u043d\u0434\u0430\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0430\u0441\u0442\u0435\u0439 \u043b\u044e\u0431\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044e\u0449\u0430\u044f \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c \u0438 \u0446\u0435\u043b\u043e\u0441\u0442\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u043e\u0433\u043e \u0440\u0435\u0435\u0441\u0442\u0440\u0430 \u0431\u0435\u0437 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e\u0441\u0442\u0438 \u0432 \u0446\u0435\u043d\u0442\u0440\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438. \u0422\u0430\u043a\u043e\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u0443 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432 \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442\u044c \u043a \u0441\u043e\u0433\u043b\u0430\u0441\u0438\u044e \u043e \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044f \u043d\u0435\u0438\u0437\u043c\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u0438 \u043f\u0440\u043e\u0437\u0440\u0430\u0447\u043d\u043e\u0441\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0445 \u0434\u0430\u0436\u0435 \u0432 \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u0445 \u043f\u043e\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e \u043d\u0435\u043d\u0430\u0434\u0435\u0436\u043d\u043e\u0439 \u0438\u043b\u0438 \u0437\u043b\u043e\u043d\u0430\u043c\u0435\u0440\u0435\u043d\u043d\u043e\u0439 \u0441\u0440\u0435\u0434\u044b, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043a\u0430\u0436\u0434\u044b\u0439 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a \u043c\u043e\u0436\u0435\u0442 \u0434\u0435\u0439\u0441\u0442\u0432\u043e\u0432\u0430\u0442\u044c \u0432 \u043f\u0435\u0440\u0432\u0443\u044e \u043e\u0447\u0435\u0440\u0435\u0434\u044c \u0438\u0441\u0445\u043e\u0434\u044f \u0438\u0437 \u043c\u0430\u043a\u0441\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0439 \u0432\u044b\u0433\u043e\u0434\u044b.<\/p>\n<p>\u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0440\u0430\u0437\u043d\u043e\u0432\u0438\u0434\u043d\u043e\u0441\u0442\u0435\u0439 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u044b\u0445 \u0434\u043b\u044f \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u0435\u043d\u0438\u044f \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u0439 \u043a \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438, \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0438 \u043c\u0430\u0441\u0448\u0442\u0430\u0431\u0438\u0440\u0443\u0435\u043c\u043e\u0441\u0442\u0438 \u0441\u0435\u0442\u0438. \u041d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b\u0435 \u0438\u0437 \u043d\u0438\u0445 \u2014 Proof of Work (PoW), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0432 Bitcoin, \u0433\u0434\u0435 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0438 \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u043c\u043e\u0449\u043d\u043e\u0441\u0442\u0438 \u0434\u043b\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0441\u043b\u043e\u0436\u043d\u044b\u0445 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0437\u0430\u0434\u0430\u0447 \u0434\u043b\u044f \u043f\u043e\u0434\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u0438 Proof of Stake (PoS), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0441\u0435\u0439\u0447\u0430\u0441 \u0432 Ethereum (\u0440\u0430\u043d\u0435\u0435 \u0442\u0430\u043c \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0441\u044f PoW), \u0433\u0434\u0435 \u043f\u0440\u0430\u0432\u043e \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u043d\u043e\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0430 \u0432\u044b\u0434\u0430\u0435\u0442\u0441\u044f \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0443 \u0441 \u043d\u0430\u0438\u0431\u043e\u043b\u044c\u0448\u0438\u043c \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e\u043c \u043d\u0430\u0442\u0438\u0432\u043d\u044b\u0445 \u0442\u043e\u043a\u0435\u043d\u043e\u0432.\u00a0<\/p>\n<p>\u041f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u044b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0437\u0434\u0435\u043b\u0438\u0442\u044c \u043d\u0430 \u0434\u0432\u0435 \u0433\u0440\u0443\u043f\u043f\u044b \u043f\u043e \u0442\u0438\u043f\u0443 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u0441\u0435\u0442\u0438, \u043a \u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043e\u043d\u0438 \u0443\u0441\u0442\u043e\u0439\u0447\u0438\u0432\u044b. \u041d\u0435\u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0435 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432\u043e\u0437\u043d\u0438\u043a\u0430\u044e\u0442, \u043a\u043e\u0433\u0434\u0430 \u0443\u0437\u043b\u044b \u0432\u044b\u0445\u043e\u0434\u044f\u0442 \u0438\u0437 \u0441\u0442\u0440\u043e\u044f \u0438\u0437-\u0437\u0430 \u0430\u043f\u043f\u0430\u0440\u0430\u0442\u043d\u044b\u0445 \u0441\u0431\u043e\u0435\u0432 \u0438\u043b\u0438 \u0441\u0435\u0442\u0435\u0432\u044b\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c, \u043d\u043e \u043d\u0435 \u0432\u0435\u0434\u0443\u0442 \u0441\u0435\u0431\u044f \u0437\u043b\u043e\u043d\u0430\u043c\u0435\u0440\u0435\u043d\u043d\u043e. \u0412\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0435 \u043e\u0448\u0438\u0431\u043a\u0438, \u0441 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u044e\u0442 \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0432\u0440\u0435\u0434\u043e\u043d\u043e\u0441\u043d\u044b\u0445 \u0443\u0437\u043b\u043e\u0432, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u043e \u0438\u043b\u0438 \u0443\u043c\u044b\u0448\u043b\u0435\u043d\u043d\u043e \u0432\u0440\u0435\u0434\u0438\u0442\u044c \u0441\u0435\u0442\u0438, \u043f\u0435\u0440\u0435\u0434\u0430\u0432\u0430\u044f \u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0440\u0435\u0447\u0438\u0432\u0443\u044e \u0438\u043b\u0438 \u043b\u043e\u0436\u043d\u0443\u044e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e. \u041b\u0435\u0441\u043b\u0438 \u041b\u044d\u043c\u043f\u043e\u0440\u0442 \u0438 \u0420\u043e\u0431\u0435\u0440\u0442 \u0428\u043e\u0441\u0442\u0430\u043a <a href=\"https:\/\/lamport.azurewebsites.net\/pubs\/reaching.pdf\">\u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438<\/a>, \u0447\u0442\u043e \u0434\u043b\u044f \u0434\u043e\u0441\u0442\u0438\u0436\u0435\u043d\u0438\u044f \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0441 <em>N<\/em> \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u0445 \u0443\u0437\u043b\u043e\u0432 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u0430\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u0434\u043e\u043b\u0436\u043d\u0430 \u0441\u043e\u0441\u0442\u043e\u044f\u0442\u044c \u043a\u0430\u043a \u043c\u0438\u043d\u0438\u043c\u0443\u043c \u0438\u0437 <em>3N\u202f+\u202f1<\/em> \u0443\u0437\u043b\u043e\u0432 \u0438 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0430\u0442\u044c \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0443\u0441\u0442\u043e\u0439\u0447\u0438\u0432\u044b\u0439 \u043a \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c \u043e\u0448\u0438\u0431\u043a\u0430\u043c (Byzantine Fault Tolerant, BFT).<\/p>\n<p>\u0420\u043e\u043b\u044c \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430\u0445 \u043a\u0440\u0438\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0432\u0430\u0436\u043d\u0430 \u0434\u043b\u044f \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0438 \u0434\u0435\u0446\u0435\u043d\u0442\u0440\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u0435\u0442\u0438. \u0412\u044b\u0431\u043e\u0440 \u043d\u0435\u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0441\u0435\u0442\u0435\u0432\u044b\u043c \u0440\u0430\u0437\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u043c, \u043f\u0440\u0438 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0440\u0430\u0437\u043d\u044b\u0435 \u0443\u0437\u043b\u044b \u0431\u0443\u0434\u0443\u0442 \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0440\u0430\u0437\u043d\u044b\u0435 \u0446\u0435\u043f\u043e\u0447\u043a\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u0438\u043b\u0438 \u043a \u043f\u043e\u043b\u043d\u043e\u0439 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435 \u0441\u0435\u0442\u0438. \u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432 \u0430\u0442\u0430\u043a \u043d\u0430 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u044b \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u0421\u0430\u043c\u0430\u044f \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u0430\u044f \u0438\u0437 \u043d\u0438\u0445 \u2014 <a href=\"https:\/\/academy.binance.com\/ru\/glossary\/51-percent-attack\">\u0430\u0442\u0430\u043a\u0430 51%<\/a> \u043d\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u044b PoW, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0449\u0430\u044f \u0437\u043b\u043e\u0443\u043c\u044b\u0448\u043b\u0435\u043d\u043d\u0438\u043a\u0443 \u0441 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0439 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u043c\u043e\u0449\u043d\u043e\u0441\u0442\u044c\u044e \u043a\u043e\u043d\u0442\u0440\u043e\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u0435\u0442\u044c \u0438 \u0441\u043e\u0432\u0435\u0440\u0448\u0430\u0442\u044c \u0434\u0432\u043e\u0439\u043d\u044b\u0435 \u0442\u0440\u0430\u0442\u044b.\u00a0<\/p>\n<h2>\u041a\u0430\u043a \u043e\u0431\u0435\u0437\u043e\u043f\u0430\u0441\u0438\u0442\u044c \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d \u043e\u0442 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0435<\/h2>\n<p><a href=\"https:\/\/habr.com\/en\/companies\/pt\/articles\/804861\/\">\u041a\u0430\u043a \u043c\u044b \u0443\u0436\u0435 \u0437\u043d\u0430\u0435\u043c<\/a>, \u043c\u0435\u0442\u043e\u0434\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u044b \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u041e\u043d\u0438 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u044b \u0438 \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430, \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044f \u0438\u0445 \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0441\u0442\u043e\u044f\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u043c \u0442\u0438\u043f\u0430\u043c \u0430\u0442\u0430\u043a \u0438 \u043e\u0442\u043a\u0430\u0437\u043e\u0432.<\/p>\n<p>\u0412 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u043b \u0434\u0432\u0430 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u043f\u043e\u0434\u0445\u043e\u0434\u0430 \u043a \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c: \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u0443\u044e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e \u0438 model checking. \u0414\u043b\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u0430 \u044d\u0442\u0438\u0445 \u043c\u0435\u0442\u043e\u0434\u0430, \u043e\u0434\u043d\u0430\u043a\u043e \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u0435\u043d \u043c\u0435\u0442\u043e\u0434 model checking. \u042d\u0442\u043e \u0441\u0432\u044f\u0437\u0430\u043d\u043e \u0441 \u0442\u0435\u043c, \u0447\u0442\u043e \u043e\u0431\u044b\u0447\u043d\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u043f\u0440\u0435\u0437\u0435\u043d\u0442\u0443\u0435\u0442\u0441\u044f \u0432 \u0430\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043d\u0430 \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0438\u043b\u0438 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0430, \u0438 \u0443\u0436\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u044d\u0442\u0438\u0445 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0440\u0435\u0430\u043b\u0438\u0437\u0443\u0435\u0442\u0441\u044f \u043d\u0430 \u0432\u044b\u0431\u0440\u0430\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f.\u00a0<\/p>\n<p>\u041c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0434\u043e\u0431\u043d\u043e \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0442\u044c \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0430, \u0430 \u0432\u044b\u0440\u0430\u0437\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u044f\u0437\u044b\u043a\u043e\u0432 \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0438 \u043e\u0431\u044b\u0447\u043d\u043e \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0434\u043b\u044f \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u0438\u044f \u0442\u0430\u043a\u0438\u0445 \u043c\u043e\u0434\u0435\u043b\u0435\u0439. \u041e\u0434\u043d\u0430\u043a\u043e \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0442\u043e\u0436\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u041e\u0434\u0438\u043d \u0438\u0437 \u0443\u0441\u043f\u0435\u0448\u043d\u044b\u0445 \u043a\u0435\u0439\u0441\u043e\u0432 \u2014 \u044d\u0442\u043e <a href=\"https:\/\/github.com\/uwplse\/verdi-raft\">\u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 Raft \u0432\u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435 Verdi<\/a>, \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0432 Coq.\u00a0<\/p>\n<h2>TLA+<\/h2>\n<p>\u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u044e\u0441\u044c \u043d\u0430 \u043c\u0435\u0442\u043e\u0434\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0438 \u0431\u0443\u0434\u0443 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u044f\u0437\u044b\u043a TLA+ \u0432\u043c\u0435\u0441\u0442\u0435 \u0441 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0438 TLC. TLA+ \u2014 \u044d\u0442\u043e \u044f\u0437\u044b\u043a \u0434\u043b\u044f \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c \u0438 \u043f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432. \u041e\u043d \u043e\u0441\u043d\u043e\u0432\u0430\u043d \u043d\u0430 \u0442\u0435\u043e\u0440\u0438\u0438 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432, \u043b\u043e\u0433\u0438\u043a\u0435 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u0438 \u0442\u0435\u043c\u043f\u043e\u0440\u0430\u043b\u044c\u043d\u043e\u0439 \u043b\u043e\u0433\u0438\u043a\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439 (TLA, temporal logic of actions). \u041f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0435 \u043d\u0430 TLA+, \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u043c \u043a\u0430\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043d\u0430 \u043e\u0431\u044b\u0447\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f: \u043e\u043d\u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u044e\u0442\u0441\u044f \u0447\u0435\u0440\u0435\u0437 \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439. \u0421\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 (model checker) \u2014 \u044d\u0442\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u044b. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0437\u0430\u0434\u0430\u0435\u0442 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e, \u0430 model checker \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442, \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u044b \u043b\u0438 \u043e\u043d\u0438 \u0434\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0438 \u0438\u043b\u0438 \u043d\u0435\u0442. \u0412 \u0441\u043b\u0443\u0447\u0430\u0435 \u0435\u0441\u043b\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f, \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u0438\u0442 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440.<\/p>\n<p>\u041c\u043e\u0434\u0435\u043b\u044c \u0432 TLA+ \u2014 \u044d\u0442\u043e<strong> <\/strong>\u043d\u0430\u0431\u043e\u0440 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0438 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u044d\u0442\u0438\u043c\u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0437\u0430\u0434\u0430\u044e\u0442\u0441\u044f \u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432 \u0438 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439. \u041c\u043e\u0434\u0435\u043b\u044c \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0441\u0438\u0441\u0442\u0435\u043c\u044b \u043a\u0430\u043a \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439, \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0449\u0438\u0445 \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c \u0438 \u0438\u0437\u043c\u0435\u043d\u044f\u044e\u0449\u0438\u0445\u0441\u044f \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439. \u0414\u043b\u044f \u0442\u043e\u0433\u043e \u0447\u0442\u043e\u0431\u044b \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u043d\u0430 TLA+, \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0437\u0430\u0434\u0430\u0442\u044c \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0438 \u0441\u0438\u0441\u0442\u0435\u043c\u0443 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432. \u041f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u043c\u043e\u0436\u043d\u043e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0432 \u044d\u0442\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432 \u0438 \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0432 model checker.<\/p>\n<p>\u0421 \u043f\u043e\u043c\u043e\u0449\u044c\u044e TLA+ \u0431\u044b\u043b\u043e \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u043e \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043e \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430: <a href=\"https:\/\/github.com\/tlaplus\/Examples\/tree\/master\/specifications\/Paxos\">Paxos<\/a>, <a href=\"https:\/\/github.com\/ongardie\/raft.tla\/blob\/master\/raft.tla\">Raft<\/a>, <a href=\"https:\/\/arxiv.org\/pdf\/1807.04938\">Tendermint<\/a>, <a href=\"https:\/\/www.mais-journal.ru\/jour\/article\/view\/1436\/1091\">HotStuff<\/a> \u0438 \u0434\u0440\u0443\u0433\u0438\u0435.<\/p>\n<h2>\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c IBFT<\/h2>\n<p><a href=\"https:\/\/pmg.csail.mit.edu\/papers\/osdi99.pdf\">\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c Practical Byzantine Fault Tolerant (pBFT)<\/a> \u0431\u044b\u043b \u043f\u0435\u0440\u0432\u044b\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u043c, \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u044e\u0449\u0438\u043c \u0434\u043e\u0441\u0442\u0438\u0436\u0435\u043d\u0438\u0435 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0447\u0430\u0441\u0442\u0438\u0447\u043d\u043e \u0441\u0438\u043d\u0445\u0440\u043e\u043d\u043d\u044b\u0445 \u0441\u0435\u0442\u044f\u0445 \u0441 \u0432\u0438\u0437\u0430\u043d\u0442\u0438\u0439\u0441\u043a\u0438\u043c\u0438 \u043e\u0448\u0438\u0431\u043a\u0430\u043c\u0438, \u0433\u0434\u0435 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c \u043d\u0435 \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u042d\u0442\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u0438\u043b\u0430 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432, \u0443\u043b\u0443\u0447\u0448\u0430\u044e\u0449\u0438\u0445 \u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u044f\u044e\u0449\u0438\u0445 pBFT, \u0441\u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 \u043e\u0434\u043d\u043e\u0439 \u0438 \u0442\u043e\u0439 \u0436\u0435 <a href=\"https:\/\/groups.csail.mit.edu\/tds\/papers\/Lynch\/jacm88.pdf\">\u0447\u0430\u0441\u0442\u0438\u0447\u043d\u043e \u0441\u0438\u043d\u0445\u0440\u043e\u043d\u043d\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0438<\/a>, \u0433\u0434\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0432 \u0442\u0435\u0447\u0435\u043d\u0438\u0435 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438.<\/p>\n<figure class=\"full-width\">\n<div><figcaption>\u0420\u0438\u0441\u0443\u043d\u043e\u043a 1. \u0420\u0430\u0431\u043e\u0442\u0430 pBFT<\/figcaption><\/div>\n<\/figure>\n<p>\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c IBFT (Istanbul Byzantine Fault Tolerant) \u0442\u0430\u043a\u0436\u0435 \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u043b\u0435\u043d pBFT \u0438 \u0431\u044b\u043b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 <a href=\"https:\/\/github.com\/ethereum\/EIPs\/issues\/650\">EIP650<\/a> (Ethereum Improvement Proposals). \u0421\u043e\u0437\u0434\u0430\u043d\u0438\u0435 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0431\u044b\u043b\u043e \u043c\u043e\u0442\u0438\u0432\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u0442\u0435\u043c, \u0447\u0442\u043e pBFT \u0432 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u043c \u0432\u0438\u0434\u0435 \u043d\u0435 \u043f\u043e\u0434\u0445\u043e\u0434\u0438\u0442 \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0441\u0435\u0442\u044f\u0445. \u042d\u0442\u043e \u0441\u0432\u044f\u0437\u0430\u043d\u043e \u043f\u043e\u043f\u0440\u043e\u0441\u0442\u0443 \u0441 \u0442\u0435\u043c, \u0447\u0442\u043e \u043e\u043d \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u043b\u0441\u044f \u0432 \u0434\u0430\u043b\u0435\u043a\u043e\u043c 1999 \u0433\u043e\u0434\u0443, \u0437\u0430 10 \u043b\u0435\u0442 \u0434\u043e \u043f\u043e\u044f\u0432\u043b\u0435\u043d\u0438\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430 Bitcoin. \u0412 pBFT, \u043a\u0430\u043a \u0432\u0438\u0434\u043d\u043e \u0438\u0437 \u0435\u0433\u043e \u0441\u0445\u0435\u043c\u044b, \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u0442\u0441\u044f \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u00ab\u043a\u043b\u0438\u0435\u043d\u0442\u0430\u00bb, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0437\u0430\u043f\u0440\u043e\u0441\u044b \u0438 \u0436\u0434\u0435\u0442 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432. \u041e\u0434\u043d\u0430\u043a\u043e \u0432 \u043a\u043e\u043d\u0442\u0435\u043a\u0441\u0442\u0435 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430 \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u0432\u0441\u0435\u0445 \u0432\u0430\u043b\u0438\u0434\u0430\u0442\u043e\u0440\u043e\u0432 \u043a\u0430\u043a \u00ab\u043a\u043b\u0438\u0435\u043d\u0442\u043e\u0432\u00bb. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0446\u0435\u043f\u043e\u0447\u043a\u0430 \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0438\u0440\u043e\u0432\u0430\u043b\u0430, \u0432 \u043a\u0430\u0436\u0434\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435 \u0434\u043e\u043b\u0436\u0435\u043d \u043f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u043e \u0432\u044b\u0431\u0438\u0440\u0430\u0442\u044c\u0441\u044f \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u0442\u044c \u0431\u043b\u043e\u043a-\u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430. \u0422\u0430\u043a\u0436\u0435 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u0440\u0430\u0431\u043e\u0442\u044b \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u043e\u0433\u043e pBFT \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 \u0447\u0442\u0435\u043d\u0438\u044f \u0438 \u0437\u0430\u043f\u0438\u0441\u0438 \u0432 \u0444\u0430\u0439\u043b\u043e\u0432\u043e\u0439 \u0441\u0438\u0441\u0442\u0435\u043c\u0435, \u0430 \u043e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435 \u043c\u044b \u043e\u0436\u0438\u0434\u0430\u0435\u043c \u0432\u044b\u0431\u043e\u0440 \u043d\u043e\u0432\u043e\u0433\u043e \u0431\u043b\u043e\u043a\u0430 \u0434\u043b\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0432 \u0446\u0435\u043f\u043e\u0447\u043a\u0443.<\/p>\n<p>IBFT \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0441\u0435\u0442\u044f\u0445 \u0441 \u0440\u0430\u0437\u0440\u0435\u0448\u0435\u043d\u0438\u044f\u043c\u0438 (permissioned blockchains), \u0433\u0434\u0435 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a\u0438 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b \u0438 \u0438\u0434\u0435\u043d\u0442\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u044b. \u041e\u043d \u0431\u044b\u043b \u043f\u0435\u0440\u0432\u043e\u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d \u043a\u0430\u043a \u0447\u0430\u0441\u0442\u044c \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c\u044b Quorum, \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u043e\u0439 \u043a\u043e\u043c\u043f\u0430\u043d\u0438\u0435\u0439 JPMorgan Chase. \u041e\u0434\u043d\u0430\u043a\u043e \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u043e\u0448\u0435\u043b \u0434\u043e\u043b\u0433\u0438\u0439 \u043f\u0443\u0442\u044c \u0447\u0435\u0440\u0435\u0437 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0434\u043e\u0440\u0430\u0431\u043e\u0442\u043e\u043a \u043f\u0435\u0440\u0435\u0434 \u043f\u043e\u043b\u043d\u043e\u0446\u0435\u043d\u043d\u044b\u043c \u0432\u043d\u0435\u0434\u0440\u0435\u043d\u0438\u0435\u043c \u0432 Quorum.<\/p>\n<p>\u041f\u0435\u0440\u0432\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u044f IBFT \u043d\u0435 \u0432\u0441\u0435\u0433\u0434\u0430 \u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e: \u0434\u0432\u0430 \u0447\u0435\u0441\u0442\u043d\u044b\u0445 \u0443\u0437\u043b\u0430 \u043c\u043e\u0433\u043b\u0438 \u0432\u044b\u0431\u0440\u0430\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f. \u0412 \u043e\u0431\u043d\u043e\u0432\u043b\u0435\u043d\u043d\u043e\u043c \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0435 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0431\u044b\u043b\u0438 \u0440\u0435\u0448\u0435\u043d\u044b, \u043d\u043e \u043f\u043e\u044f\u0432\u0438\u043b\u0438\u0441\u044c <a href=\"https:\/\/github.com\/jpmorganchase\/quorum\/issues\/305\">\u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0441 \u0436\u0438\u0432\u0443\u0447\u0435\u0441\u0442\u044c\u044e \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430<\/a>: \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043c\u043e\u0433\u043b\u0438 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0432\u0437\u0430\u0438\u043c\u043d\u043e\u043c\u0443 \u043e\u0436\u0438\u0434\u0430\u043d\u0438\u044e \u0438 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435 (deadlock). \u0412 \u043e\u0442\u0432\u0435\u0442 \u043d\u0430 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0431\u044b\u043b\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043e \u0434\u0432\u0430 \u0440\u0435\u0448\u0435\u043d\u0438\u044f. <a href=\"https:\/\/arxiv.org\/pdf\/1901.07160\">\u041f\u0435\u0440\u0432\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435<\/a> \u2014 \u0438\u0437\u0431\u0430\u0432\u0438\u0442\u044c\u0441\u044f \u043e\u0442 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u0430 \u0431\u043b\u043e\u043a\u0438\u0440\u043e\u0432\u043a\u0438 \u0443\u0437\u043b\u043e\u0432 \u0438 \u0434\u043e\u0431\u0430\u0432\u0438\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u043e\u0432, \u043f\u043e\u0445\u043e\u0436\u0438\u0439 \u043d\u0430 \u0442\u043e\u0442, \u0447\u0442\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0432 pBFT. \u0412\u0442\u043e\u0440\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0431\u044b\u043b\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043e \u043a\u0430\u043a \u0440\u0430\u0437 \u0432 \u0440\u0430\u043c\u043a\u0430\u0445 \u0440\u0430\u0431\u043e\u0442\u044b \u043d\u0430\u0434 Quorum, \u0438 \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u0431 \u044d\u0442\u043e\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043f\u043e\u0439\u0434\u0435\u0442 \u0440\u0435\u0447\u044c \u0434\u0430\u043b\u0435\u0435.<\/p>\n<figure class=\"full-width\">\n<div><figcaption>\u0420\u0438\u0441\u0443\u043d\u043e\u043a 2. <a href=\"https:\/\/github.com\/ethereum\/EIPs\/issues\/650\">\u0420\u0430\u0431\u043e\u0442\u0430 IBFT<\/a><\/figcaption><\/div>\n<\/figure>\n<h2>\u041c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 IBFT \u043d\u0430 TLA+<\/h2>\n<p>\u041a\u0430\u043a \u044f \u0443\u0436\u0435 \u043e\u0442\u043c\u0435\u0442\u0438\u043b, \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u043e\u0432 \u043a\u043e\u043d\u0441\u0435\u043d\u0441\u0443\u0441\u0430 \u0443\u0434\u043e\u0431\u043d\u043e \u0441\u0442\u0440\u043e\u0438\u0442\u044c \u043f\u043e \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434\u0443 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u0418\u043c\u0435\u043d\u043d\u043e \u0442\u0430\u043a\u043e\u0439 \u043f\u043e\u0434\u0445\u043e\u0434 \u044f \u0438\u0437\u0431\u0440\u0430\u043b \u0434\u043b\u044f IBFT, \u0432\u0437\u044f\u0432 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 <a href=\"https:\/\/arxiv.org\/pdf\/2002.03613\">\u0438\u0437 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0439 \u043f\u0443\u0431\u043b\u0438\u043a\u0430\u0446\u0438\u0438 Quorum \u043e\u0431 \u044d\u0442\u043e\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435<\/a>.\u00a0<\/p>\n<p>\u041a\u0430\u0436\u0434\u044b\u0439 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u0442 \u043f\u043e \u0440\u0430\u0443\u043d\u0434\u0430\u043c. \u0412 \u043a\u0430\u0436\u0434\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435 \u043e\u0434\u0438\u043d \u0438\u0437 \u0443\u0437\u043b\u043e\u0432 \u0432\u0435\u0434\u0435\u0442 \u0441\u0435\u0431\u044f \u043a\u0430\u043a \u043b\u0438\u0434\u0435\u0440, \u0447\u0442\u043e\u0431\u044b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u0442\u044c \u043e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u043c \u0443\u0437\u043b\u0430\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f. \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0432\u044b\u0431\u043e\u0440\u0430 \u043b\u0438\u0434\u0435\u0440\u0430 \u043d\u0430 TLA+ \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c: <code>Leader == [v \\in 0..MaxView |-&gt; v % N],<\/code> \u0433\u0434\u0435 <code>MaxView<\/code><em> <\/em>\u2014 \u043d\u043e\u043c\u0435\u0440 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0433\u043e \u0440\u0430\u0443\u043d\u0434\u0430, \u0430 <code>N<\/code><em> <\/em>\u2014 \u043e\u0431\u0449\u0435\u0435 \u0447\u0438\u0441\u043b\u043e \u0443\u0437\u043b\u043e\u0432.<\/p>\n<p>\u041a\u0430\u043a \u0443\u0436\u0435 \u0431\u044b\u043b\u043e \u0441\u043a\u0430\u0437\u0430\u043d\u043e \u0432\u044b\u0448\u0435, \u043c\u043e\u0434\u0435\u043b\u044c \u0432 TLA+ \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0438 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u044d\u0442\u0438\u043c\u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u043c\u0438. \u0421\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0435\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445. \u0414\u043b\u044f \u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432 TLA+ \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043a\u043b\u044e\u0447\u0435\u0432\u043e\u0435 \u0441\u043b\u043e\u0432\u043e <code>VARIABLES<\/code>.<\/p>\n<pre><code class=\"bash\">VARIABLES        messages,       \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u044b\u0445 \u0443\u0437\u043b\u0430\u043c\u0438     RCmessages      \\* \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u0441\u0435\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u043e \u0441\u043c\u0435\u043d\u0435 \u0440\u0430\u0443\u043d\u0434\u0430       processState,   \\* \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0443\u0437\u043b\u043e\u0432 IBFT     decision\u00a0 \u00a0 \u00a0 \u00a0 \\* \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u0430\u044f \u2013 \u0445\u0440\u0430\u043d\u0438\u0442 \u043f\u0440\u0438\u043d\u044f\u0442\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435<\/code><\/pre>\n<p>\u0412 IBFT \u0435\u0441\u0442\u044c \u0447\u0435\u0442\u044b\u0440\u0435 \u0442\u0438\u043f\u0430 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u0443\u0437\u043b\u044b: <code>PRE-PREPARE<\/code>, <code>PREPARE<\/code>, <code>COMMIT<\/code> \u0438 <code>ROUND-CHANGE<\/code>. \u041f\u0435\u0440\u0432\u044b\u0435 \u0442\u0440\u0438 \u0438\u043c\u0435\u044e\u0442 \u0432\u0438\u0434 <code>&lt;message-type, \u03bb, r, value&gt;<\/code>, \u0433\u0434\u0435 <code>\u03bb<\/code> \u2014 \u043d\u043e\u043c\u0435\u0440 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430, <code>r<\/code> \u2014 \u0442\u0435\u043a\u0443\u0449\u0438\u0439 \u0440\u0430\u0443\u043d\u0434, \u0430 <code>value<\/code> \u2014 \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435; \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u0441\u0435\u0445 \u0442\u0430\u043a\u0438\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0431\u0443\u0434\u0435\u043c \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0432 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 messages. \u0421\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 <code>ROUND-CHANGE<\/code> \u043f\u0440\u0435\u0434\u043d\u0430\u0437\u043d\u0430\u0447\u0435\u043d\u044b \u0434\u043b\u044f \u0441\u043b\u0443\u0447\u0430\u044f \u0441\u043c\u0435\u043d\u044b \u0440\u0430\u0443\u043d\u0434\u0430 \u0438 \u0438\u043c\u0435\u044e\u0442 \u0432\u0438\u0434 <code>&lt;ROUND-CHANGE, \u03bb, r, pr, pv&gt;<\/code>, \u0433\u0434\u0435, \u043f\u043e\u043c\u0438\u043c\u043e \u043d\u043e\u043c\u0435\u0440\u043e\u0432 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0438 \u0440\u0430\u0443\u043d\u0434\u0430, \u043f\u0435\u0440\u0435\u0434\u0430\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435: <code>pr<\/code> (prepared round) \u2014 \u043d\u043e\u043c\u0435\u0440 \u0440\u0430\u0443\u043d\u0434\u0430, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0443\u0437\u0435\u043b \u043f\u043e\u043b\u0443\u0447\u0438\u043b \u043a\u0432\u043e\u0440\u0443\u043c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 <code>PREPARE<\/code>, \u0438 <code>pv<\/code> (prepared value) \u2014 \u0432\u0435\u043b\u0438\u0447\u0438\u043d\u0430, \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u043d\u0430\u044f \u0432 \u044d\u0442\u0438\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f\u0445.<\/p>\n<p>\u0412 \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 IBFT \u0435\u0441\u0442\u044c \u043f\u044f\u0442\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f: \u043d\u043e\u043c\u0435\u0440 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430, \u043e\u0442\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0438\u0437 \u043d\u043e\u043c\u0435\u0440\u0430 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0430 \u0432 \u043d\u043e\u043c\u0435\u0440\u0435 \u0442\u0435\u043a\u0443\u0449\u0435\u0433\u043e \u0440\u0430\u0443\u043d\u0434\u0430, <code>pr<\/code>, <code>pv<\/code>, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435. \u0421\u0442\u043e\u0438\u0442 \u0443\u043f\u043e\u043c\u044f\u043d\u0443\u0442\u044c, \u0447\u0442\u043e \u044f \u0441\u0442\u0440\u043e\u0438\u043b \u043c\u043e\u0434\u0435\u043b\u044c \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043d\u043e\u043c\u0435\u0440\u0430 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u043e\u0432 \u0432\u0435\u0437\u0434\u0435 \u0431\u0443\u0434\u0443\u0442 \u043e\u043f\u0443\u0449\u0435\u043d\u044b.<\/p>\n<p>\u041e\u043f\u0438\u0448\u0435\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430. \u0412\u0441\u0435 \u0443\u0437\u043b\u044b \u043d\u0430\u0445\u043e\u0434\u044f\u0442\u0441\u044f \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u0440\u0430\u0443\u043d\u0434\u0435, \u0430 \u043b\u0438\u0434\u0435\u0440 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <code>PRE-PREPARE<\/code> \u0441 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043f\u0440\u0435\u0434\u043b\u0430\u0433\u0430\u0435\u043c\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c<em> <\/em><code>v<\/code>.<\/p>\n<pre><code>Init ==   <\/code><\/pre>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-443219","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/443219","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=443219"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/443219\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=443219"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=443219"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=443219"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}