Elrond сотрудничает с Runtime Verification, чтобы вывести смарт-контракты на новый уровень

  • HLCS 

Источник · Перевод автора

Научно-исследовательская группа Elrond будет тесно сотрудничать с Runtime Verification для дальнейшей разработки K-инфраструктуры и ее способности генерировать виртуальные машины с правильной конструкцией для блокчейна.

Elrond, недавно запущенная публичная сеть блокчейнов на основе шардинга, объявила о новом соглашении о сотрудничестве с Runtime Verification для исследований и разработок в основных областях методов формальной верификации.

Elrond использует K Framework, разработанный Григором Розу (Grigore Rosu) в НАСА и в Университете Иллинойса в Урбане, в качестве основы для всех своих смарт-контрактных языков.

Григор продолжил разработку K Framework вместе со своей командой в Runtime Verification, которая специализируется на формальных методах.

Опираясь на это, Elrond разработал внутреннюю серверную часть GO для интеграции виртуальной машины IELE, которая разработана командой проверки времени выполнения и полностью основана на K Framework. Elrond также работает над интеграцией KEVM и WASM аналогичным образом. Построение виртуальных машин с использованием K Framework дает Elrond доступ к мощным инструментам формальной проверки.

Посредством инициативы в области исследований и разработок между Elrond и Runtime Verification, Elrond стремится вывести умные контракты на новый уровень и создать бэкэнд GO, разработанный Elrond для K Framework, с открытым исходным кодом и доступны для широкой публики.

Другими участниками и сторонниками проверки времени выполнения являются Ethereum, Algorand, IOHK, Casper, Maker DAO, Gnosis, Toyota и многие другие.

«Мы в Runtime Verification очень рады видеть приверженность Elrond не только использовать, но и вносить вклад в развитие базовой инфраструктуры K Framework. Хотя «формальная проверка» теперь является модным словом в блокчейн-сообществе, на самом деле, немногие блокчейн-компании действительно понимают критическую, почти отчаянная необходимость формальной спецификации и проверки смарт-контрактов. И еще меньше людей понимают, что это начинается с формального моделирования языков программирования и виртуальных машин, и что инструменты формального анализа также имеют тенденцию к ошибкам, если они не получены из таких формальных моделей. Elrond берет безопасность в глубине души и следование самым известным методам обеспечения безопасной и надежной работы их блокчейна». — Григор Розу (Grigore Rosu), генеральный директор (CEO) Runtime Verification

«Elrond значительно улучшил блокчейн-пространство, установив новые стандарты производительности с точки зрения пропускной способности и скорости выполнения. В дополнение к производительности, мы считаем, что инструменты разработчика и меры безопасности, такие как формальные методы проверки, полезны для разработчиков. Благодаря партнерству с Runtime Verification. Мы намерены повысить стандарт безопасности, добавив формальную верификацию в наши смарт-контракты, в то же время интегрировав К-платформу для поддержки нескольких виртуальных машин и языков смарт-контрактов одновременно», — Бениамин Минку (Beniamin Mincu), генеральный директор (CEO) Elrond