aallan/vera

何を解決するか

モデルはスケールに応じて一貫性を維持することが難しく、状態についての推論や変数名の管理に苦労し、結果として名前関連のエラーが発生し、値の追跡が失われる傾向があります。Vera は、大規模言語モデルがコードを書くために特別に設計されたプログラミング言語であり、従来の変数名の代わりに構造的参照を使用し、コードが機械的に検証可能であることを保証するために契約を必須にしています。

動作方法

Vera は変数名の代わりに型付きスロット参照（例：@Int.0 は最新の整数バインディング）を使用します。SMTソルバー（Z3）を用いて、すべての呼び出しサイトで事前条件（requires）と事後条件（ensures）を静的に証明します。言語はデフォルトで純粋であり、効果（例：<Http> や <Inference>）は関数シグネチャで明示的に宣言する必要があります。プログラムは WebAssembly にコンパイルされ、コマンドライン、ブラウザ、または WASI Preview 2 コンポーネントとして実行可能です。

対象ユーザー

コードの主な作成者としてAIエージェントやLLMを使用する人、またモデルが命名の衝突なく生成しやすく、形式的に検証され、安全なコードを望む開発者。

特徴

型付きスロット参照：変数名の代わりに構造的参照を使用することで、名前エラーを排除します。
必須の契約：すべての関数は、コンパイラがZ3を用いて静的に証明する事前条件と事後条件を宣言しなければなりません。
明示的な効果型：副作用はシグネチャで明示的に型付けされ、不正な操作を防止します。
エージェント最適化診断：コンパイラエラーはモデル向けの指示として記述され、根拠と具体的な修正例を提供します。
設計段階から安全：文字列の発生元に関するルールを型チェックレベルで強制することで、SQLインジェクションなどの一般的な脆弱性を防止します。
マルチターゲットコンパイル：CLI、ブラウザ、WASI 0.2 ホストで実行可能な WebAssembly にコンパイルされます。