Runtime Verificationとアルゴランド、アルゴランドのスマートコントラクト・エコシステムのためのフォーマル・ツール構築のための新たなエンゲージメントを発表
投稿日: 2020年7月28日 投稿者: Musab Alturki
この度、Runtime Verificationはアルゴランド財団からアルゴランド・スマートコントラクトのためのフォーマルなセマンティック・フレームワークを開発するための助成金を授与されたことをお知らせします。この助成金は、最近開始された2億5000万ALGOエコシステム助成プログラムの一部で、アルゴランド・エコシステムの研究開発を支援することを目的とした複数年プログラムです。アルゴランドのスマートコントラクト・アーキテクチャの未来を形成し、成長する開発者コミュニティをサポートするために、アルゴランドと協力する機会を得たことを非常にうれしく思います。私たちは以前、アルゴランドとの契約において、プラットフォームのコンセンサス・プロトコルの安全性をフォーマルにモデル化し、検証することに成功しており、この新しい契約において得られた知識と経験を活用することを楽しみにしています。
アルゴランドとの新たな契約を通じて、私たちの目標は、「Kフレームワーク」を使用してアルゴランド・スマートコントラクトの高度なアーキテクチャのためのフレームワークを開発することです。このフレームワークは、スマートコントラクトの開発、実装、テスト、検証に対するフォーマルなセマンティック・アプローチを促進するものです。これは、スマートコントラクト開発者がアルゴランド・プラットフォーム上で安全で信頼性の高いアプリケーションを構築できるようにする、正しい構築によるスマートコントラクト・ツールを開発するための基礎を築くのに役立ちます。また、将来的にアーキテクチャをさらに進化させるための土台となります。
このフレームワークの中心は、Blockstack Clarity言語を応用したアルゴランド・スマートコントラクト言語と、ブロックチェーンとのインターフェースのKによるフォーマルな定義です。また、この形式化には、アルゴランドの取引ロジックと、アルゴランドのオンチェーン取引実行承認言語（TEAL： Transaction Execution Approval Language）のセマンティクスが含まれます。このフレームワークは、システムの実行可能なドキュメント、プログラムの実行とデバッグのための言語インタプリタと効率的な参照実装、モデルベーステストとセマンティックカバレッジツール、静的解析ツール、記号実行エンジン、到達性解析とモデル検査ツールなどの多様なツールを自動的に生成するために使用できる数学的に十分に根拠のある曖昧でない定義が可能になります。
私たちRuntime Verificationは、このKセマンティクス・ベースのアプローチを開拓し、特にブロックチェーン空間における言語設計、実装、検証への適用において、学術的かつ商業的な経験を豊富に有しています。Kベースの正式モデリングおよび検証サービスの提供に加え、これらのサービスの一部を、Ethereumにおける高保証スマートコントラクトを定義するためのフォーマル・システムであるFireflyなど、コミュニティが使用できる製品に変換しているのです。今回の契約は、アルゴランド・プラットフォームでそのような製品を開発するための最初のステップと位置づけています。
元記事：https://runtimeverification.com/blog/runtime-verification-and-algorand-announce-a-new-engagement-to-build-formal-tools-for-algorands-smart-contract-ecosystem