Bend: a language that blocks AI mistakes with proofs

Bend arrives with a one-line pitch: a fast language that blocks AI mistakes through proof, combining C speed, CUDA parallelism, Lean proofs and Python syntax. The project's framing is that in a post-AGI economy people will eventually stop reading and writing code but still need an unambiguous way to tell the machines what to build. Laws, the site argues, express intent more precisely than natural language; proofs verify that a model implemented the intent correctly; and a fast compiler runs the result at speed.

Fast to run, fast to check

Bend compiles to native code. On a single core the site claims performance close to C, and the same binary spreads across sixteen cores or a GPU, running up to a hundred times faster than one core. Speed matters on the checking side too: Bend's type checker is a proof checker in the tradition of Lean and Rocq, systems whose checks can take minutes on a mid-sized codebase. Bend takes a second at most, the site says, which is what makes it plausible for an agent to verify its work after every change.

Parallelism without threads or kernels

There are no threads, no locks and no kernels to write. A programmer splits the work in two and the language spreads the calls over every core it can find, then joins the results. The demo shows a power-of-two computation running on 4,096 GPU cores.

Laws as AGENTS.md backed by proof

Bend's answer to trusting code nobody read is to demand a proof. Laws are declared in a file named LAWS.bend, and after that, the site claims, no agent can ship a line that breaks them. The example is a game rule stating that no sequence of moves leads to victory, written as a law over an arbitrary list of moves, replaying the board from the start and asserting that it is never won. The companion PROOF.bend, which the AI writes, establishes that the law holds. In the illustration a wrap-around board feature shipped a live bug; with the law declared, the agent had to retry until it proved the constraint held. Merging a bug becomes, in the site's words, mathematically impossible — it is a theorem.

Getting started

Installation is a single shell command, after which the instructions are aimed at coding agents: add a short block to AGENTS.md telling the agent to run bend guide, keep important rules in LAWS.bend, run bend PROOF.bend before every commit, and parallelize wherever possible. The site suggests asking for laws around anything that must never break, working back-end first on Linux or macOS. Bend is young, it warns, so bugs are expected and should be reported as issues; further detail lives in the language guide on GitHub and in two papers, one on the affine dependent type theory at Bend's core and one on a parallel runtime for CPUs and GPUs.