プログラミング言語と形式手法に特化した研究開発会社
Inferaraの目標は、エンジニアが形式検証をより利用しやすくすることです。
私たちは、自動定理証明器1,2がコードのエラーを発見するための最も強力なツールであることを知っています。しかし、大学以外では、ほとんど誰もそれを使用していません。
そこで、私たちは以下を目指します：
- 自動定理証明器をエンジニアが利用できるようにする
- ミッションクリティカルなソフトウェアの安定性とセキュリティの向上
- ソフトウェア障害、評判、物理的損害、金銭的損害の防止
Inferaraが設計・開発した、エンジニアフレンドリーな最初の形式仕様言語。
Inferenceを使えば、数学の博士号を必要とせずにソフトウェア プログラムのプロパティを指定して正式に証明できます。
Inferenceプログラミング言語に関する 1 ページのパンフレットをダウンロードしてください。仕組み
flowchart LR
Inference --> WAT
WAT --> WASM
WASM --> V;
Inferenceのコンパイルプロセスは、以下のステップから構成されています：
- InferenceコードをWebAssembly Text (WAT)にトランスパイルする
- WATをWebAssembly (WASM)にコンパイルする
- WASMをV（証明支援コード）に変換する
graph TD
SC -.->|コンパイル＆インクルード| A
PA[証明]
A -->|帰納的プログラムシミュレーション| PA
PA --> B
PA --> C
subgraph UC[ユーザーコンテキスト]
A[Inference仕様]
SC[スマートコントラクト]
end
subgraph OC[動作コンテキスト]
B[最終マシン状態]
end
subgraph LC[論理コンテキスト]
C[証明すべき定理のリスト]
end
C -.-> |状態が到達可能であることを証明：トラップがなく、ガス切れなど| B
C --> H[Hammer]
C --> S[Inferara tactics]
S -.-> H
H -.-> S
S --> D([✅ 正しさの証明書])
H --> D;
Inferenceは、Inferaraの非決定的抽象機械実行に関する研究に基づいた形式仕様プログラミング言語です。詳細については、論文をご覧ください。