Bend turns its type checker into a proof checker for AI-written code

Bend is a new programming language built around the idea that code written by AI agents should be verified by proof rather than read. Its type checker is also a proof checker, in the manner of Lean and Rocq. The difference the team stresses is speed: those tools can take minutes on a mid-sized codebase, while Bend is said to take at most a second, so an agent can run a check after every change.

Laws that cannot be broken

Rules live in a file called LAWS.bend. Once a law is declared there, no AI can ship a single line that violates it. In the demonstration described on the project site, a bug reaches production without LAWS.bend; with the file in place, the AI has to retry until it proves the law holds. Merging a bug becomes mathematically impossible, the team writes, because it is now a theorem. They describe the approach as AGENTS.md backed by proof.

One core, sixteen cores, or the GPU

Bend compiles to native code. On a single core it runs nearly as fast as C, and the same binary also runs on sixteen cores or on the GPU, reportedly up to a hundred times faster than one core. There are no threads, locks or kernels to write: you split the work in two and Bend spreads the calls over every core it finds, then joins them back. One example shows pow2 running on 4,096 GPU cores.

The full language is documented in GUIDE.md, which the bend guide command prints. Two papers cover the internals: BendTT, an affine dependent type theory at the core, and BendRT, the parallel runtime for CPUs and GPUs. The project is young, works best on the back end on Linux and macOS, and the team asks users to report bugs. Details at the project site.