Bend – A language that blocks AI mistakes via proof and runs on GPUs
Bend is a new programming language combining C-speed compilation, GPU parallelism, and Lean-style proofs that stop AI agents from merging code violating declared laws.
Bend is a programming language whose type checker acts as a proof checker, letting developers declare invariants in LAWS.bend that AI coding agents must prove with PROOF.bend before committing. It compiles to native code running near C speed on a single core and up to 100x faster across GPU cores, with automatic parallelism requiring no threads or locks. The project publishes two papers, BendTT (an affine dependent type theory) and BendRT (a parallel CPU/GPU runtime), and integrates with AGENTS.md workflows for AI-driven 'vibe coding'.
- Proof-checking type system verifies AI-written code against laws declared in LAWS.bend.
- Compiles to native code with near-C single-core speed and up to 100x faster on GPUs.
- Automatic parallelism spreads calls across CPU cores and CUDA GPUs without threads or locks.
- Ships with AGENTS.md integration so agents run proofs before committing changes.
Full article620 words · extracted from bend-lang.com · click to collapse
1.Install
curl -fsSL https://bend-lang.com/install.sh | sh2.Add this to your 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 possible3.Enjoy bug-free, fast vibe-coded apps!
a fast language that blocks AI mistakes via proof
C speed · CUDA parallelism · Lean proofs
In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.
With laws, our intents can be much more precise than natural language. With proofs, we can verify that the AI implemented our prompts correctly. And a fast compiler runs it at speed.
That's Bend - and nothing else.
1.Bend runs FAST.
Bend compiles to native code. On one core, it runs nearly as fast as C. The same binary also runs on sixteen cores, or on the GPU, running up to a hundred times faster than one core.
2.Bend compiles FAST.
Bend's type checker is a proof checker, as in Lean and Rocq. Those can take minutes on a mid-sized codebase. Bend takes a second at most, so an AI agent can check after every change.
3.Bend is PARALLEL.
No threads, no locks, no kernels to write. Split the work in two, and Bend spreads the calls over every core it can find, then joins them back. Now watch pow2 run on 4,096 GPU cores:
4.Bend BLOCKS mistakes - with proof
How can you trust code you never read? By demanding a proof. LAWS.bend is where you declare laws. From then on, no AI can ship one line that breaks them, ever. Watch it guard a game:
Law: winning is impossible
New feature:
“Claude, make the board wrap around”
Without LAWS.bend:
With LAWS.bend:
Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem.
LAWS.bend
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False{} # never leads to victoryPROOF.bend
# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... written by the AILAWS.bend is AGENTS.md backed by proof.
“Make no mistakes” is now type-checked.
Skeptical? Try breaking the game.
5.Get started.
5.1.Install
curl -fsSL https://bend-lang.com/install.sh | sh5.2.Tell your agent to use Bend
Add this to your 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 possibleThen, just say: "use Bend"!
5.3.Enjoy bug-free, fast vibe-coded apps!
Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is young: if anything goes wrong, ask it to open an issue. Bend works best on the back-end, on Linux and on macOS. Enjoy! <3
6.References.
Guide: GUIDE.md is the whole language; bend guide prints it.
Paper: BendTT, an affine dependent type theory, Bend's core.
Paper: BendRT, a parallel runtime for CPUs and GPUs, the VM.
Bend is still evolving. Expect bugs, and please report them.
Text extracted automatically; images, tables and formatting may be missing. Original: https://bend-lang.com/