GoKawiilNew language Bend uses formal proofs to stop AI coding agents from shipping bugs
Bend is a newly introduced programming language that compiles to native code, runs on multiple CPU cores or GPUs without manual threading, and includes a built-in proof checker similar to Lean and Rocq. Developers can write rules in a LAWS.bend file, and Bend will refuse to accept any AI-generated code change that violates those rules, checking each change in about a second. Its creators demonstrate this by showing an AI agent attempt to break a game's win condition, which Bend blocks until the AI produces a compliant fix.