【Vera深掘り】AIが書くために設計されたプログラミング言語がヤバすぎる

ねこまろだよ！今日は特別回。
「AIが書くために設計されたプログラミング言語」
そんなぶっ飛んだ発想のVera（ヴェラ）を
徹底的に深掘りするよ。

🔧 Veraってそもそも何？
🤯 LLMがPythonより正確に書ける
📝 コードはこんな感じ
🧠 LLM呼び出しが言語機能に組み込まれてる
✅ 3段階の検証システム
⚙️ 技術スペックまとめ
🐱 ねこまろ様的にどう思う？

🔧 Veraってそもそも何？

Vera（ラテン語で「真実」）は
人間じゃなくLLMが書くために設計された
静的型付き純粋関数型プログラミング言語だよ。

元天体物理学者のAlasdair Allanが開発して
2026年2月28日にMITライセンスで公開。
GitHub上で778コミット・111リリースと
開発がめちゃくちゃ活発なんだ。

普通の言語は「人間が読み書きしやすい」が目標だけど
Veraは「AIが正確なコードを出力しやすい」が目標。
発想が完全に逆なんだよね。

veralang.dev

🤯 LLMがPythonより正確に書ける

一番衝撃的なのがベンチマーク結果だよ。

VeraBench（50問・5段階）で
Kimi K2.5がVeraで正答率100%を達成。
同じモデルのPython 86%・TypeScript 91%を
大幅に上回ったんだ。

しかもVeraはどのLLMの学習データにも入ってない。
つまりゼロショットで100%正解ってこと。

なぜそんなことが可能かというと
Veraは「正しくないコードが書けない」設計だから。
コンパイラが全部チェックしてくれるんだよ。

github.com

📝 コードはこんな感じ

Veraのコードを見てみよう。
安全な割り算の関数はこうなるよ：

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{ @Int.0 / @Int.1 }

特徴的なのは3つ：

・requires()：引数の事前条件（0除算は型エラーに）
・ensures()：戻り値の事後条件（契約）
・effects()：副作用の宣言

変数名の代わりに@Int.0や@Int.1を使う。
これは「De Bruijn indices」という仕組みで
変数名の曖昧さをゼロにするためだね。
人間には読みにくいけどAIには最適なんだ。

🧠 LLM呼び出しが言語機能に組み込まれてる

Veraの一番ユニークな機能がこれ。
LLM推論が「言語のエフェクト」として
型システムに組み込まれてるんだよ。

public fn classify_sentiment(@String -> @Result)
  effects(<Inference>)

<Inference>エフェクトを宣言した関数だけが
LLMを呼び出せる設計になってるね。

Anthropic・OpenAI・Moonshotの
APIに標準対応してるよ。
「この関数はAIを使います」が
型レベルで保証される世界。すごくない？

✅ 3段階の検証システム

Veraのコンパイラは3段階で正しさを検証するよ。

第1段階：Z3による静的証明
数学的にコードが正しいことを証明する。
定理証明器Z3が自動で動くんだ。

第2段階：ガイド付き検証
Z3で証明できない部分を
契約ベースのテストで補完する。

第3段階：ランタイムフォールバック
実行時にも契約違反をチェック。
3重の安全網があるんだね。

エラーメッセージも特殊で
「何が間違い」「なぜ」「直し方のコード例」「仕様参照」の
4点セットで出力される。
AIが次の修正に使えるように設計されてるんだ。

⚙️ 技術スペックまとめ

・コンパイル先：WebAssembly（wasmtime）
・組み込み関数：122個（文字列・配列・JSON・HTML等）
・テスト：3,239テスト・カバレッジ96%
・エージェント対応：SKILL.md・AGENTS.md・CLAUDE.md同梱
・VS Code拡張あり
・非同期対応：Future型
・ライセンス：MIT

github.com