Vera: LLMが書くために設計されたプログラミング言語

Apr 29, 2026 · coding ai web · Source ↗

要点まとめ

VeraはDe Bruijn型インデックスで変数名を廃止し、Z3で検証済みのコントラクトを義務付け、WebAssemblyにコンパイルすることで、LLM生成コードを意味論的な信頼ではなく構造的な検査の対象にする。

変数名なし：@Int.0 が直近のInt束縛、@Int.1 がその前の束縛を指し、shadowingや誤認識といったLLM特有の命名エラーを排除する。
全関数に requires()、ensures()、effects() 句が必須。Tier 1コントラクトはZ3 SMTソルバーが静的に証明し、決定不能なケースはランタイムで対処する。
エフェクト型は構造的なケイパビリティ証明：LLMを呼び出す関数は effects(<Inference>) を宣言しなければならず、それを許可しない呼び出し元はコンパイル時に呼び出し不可となる。
コンパイラの診断はmachine-readable：安定したエラーコードE001〜E702、--json によるJSON出力、各エラーに具体的な修正例が含まれており、対象は人間ではなくモデル。
VeraBenchの初期結果：Kimi K2.5はVeraで run_correct 100%を達成（Python 86%、TypeScript 91%）。50問・5階層のベンチマークで3モデルがTypeScriptを上回る。

名前なし構文がLLMに有利か不利かで意見が割れている。Go・Javaのような冗長で明示的な言語の方がLLMは高性能であり、新しいメンタルモデルを要する構文は逆効果だという主張もある。
最も同意を集めたのはエフェクト型システム：コンパイル時に型付きケイパビリティ証明を行うことで、エージェント生成コードがIOやネットワーク呼び出しを行えないことを実行前に検証でき、命名の議論とは独立したサンドボックス上の実用的価値がある。
構造的参照がLLMエラーを減らすという実証的主張に疑問の声もあり、改善を示す対照ベンチマークがない以上、単なる難読化に過ぎないとするコメントも存在する。

@unignorant: エフェクトシステムにより実行前のケイパビリティ証明が可能になる——「IOができないことがわかる」——ため、エージェントコードを内容確認なしでサンドボックス化できると指摘。
@danpalmer: 名前なし構文は裏目に出る可能性があると主張。LLMはページを読むだけでなくメンタルモデルの保持が必要なHaskell的抽象化では性能が低下するとする。
@ginko: 構造的参照が変数名よりもLLMコード生成で優れていることを示すエビデンスを求め、現在の根拠は説得力に欠けると指摘。