EVMの形式的定義
概要
Yellow Paperは仕様記述の標準にしたがっておらず、曖昧さが残るため、プログラム検証に使えない。そもそも「実行可能なセマンティック」ではない。 eth-isabelle
LemによるEVMのspecの定義
Lemは仕様記述言語で、以下に変換される
Coq, Isabelle/HOL, HOL4, OCaml, HTML and LaTeX
LemによるEVMのセマンティックを、Isabelle/HOLに変換
CoqへのEVMのセマンティックの変換は不完全だった模様
Isabelleによるコントラクトの形式的検証
Isabelleによって形式的にspecificationを記述し、EVMのセマンティックを使ってEVMバイトコードを検証する
参考
Casper FFGの形式的検証に関する記事は消えている
その他
概要
K Framework自体の研究開発チーム(UIUC)とメンバー被ってたりするので大学発ベンチャー的な感じなのか?
Cardanoを開発するIOHKがKEVMとKIELEの開発を支援した模様 記事 F*によるEVMの形式的セマンティック