【OSS】Microsoft、スマートコントラクト検証ツール「VeriSol」をオープンソース公開---高カバレッジの記号テストをサポート

Microsoftは、スマートコントラクト検証ツール「VeriSol」をオープンソース公開した。

「VeriSol」とは

「VeriSol(Verifier for Solidity)」はスマートコントラクト用の正式な検証および分析システムのプロトタイプを作成するためのMicrosoft Researchプロジェクト。

→GitHub　→microsoft/verisol

プログラミング言語「Solidity」を利用

「Solidity」は、Ethereumプラットフォームでスマートコントラクトを実装するための高級言語で、「静的型付け」「コントラクト指向」などの特徴を持つ。

→GitHub　→ethereum/solidity

「VeriSol」は、Solidityプログラムのセマンティクスを正式な中間検証言語「Boogie」にエンコードし、Boogie検証ツールチェーンを活用し拡張することによって動作する。

高カバレッジの記号テストをサポート

「VeriSol」は、反例の痕跡を自動的に見つけるための高カバレッジの記号テストをサポートしている。

また、自動的に正確さの証明を実行できる。

以上、下記URLからの要約
https://www.microsoft.com/en-us/research/blog/researchers-work-to-secure-azure-blockchain-smart-contracts-with-formal-verification/?ocid=msr_blog_verisol_tw