Bend: a proof-checked language that aims to make AI coding bugs unmergeable

Bend is a programming language pitched squarely at AI-generated code. Its central idea is a lightweight formal-verification workflow: developers write invariants in a LAWS.bend file, and the AI agent must produce a machine-checked proof (in PROOF.bend) that its code upholds them before anything can be committed. The example given is a game where a law asserts no sequence of moves can win; adding a ‘wrap-around’ feature that would normally introduce a bug instead forces the agent to retry until the proof holds. The claim is that merging a violation becomes mathematically impossible rather than a matter of testing or review.

The technical hook is that Bend’s type checker doubles as a proof checker in the tradition of Lean and Rocq, but is engineered to run in about a second rather than minutes, so an agent can re-verify after every edit. It uses Python-like syntax, compiles to native code at near-C single-core speed, and automatically parallelizes across many CPU cores or GPUs—advertised at up to 100x over a single core—without the developer writing threads, locks, or kernels. Two papers back the approach: BendTT, an affine dependent type theory for the core, and BendRT, the parallel CPU/GPU runtime.

The framing is unabashedly aimed at ‘vibe-coded’ and ‘post-AGI’ development, positioning formal proofs as the guardrail for code humans no longer read. That marketing gloss aside, the underlying pitch is a real one: pairing fast dependent-type proofs with automatic parallelism to make AI output verifiable rather than merely plausible. The project openly warns it is young, expect bugs, and works best on the back end under Linux and macOS—so the promise of provably correct AI code is aspirational for now, but the direction is worth watching.