Bend 2 Makes AI Agents Prove Their Code in 484 Lines; SPARK Needed No Proof File

TL;DR

Bend 2 went public on September 17 with a pitch aimed squarely at anyone who lets an agent write code. You declare invariants in a file called LAWS.bend, and the compiler refuses an edit unless the AI produces a machine-checked proof that the laws still hold. Its author, Victor Taelin, sums it up in one line in the README: LAWS.bend is AGENTS.md backed by proof.

The checker is genuinely fast. On the repo's own pinned numbers, Bend checks a 12,800-definition file in 0.295s where Lean needs 36.177s and Rocq needs 5.985s. The runtime targets CPU and GPU from one source, and the pow2(20) demo splits until one task sits on each of 4,096 GPU cores, with no threads or locks in your code.

Then somebody rebuilt the flagship demo in SPARK, an open-source formal verification language for Ada, and the prover discharged every check without a proof file at all. That comparison, not the launch, is the useful part.

What LAWS.bend actually does

Bend is Apache-2.0, installs from a one-line shell script, and has Python-shaped syntax on top of a dependent type theory. The part that matters for agent workflows is a two-file convention.

In LAWS.bend you write claims. The README's examples are the sum of all balances must be zero, players can never pass through solid walls, list_sort() must always return ascending numbers, array_set() may never be called out of bounds. In PROOF.bend, the AI fills each one. An unfilled law is a compile error, so bend PROOF.bend is the entire verification step.

The onboarding instruction is four lines pasted into your AGENTS.md: run bend guide to learn it, keep important rules in LAWS.bend, run bend PROOF.bend before committing, parallelize where possible. Then you say "use Bend" and the agent does the rest.

A law is not a test

This is the idea worth stealing even if you never install Bend. A test samples. It runs the inputs someone thought of, and a new feature that breaks an unthought-of case sails through green. A law quantifies over every input, and the proof has to cover all of them or the build fails.

A test is a guard checking a few bags at random. A law is a doorway the contraband does not fit through.

The homepage demo makes it concrete with a grid game whose only law is that winning is impossible. Ask the AI to make the board wrap around and, without the law, the player wraps past the edge, grabs the flag, and the bug merges. With the law, the AI cannot merge that edit. Taelin notes on Hacker News that the fix it picked, a wall on the far edge, was one of several it could have chosen.

The checker really is fast

Bend's compiler doubles as a proof checker, and the speed claim is the load the rest of the pitch rests on. If proving costs minutes per edit, no agent loop survives it.

The repo pins its own measurements. On an Apple M4 Max, checking a file of 12,800 definitions takes Bend 0.295s. Rocq takes 5.985s, Lean takes 36.177s, and Agda and Isabelle both blow past a 300-second cutoff. On a 3,200-proof file, Bend takes 0.834s and Lean times out.

One honest note the repo makes itself: the Isabelle row was carried over from an earlier run and not re-measured, and the team says it does not have as many checker benchmarks as it would like.

The counter-experiment

A day after launch, Liam Powell published Bend 2 and the Vibe-Coding Trap, and it is the most useful thing written about the project so far.

His observation starts with volume. Bend's own demo needs a LAWS.bend file just to state that the player can never reach the flag, and a PROOF.bend file to discharge it. Powell counted 58 and 442 lines on September 18. As of September 20 the files stand at 68 and 484, because the repo is moving fast.

Then he did the thing more critics should do. He told an LLM, with no further guidance, to recreate the same demo in SPARK. He got roughly 50 lines of Ada package spec and body carrying both of Bend's laws as postconditions, ran GNATprove, and got back a single line: all checks proved, 12 checks. No proof file. The solver built the argument.

Powell's broader point is sharper than the line count. The words "formal verification" appear nowhere on Bend's webpage or in its codebase, and he argues that vibe coding now lets you build a whole language and compiler before you learn enough about the field to notice the field exists. An LLM asked for a proof language will happily build you one. It will not stop to mention that solvers have been discharging these obligations for decades.

The rebuttal Bend can make is real: its checker is self-contained with no external solver, its kernel is formalized in Lean, and its whole premise is that the human writes only the law while the machine pays for the proof. But 484 lines of generated proof is 484 lines of tokens per law, and the README concedes that Bend has no tactics and no proof search, which is exactly why the number is that big.

Where the speed claim wobbles

The README targets C on the CPU and CUDA on the GPU. The GPU half delivers. In the repo's pinned runtime results, Game of Life finishes in 0.063s on the GPU against 6.776s for C, mandelbrot in 0.057s against 3.750s, n-body in 0.059s against 5.126s.

Single-core is a different story, and the repo publishes the numbers that undercut its own headline. Across the 16 runtime benchmarks, Bend's sequential CPU build beats C exactly once, on tree-matmul, and lands within about one percent on kmeans and terrain. Everywhere else it is slower, and on hashmap it is slower by more than 4x.

None of this makes Bend slow. Parallel CPU cuts most of those benchmarks to roughly a tenth, and the GPU column is the headline. It just means "as fast as C on one core" is a target, not a result, and the repo is straightforward enough to ship the evidence against itself.

What the author concedes

Taelin spent launch day answering questions in public, and the concessions are more informative than the pitch.

• Laws only cover what you remember to write. His words: they are not a silver bullet. His example of one that would have earned its keep is a contract law that the sum of all balances must be zero, which he argues would have blocked the DAO hack.
• You still read code, just far less of it. He advises reading what the AI puts in LAWS.bend, since that file is the thing you are trusting.
• The stars are not adoption. The repo shows 21,907 stars, and Taelin says plainly that they came from the Bend 1 launch in 2024 and that it already had 20k before this release.
• The compiler is 99% AI-written. That is straight from the limitations block in the README, along with the note that it has not been fully audited. The kernel, he says, is human-designed and human-audited. A compiler built to stop AI mistakes that was itself mostly written by an AI is at least printed on the tin.
• The standard library is small. Proving simple theorems takes the AI more effort than it would in Lean. In his words, the project needs a mathlib.

The README's limitations list runs to about 40 lines and is the most useful page in the repo. No U64, I64 or F64. Strings are linked lists of characters, so text processing is slow. No TLS, HTTP, JSON or regex. No Windows, though WSL works. No test framework, no debugger, no profiler, no REPL, and terse error messages. Also this: the Lean formalization and the implementation currently mismatch, so early consistency bugs are possible.

Should you try it

If you run agents against a codebase where a class of bug is genuinely unacceptable, the LAWS.bend pattern is worth an afternoon, and the version history says the project is alive: 12 tagged releases between September 18 and September 20, ending at v2.0.19.

If you want that property in production today, read Powell's post first and price out SPARK, Lean or Rocq before you rewrite anything. The interesting question Bend raises is not whether it wins. It is whether "the agent must prove it" becomes a normal gate in a pull request, next to lint and tests. On that, Bend is early and pointed in a defensible direction.

Key Takeaways

• The mechanism is the story. LAWS.bend holds invariants, PROOF.bend holds the AI's proof, an unfilled law is a compile error, and bend PROOF.bend is the whole gate.
• The checker is fast enough for an agent loop. 0.295s on a 12,800-definition file against 36.177s for Lean and 5.985s for Rocq, on the repo's pinned Apple M4 Max run.
• The token cost is real. Bend's own demo needs 68 lines of law and 484 lines of generated proof, because Bend ships no tactics and no proof search.
• An existing tool did it with no proof file. A vibe-coded SPARK version of the same demo, about 50 lines, returned all 12 checks proved from GNATprove.
• Single-core parity with C is a target, not a result. Bend leads C on 1 of 16 sequential benchmarks. The GPU column is where the runtime earns its claims.
• Check the star count before you read it as traction. The 21,907 stars predate this release, by the author's own account.

Sources: bendlang/bend on GitHub, bend-lang.com, Bend pinned checker benchmarks, Apple M4 Max, Bend pinned runtime benchmarks, Apple M4 Max, demos/app_win_is_bug_2d/LAWS.bend, demos/app_win_is_bug_2d/PROOF.bend, Bend releases v2.0.8 to v2.0.19, Liam Powell, "Bend 2 and the Vibe-Coding Trap" (September 18, 2026), Hacker News launch discussion (September 17, 2026), AdaCore: About SPARK, BendRT: A Parallel Runtime for CPUs and GPUs, Bend GUIDE.md, HigherOrderCO/HVM