aallan/vera

解決する課題

LLMは、コードの一貫性の維持、大規模なコードベース全体にわたる不変条件の保持、および状態に関する推論に苦労することがよくあります。また、命名エラーや変数アイデンティティの喪失が発生しやすい傾向にあります。Veraは、変数名を構造的参照に置き換え、すべての関数に対して明示的で検証可能なコントラクトを要求することで、これらの問題に対処します。

仕組み

Veraは、コードの正確性を確保するために独自の方式を採用しています：

• 構造的参照: 変数名の代わりに、型付きの De Bruijn indices (例: @Int.0) を使用して、命名に関連するエラーを回避します。
• 必須コントラクト: すべての関数は、requires (事前条件)、ensures (事後条件)、および effects (副作用) を宣言する必要があります。
• 静的検証: SMTソルバ (Z3) が、コンパイル時にこれらのコントラクトが成立することを証明しようと試みます。
• 3層検証: コントラクトを静的に証明できない場合、コンパイラは実行時ガードを挿入し、サイレントな失敗が発生する前にエラーを捕捉します。
• エージェント中心の診断: エラーはLLM向けの指示として設計されており、問題の解決策となる根拠と具体的なコード例を提供します。

対象者

• LLMエージェント: この言語はAIモデルが記述することを特別に最適化しており、エージェントのワークフローに合わせて調整されたドキュメント (SKILL.md) と指示 (AGENTS.md) を備えています。
• AI駆動型システムを構築する開発者: モデルによって生成された高保証のコードを必要とする方々。

ハイライト

• CLI、ブラウザ、または WASI Preview 2 ホストでの実行のために WebAssembly にコンパイルされます。
• <Inference> や <Http> のような副作用を追跡するための明示的なエフェクトシステムを備えています。
• エディタサポートのための Language Server Protocol (LSP) を含んでいます。
• 従来の言語と比較して、Veraを記述するモデルの高い成功率を示すベンチマーク (VeraBench) を含んでいます。