プログラミング言語および形式手法を専門とする独立研究グループ
Inferaraの目標は、Web3開発者向けに形式検証をより利用しやすいものにすることです。
私たちは、自動定理証明器1,2がコードのエラーを発見するための最も強力なツールであることを知っています。しかし、大学以外では、ほとんど誰もそれを使用していません。
そこで、私たちは以下を目指します：
- 自動定理証明器を開発者が利用しやすいものにする
- スマートコントラクトの安全性を向上させる
- 次の数百万ドル規模のハッキングを未然に防ぐ
私たちは、成果をオープンソースとして公開しているため、皆様のご支援を必要としています💌
Web3向けに設計された初の開発者に優しい形式仕様言語。
Inferenceを使えば、数学の博士号がなくても、スマートコントラクトの性質を指定し、形式的に証明することができます。
仕組み
flowchart LR
Inference --> WAT
WAT --> WASM
WASM --> V;
Inferenceのコンパイルプロセスは、以下のステップから構成されています：
- InferenceコードをWebAssembly Text (WAT)にトランスパイルする
- WATをWebAssembly (WASM)にコンパイルする
- WASMをV（証明支援コード）に変換する
graph TD
A[プログラム]
PA[証明]
A -->|帰納的プログラムシミュレーション| PA
PA --> B
PA --> C
subgraph OC[動作コンテキスト]
B[最終マシン状態]
end
subgraph LC[論理コンテキスト]
C[証明すべき定理のリスト]
end
C -.-> |状態が到達可能であることを証明：トラップがなく、ガス切れなど| B
C --> H[Hummer]
C --> S[Inferara tactics]
S -.-> H
H -.-> S
S --> D([✅ 正しさの証明書])
H --> D;
Inferenceは、Inferaraの非決定的抽象機械実行に関する研究に基づいた形式仕様プログラミング言語です。詳細については、論文をご覧ください。