セキュリティ、テスト、形式的検証

私たちは、重要なシステムの安全性と正確性を確保するための厳密なツールを構築している研究開発企業、Runtime Verificationです。私たちのチームは、K Frameworkで記述された、Ethereum Virtual Machine（EVM）の最も完全で実戦テスト済みの形式的セマンティクスであるKEVMを開発しました。 KEVMは単なる仕様ではなく、スマートコントラクトのシンボリックな推論、適合性テストの実行、ガス使用量の分析、プログラムのデバッグ、および正確性プロパティの形式的検証に使用できる実行可能な仕様です。Ethereumの完全なテストスイートに合格しており、SolidityとVyperの両方のERC-20トークンを含む、価値の高いコントラクトの検証に使用されています。最近、Pectraアップグレードをサポートするためにセマンティクスを更新しました。 KEVMは、Solidity向けの形式的検証ツールであるKontrolによって積極的に活用されています。Kontrolは、Optimism、Ethereum Foundation、Lido、UniswapなどのEVMエコシステムの主要チームや、より広範なEthereumコミュニティのセキュリティ研究者や監査人によって積極的に使用されています。 私たちはこのリポジトリを積極的に維持し、Ethereumのプロトコルの進化に貢献し、Foundryなどの開発者ツールと統合しています。KEVMを通じて、証明可能で安全なスマートコントラクトインフラストラクチャにおいて可能なことの限界を押し広げています。

Branching Tree Technique (分岐ツリー手法) に基づくスマートコントラクトのテストジェネレーターです。

Runtime Verificationは、10年以上にわたりオープンソースの形式的検証ツールの最前線に立ってきました。私たちの汎用的なアプローチにより、複数のブロックチェーンで当社のテクノロジーを使用できます。KEVMはすべてのEVMベースのスマートコントラクトに検証インフラストラクチャを提供しますが、KontrolはSolidityスマートコントラクトの形式的検証への参入障壁を大幅に下げます。 私たちのツールは完全にオープンソースであり、Optimismエコシステムのすべての開発者が追加費用なしで自由にアクセスできます。 KEVMは、K Frameworkで記述されたEVMの実行可能な形式的セマンティクスです。KEVMはすべてのEthereum適合性テストに合格しており、K Frameworkを使用してスマートコントラクトを形式的に検証するためのエントリーポイントです。ただし、プレーンなKEVMを使用するには、仕様を記述するためにK Frameworkに関する特別なトレーニングが必要です。さらに、これらの仕様は非常に冗長になる可能性があり、記述の難易度が高くなります。 Kontrolは、開発者がスマートコントラクトの形式的仕様をFoundryのプロパティテストとして直接記述できるようにすることで、この問題を解決します。これらのテストは自動的にKEVM仕様に変換され、すべての検証保証を維持しながら、開発者エクスペリエンスを大幅に向上させます。