Bend：CPUとGPU上でAIのミスを防ぐ証明検証済み言語

Bendは、AIが生成したコードを対象としたコンパイル型の並列言語です。その核心的な主張は、読まない出力を信用するのではなく、LAWS.bendファイルに法則を宣言し、マージ前にエージェントにその証明を要求するというものです。

この売り文句は他のAIコーディングツールと同じに聞こえますが、仕組みが異なります。Bendの型チェッカーは証明チェッカーであり、LeanやRocqと同じ考え方です。Bendが強調する違いは速度です。これらのチェッカーは中規模のコードベースでは数分かかることがありますが、Bendは最大1秒で済むと主張しており、エージェントは変更のたびにチェックを実行できます。

速度の源泉

• ネイティブコードにコンパイル。シングルコアでほぼC並みの速度。
• 同じバイナリが16コアまたはGPUにスケール。ドキュメントではシングルコア比で最大100倍高速と主張。
• 並列化は自動。作業を2つに分割すると、Bendが呼び出しをコアやGPUコアに分散し、その後結合します。スレッドもロックもカーネルコードも不要。

サイトでは、4,096個のGPUコアで実行されるpow2.bendの例が示されています。

法則と証明モデル

LAWS.bendに法則を書きます：

# LAW: no move sequence leads to victory.
law you_cant_win : for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False

次にエージェントがPROOF.bendに対応する証明を書きます：

# PROOF: you_cant_win holds.
def Laws.you_cant_win (moves):
    # ... written by the AI

法則が宣言されると、サイトはエージェントがそれを破る行をマージできないと主張します。デモではゲームを使用：Claudeにボードをラップアラウンドさせるよう依頼します。LAWS.bendがなければ、バグはマージされて出荷されます。あれば、エージェントは証明を構築するまで再試行しなければなりません。ソースの表現では、バグのマージは「数学的に不可能」になります。

セットアップ

インストール：

curl -fsSL https://bend-lang.com/install.sh | sh

次に、エージェントが何をすべきか分かるように、このブロックをAGENTS.mdに追加します：

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

Bendは本質的にLAWS.bendを証明に裏打ちされたAGENTS.mdとして扱います。「ミスを犯すな」が型チェックされるのです。

ソースからの注意点

ドキュメントは率直です：Bendは若く、バグを想定し、報告してください。バックエンドで最もよく機能し、LinuxとmacOSを対象としています。コアは2つの論文に裏打ちされています — BendTT（アフィン依存型理論）とBendRT（並列CPU/GPUランタイム）。

対象者

エージェントに読まないコードを出荷させるチーム、特に「残高は決して負にならない」といったルールをコードレビューではなく強制する必要があるバックエンドサービス。