ベラ：機械が記述するためのプログラミング言語です。

Vera（ヴェーラ）は、大規模言語モデル（LLM）によって書かれることを意図して設計されたプログラミング言語です。その名前は、「真理」を意味するラテン語の veritas に由来します。この言語で記述されたプログラムは WebAssembly にコンパイルされ、コマンドラインやブラウザ上でも実行可能です。

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

変数の名前（イデントフィカ）を使用しません。

@Int.0

は最新のスロット（結合子）を、

@Int.1

はそれ以前のものを指します。

requires

クローズはコンパイラが各呼び出し場所でチェックする前置条件です。

ensures

クローズは SMT ソルバによって静的に証明される後置条件です。この関数は「純粋」であり、あらゆる種類の副作用を持ちません。これらのいずれかが満たされない場合、コードはコンパイルされません。

なぜですか？

プログラミング言語は常にその利用者と共進化してきました。アセンブリ言語はハードウェアの制約から生まれ、C 言語はオペレーティングシステムから、Python は生産性要件から発展しました。もしモデルがコードの主著者となるのであれば、言語もそれに適応するはずです。

証拠が示唆しているのは、モデルが直面する最大の課題は構文ではなく、スケールにおける「整合性（coherence）」の欠如です。モデルはコードベース全体にわたる不変式の維持、変更の波及効果への理解、そして時間経過に伴う状態に関する推論において苦労します。彼らは局所的な妥当性を最適化するためのパターン Matcher に過ぎず、システム全体を心に留めたアーキテクトではありません。実証文献によれば、モデルは誤解を招く命名の選択、不適切な名の再利用、どの名がどの値を指すかを失うといった命名関連のエラーに特に脆弱であることが示されています。

Vera はすべてを明示的かつ検証可能にすることでこの問題を解決します。モデルが正しい必要はなく、チェック可能であればよいのです。名前が構造的参照によって置換されます。契約は義務付けられ、効果は型付けされます。各関数は、コンパイラが実装に対して検証できる仕様書です。

設計に関する詳細な質問については FAQ を参照してください。変数の名前がない理由、何が検証されるか、Vera が Dafny/Lean/Koka/F* とどう比較されるか、そして設計決定の背後にある実証的証拠について詳しく解説されています。

Vera の外観

Vera ならではの特徴を示す 3 つの例です。完全な概要（契約、改悪型、代数データ型、効果、例外処理、再帰、Markdown、JSON、HTML、HTTP、LLM 推論）については EXAMPLES.md をご参照ください。

コンパイラが証明する契約

ゼロ除算はランタイムエラーではなく、タイプエラーです。コンパイラはすべての呼び出し場所で除算子（denominator）がゼロでないことを証明するためにチェックを行います。

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

明示的な効果

Vera はデフォルトで純粋です。LLM を呼び出す関数はその签名（シグネチャ）にそれを宣言しています。

<Inference>

を許可しない呼び出し元はこれを呼ぶことはできません。また

<Http>

を許可しない呼び出し元も同様です。両方の呼び出し元は完全な効果行（effect row）を宣言しなければなりません。

public fn research_topic(@String -> @Result<String, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Http, Inference>)
{
  let @Result<String, String> = Http.get(
    string_concat("https://search.example.com/?q=", @String.0));
  match @Result<String, String>.0 {
    Ok(@String) -> Inference.complete(
      string_concat("Summarise this research:\n\n", @String.0)),
    Err(@String) -> Err(@String.0)
  }
}

6 行のロジックだけです。签名がすべての手続き（パラメータ型、契約、効果宣言）を担うため、本体はパイプラインのように読み進められます。

VERA_ANTHROPIC_API_KEY=sk-ant-... vera run examples/inference.vera

で実際の例を実行できます。

エラーとは指示のこと

従来のコンパイラは人間向けに診断情報を生成しますが（期待されたトークン「{」など）、Vera はコードを書いたモデルに対して指示を生成します。各エラーには何が間違っているか、なぜ間違っているか、具体的なコード例での修正方法、そして仕様への参照が含まれます。

[E001] エラー: main.vera の 14 行目、1 カラム目

    {
    ^

  関数に契約ブロックが不足しています。Vera のすべての関数は、签名と本体の間に
  requires()、ensures()、および effects() クローズを宣言する必要があります。

  Vera はすべての関数が明示的な契約を持つことを要求しており、それによって各関数の
  振る舞いが機械的にチェック可能になります。

  修正方法:

    签名の後に契約ブロックを追加してください：

      private fn example(@Int -> @Int)
        requires(true)
        ensures(@Int.result >= 0)
        effects(pure)
      {
        ...
      }

  参照：第 5 章「関数の構造」セクション 5.1

すべての診断情報は安定したエラーコード（E001–E702）を備えており、

--json

フラグを使用して構造化された JSON として利用可能です。

はじめに

前提条件

• Python 3.11 以上
• Git
• Node.js 22 以上（オプション：ブラウザランタイムおよび適合性テストのために使用）

インストール

git clone https://github.com/aallan/vera.git
cd vera
python -m venv .venv
source .venv/bin/activate
pip install -e ".[dev]"

ワークフロー

• vera check

  —— パースと型チェック。

• vera verify

  —— Z3 を通じた契約検証——階層 1 の契約（決定的な算術、比較、論理演算、代数データ型、終止性）は自動的に証明され、Z3 で決定できない契約は階層 3 のランタイムチェックに委譲されます。

• vera run

  —— WebAssembly にコンパイルして実行。

# 関数 f を引数 42 とともに呼び出す
vera run file.vera --fn f -- 42

# ブラウザバンドルを出力する
vera compile --target browser file.vera

# Z3 + WASM を通じた契約駆動型のテスト
vera test file.vera

# カノニカル形式へフォーマット
vera fmt file.vera

# エージェントフィードバックループ用の JSON 診断情報
vera verify --json file.vera

# スロット解決テーブルを表示（どの @T.n がどのパラメータにマップするか）
vera check --explain-slots file.vera

# インストールされたバージョンを表示
vera version

vera compile --target browser

は、ビルドステップやバンドラなしで任意のブラウザ上で実行できる自己完結型バンドル（Wasm + JS ランタイム + HTML）を生成します。必須の適合性テストにより、コマンドラインランタイムとブラウザランタイム間の振る舞いの同一性が確保されます。

エディタサポート

• VS Code 拡張機能 —— シンタックスハイライトおよび言語設定
• TextMate バンドル —— Sublime Text および他の TextMate グラムマータ編集機でも互換性あり

エージェント向け

Vera は LLM エージェント向けに以下のファイルを同梱しています：

• SKILL.md —— 完全な言語参照書。構文、スロット参照、契約、効果、一般的なミステイク、および動作する例をカバーします。
• AGENTS.md —— どの AI エージェントシステム（Copilot, Cursor, Windsurf, カスタム等）向けの指示事項。Vera コードの記述からコンパイラでの作業までを網羅します。
• CLAUDE.md —— Claude Code 向けのプロジェクトオリエンテーション。主要なコマンド、レイアウト、ワークフロー、および不変式（invariants）を含みます。
• DE_BRUIJN.md —— Vera の型付きスロット参照に関する深い掘り下げ：学術的背景、演習例、交換律操作の罠、証明支援系および LLM コード生成研究との関連性を扱います。

Claude Code は、このリポジトリ内の SKILL.md と CLAUDE.md を自動的に発見します。他のプロジェクトの場合、スキルを手動でインストールしてください：

mkdir -p ~/.claude/skills/vera-language
cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md

他のモデルについては、システムプロンプトに SKILL.md を含めたり、ファイルアタッチメントとして提供したり、検索ドキュメントとして利用するかといった方法で取り扱ってください。このファイルは Markdown を読むことができる任意のモデルと互換性のある自己完結型のものです。

Vera コードを書くための必須ルール:

1. すべての関数は签名と本体の間に

   requires()

   、

   ensures()

   、および

   effects()

   を必要とします。
2. 結合子を参照するには

   @Type.index

   を使用します——

   @Int.0

   は最新の Int で、

   @Int.1

   はそれ以前のもの指します。
3. すべての効果を宣言してください——純粋関数の場合は

   effects(pure)

   、IO の場合は

   effects(<IO>)

   など。
4. 再帰的な関数は

   decreases()

   クローズを必要とします。
5. Match 式は排他的（exhaustive）である必要があります。

プロジェクトの状態

Vera は現在 v0.0.127 でアクティブに開発中で、コミット数 810 以上、リリース数 127、テスト数 3,638、コードカバレッジ 96%、適合性プログラム 82 つ、例プログラム 33 個、および 13 章の仕様を備えています。コンパイラがどのように構築されたかは HISTORY.md を参照してください。

参照コンパイラ（パーサ、AST、型チェッカー、契約検証器（Z3）、WASM コードジェネレータ、モジュールシステム、ブラウザランタイム、およびランタイム契約挿入）は動作しています。言語仕様は 13 章にわたって草案段階にあります。

提供された主要機能:

• 型付き De Bruijn インデックス（@T.n）
• 義務付けられた契約
• 代数効果（IO, Http, State, Exceptions, Async, Inference, Random）
• 改悪型（Refinement types）
• 制約付きジェネリクス（Eq, Ord, Hash, Show）
• 代数データ型
• パターンマッチング
• モジュール
• 組み込み関数 164 （文字列、配列、マップ、セット、小数、数学、JSON、HTML、Markdown、正規表現、Base64、URL など）
• 契約駆動型のテスト
• カノニカルフォーマッタ
• ブラウザランタイム
• 3 階層検証（Z3 静的、ガイダンス付き、ランタイムフォールバック）

次なるステップ: 「動作する言語」から「エージェントが実際に使用する言語」への道のり——ロードマップの詳細については、4 つの戦略的マイルストーンを記載した ROADMAP.md をご参照ください。旗艦目標は、契約によってコンパイル時にツールスキーマを保証する検証された MCP ツールサーバーの実現です。

VeraBench —— 5 つの難易度ティアにわたる 50 問の問題集——現在は 3 つのプロバイダ（v0.0.7）の 6 つのモデルをカバーしています。主たる結果：Kimic K2.5 は Vera で 100% の

run_correct

を達成し、Python（86%）および TypeScript（91%）を凌駕しました。3 つのモデルが TypeScript を超える点において Vera で優位に立ち、旗艦ティアは平均して Vera 93% vs Python 93% で実質的に同等性を示します。これらは単一実行の結果であり変動性が高いので、詳細については完全レポートをご参照ください。

既知のバグおよびオープンされた問題には、イシュートラッカーにて追跡が行われています。集約リストについては KNOWN_ISSUES.md をご参照ください。

プロジェクトの構造

vera/
├── SKILL.md                       # LLM エージェント向け言語参照書
├── AGENTS.md                      # どの AI エージェントシステム向けの指示事項
├── CLAUDE.md                      # Claude Code 向けのプロジェクトオリエンテーション
├── FAQ.md                         # 設計理由と比較に関する資料
├── EXAMPLES.md                    # コード例を含む言語ツアー
├── HISTORY.md                     # コンパイラの構築手順
├── ROADMAP.md                     # 展望的な言語ロードマップ
├── KNOWN_ISSUES.md                # 既知のバグおよび制限事項
├── DESIGN.md                      # 技術的決定と先行事例
├── TESTING.md                     # テスト参照（唯一の情報源）
├── CONTRIBUTING.md                # 貢献者のガイドライン
├── CHANGELOG.md                   # バージョン履歴
├── LICENSE                        # MIT ライセンス
├── spec/                          # 言語仕様（13 章）
├── vera/                          # 参照コンパイラ（Python）
│   ├── grammar.lark               # Lark LALR(1) グラムマータ
│   ├── parser.py                  # パーサモジュール
│   ├── ast.py                     # 型付き AST ノード定義
│   ├── transform.py               # Lark 解析ツリー → AST トランスフォーマ
│   ├── checker/                   # 型チェッカー（ミックスインパッケージ）
│   ├── verifier.py                # 契約検証器（Z3）
│   ├── codegen/                   # コード生成（11 モジュール）
│   ├── wasm/                      # WASM 変換（9 モジュール）
│   ├── browser/                   # ブラウザランタイム
│   ├── formatter.py               # カノニカルコードフォーマッタ
│   ├── errors.py                  # LLM 向け診断情報
│   └── cli.py                     # コマンドラインインターフェース
├── docs/                          # GitHub Pages サイト (veralang.dev)
├── editors/                       # VS Code 拡張機能 + TextMate バンドル
├── examples/                      # 33 の Vera プログラム例
├── tests/                         # テストスイート（TEStING.md を参照）
└── scripts/                       # CI および検証スクリプト

コンパイラアーキテクチャおよび内部については

vera/README.md

、テスト詳細については TESTING.md をご参照ください。

デザイン

DESIGN.md をご参照し、完全な技術的決定表（表現、参照、契約、効果、検証、メモリ、ターゲット、グラムマータ、診断情報、データ型、多形、コレクション、エラー処理、再帰、命名）および先行事例（Eiffel, Dafny, F*, Koka, Liquid Haskell, Idris, SPARK/Ada, De Bruijn, TLA+/Alloy）をご覧ください。

貢献

Vera に貢献する方法については CONTRIBUTING.md をご参照ください。コンパイラ内部については vera/README.md をご参照ください。

引用

Vera を研究で使用される場合は、以下の引用をご利用ください：

@software{vera2026,
  author = {Allan, Alasdair},
  title = {Vera: a programming language designed for LLMs to write},
  year = {2026},
  url = {https://github.com/aallan/vera}
}

ライセンス

Vera は MIT ライセンスの下で提供されています。すべての直接依存項は MIT または Apache-2.0 です。1 つの転送依存項（chardet、cyclonedx-bom を介して）は LGPL v2+ ですが、MIT 再配布と互換性があります。ライセンス準拠は CI で強制されます。

依存項	ライセンス	ロール
Lark	MIT	LALR(1) パーサジェネレータ
z3-solver	MIT	契約検証のための SMT ソルバ
wasmtime	Apache-2.0	WebAssembly ランタイム

Copyright © 2026 Alasdair Allan

ここに記述するソフトウェアおよび関連するドキュメントファイル（以下「ソフトウェア」）の複製を取得した任意の個人に対して、本ソフトウェアの使用、複製、変更、統合、公開、配布、サブライセンスおよび/または販売を行う権利を含む制限なく、ソフトウェアを扱うことを許可します。ただし、以下の条件が付属しています：

前掲著作権表示およびこの許諾表示は、ソフトウェアのコピーまたは実質的な部分を問わず、すべてに含まれていなければならない。

本ソフトウェアは「現状のまま」提供され、明示的又は暗黙のすべての保証、販売適格性、特定用途への適合性及び知的財産権侵害を含まないが限定されないものを含め、一切保証されません。また、契約または不法行為に基づき、ソフトウェアの使用およびその他の取引に起因するいかなる請求、損害賠償その他の責任につき著者又は著作権保有者は一切負いません。