The argument for formal verification has always been that it catches the bugs static analysis misses and tests don’t exercise. The argument against it has been that writing proofs is slower than writing code, and the toolchain friction rarely justifies the cost. That tradeoff is shifting.
Bend 2 is a programming language built around the assumption that AI agents write the code and humans demand the proofs. The mechanism is a LAWS.bend file where you declare invariants — “this function never panics,” “this counter never goes negative,” “this state never transitions unless explicitly unlocked” — and the compiler refuses to accept any implementation that can’t produce a formal proof those laws hold. The proof checker is said to run in under a second, which matters: real-time feedback during an agentic edit loop requires the verification cycle to be fast enough not to break flow.
Beyond verification, Bend 2 aims at performance. It compiles to native code targeting C-level speeds on single cores and CUDA-level throughput via automatic GPU parallelization. The parallelism is structural — divide-and-conquer operations fan out across available cores without manual threading or kernel authoring. The syntax is Python-like, which is the accessible choice for a language that wants to be written by LLMs.
Being clear-eyed matters here: Bend 2 has seven commits and the README says “BEND IS YOUNG. EXPECT BUGS.” This is not production tooling. Whether the claimed performance and proof-checking speed survive contact with non-trivial programs is unknown. The GPU story in particular — automatically turning arbitrary code into efficient CUDA kernels — is a harder problem than it sounds; previous attempts have often produced correct-but-slow parallelism.
What’s worth taking seriously is the framing rather than the current implementation. As coding agents become more capable and operate with broader context windows and longer autonomous loops, the failure mode shifts from “agent writes wrong code” to “agent writes plausible-looking wrong code that passes review.” A human reviewer’s attention is the bottleneck, and it scales poorly. Compile-time proofs don’t scale the same way — they’re automated, deterministic, and run at merge time regardless of reviewer load.
This is what languages like Lean, Idris, and Dafny have offered for years. The difference Bend 2 proposes is making the law-declaration ergonomic and the checking fast enough to integrate into the edit cycle rather than treating verification as a separate offline analysis. Whether that actually works will show up in the next few hundred commits, if they arrive.
The deeper question Bend 2 forces is what “correctness” means when agents are the authors. Tests verify that a program matches the test writer’s expectations. Proofs verify that the program satisfies a formal spec. Neither is complete — specs can be wrong, invariants can be underspecified — but the discipline of stating invariants explicitly tends to surface underspecification earlier. In a world where the code author is an agent that confidently writes plausible implementations, the habit of declaring what must always be true is worth more than it used to be.