Bend 2 and Proof-Blocked AI: What a Law File Actually Buys

Part three: from proving theorems to proving programs

Part one of this series argued that the Lean check of Fermat’s Last Theorem mattered less for the theorem than for the loop behind it: AI proposes formal steps, a small kernel checks every one, and the loop ports to software. Part two followed the same loop into fluid dynamics.

On September 17, 2026, Victor Taelin’s Higher Order Company launched a language that claims to take that loop the last step, into the code a working engineer writes every day. His launch post:

Bend 2 is here! It is a new programming language that blocks AI mistakes via *proof checking* - the same technique big AI labs used to solve open math problems, like Navier-Stokes.

— @VictorTaelin, September 17, 2026

The mechanism is a file. You declare rules your program must never break in LAWS.bend, and the AI that edits your code must also hand the compiler a proof that every rule still holds. The website’s version: “LAWS.bend is where you declare laws. From then on, no AI can ship one line that breaks them, ever.”

That is the most direct test yet of the limitation part one ended on. A proof is only as good as the statement it proves, and Bend’s entire proposition is that you write the statement and the machine holds the AI to it. So this piece asks the series’ question again, plus the one Bend forces: what does the checker actually check, and where does the risk go once it has checked it?

Every claim about Bend here is dated. The homepage changed several times on launch day. Everything below was read on September 18, 2026, against release 2.0.5 and repository commit 0b7e2b1. We ran the checker ourselves; where a result comes from that run, the text says so.

The fact check: hype vs. the metal

• ~ “No AI can ship one line that breaks them, ever.” True inside three qualifiers. It holds for the laws you wrote, over what those laws name. It holds only if the gate is run and cannot be sidestepped, and on launch day it can be: in our run, a false law “proven” through an @unsafe definition checked with exit code 0, and a PROOF.bend that simply stops importing LAWS.bend printed “All terms check.” Both were reported publicly on launch day in issue #776, which is open. And it is a claim about a language whose own homepage says “Bend is still evolving. Expect bugs, and please report them.” None of that makes the claim false. It makes it a claim with conditions a reader needs before relying on it.
• ~ “The same technique big AI labs used to solve open math problems.” Same family, different member. Like Lean, Bend checks a proof as a typed program in a dependent type theory, with no tactics or SMT solver in the trusted path, which puts it much closer to Lean than to Dafny or Verus. But the logic is a new one, the thing that checks your proofs is Bend’s own checker rather than Lean’s kernel, and there is nothing like Mathlib behind it. “Lean proofs” in the tagline means Lean-style proofs; Lean does not check them. The Navier-Stokes comparison is in the launch post, not on the website.
• ✓ The checker refuses the proofs a model would fake. We tried the obvious cheats on 2.0.5. A “proof” that just calls itself forever was rejected: the checker asked for “a decreasing self-call.” A proof with a missing case was rejected. The textbook paradoxes that break naive type theories are rejected by the repository’s own tests. An unfinished proof (?TODO) fails the gate with “1 TODO found.” That is the part of the pitch that holds up best, and it is the hard part to build.
• ~ “C speed” and “up to a hundred times faster.” These are the vendor’s figures from one Apple M4 Max, and they say something narrower than the tagline. On one core, Bend matched or trailed C on 15 of the 16 published programs, 1.3 times slower on the geometric mean. The “up to a hundred times” is measured against Bend on one core, not against C, and it is a GPU figure: 124 times on Game of Life, with only four of the sixteen programs above 50 times. Against the single-threaded C version the GPU still wins by 108 times on Game of Life; what the chart lacks is a parallel C or GPU rival. The GPU is the M4 Max’s own integrated GPU, driven through Metal, so the “CUDA parallelism” in the tagline has no published timings yet. The C versions are single-threaded, written “1-to-1 with the Bend program” and compiled at -O3, each figure is one timed run, and the “4,096 GPU cores” on the homepage is an animation, not a measurement. The numbers are real and useful; they are one machine’s numbers.
• ✓ The author is candid about what is not finished. The launch thread says there is “WAY more AI slop” in the project than he is comfortable with, and that the kernel is the part that has been deeply human-audited. The source files say the same thing in their own headers. More on that below, because it is the most useful thing in the launch.

What the checker actually checks

Bend’s type checker is a proof checker in the sense Lean’s is. A law is a type, and a proof is an ordinary function of that type: the guide puts it as “a proposition is a type, and a proof is a def of that type.” There are no tactics and no proof search; the proof is code the checker runs. Three rules keep that honest.

Proofs must terminate. A function that never returns has every type, so it could “prove” anything. Bend requires every recursive call to shrink one of its arguments, and it bans mutual recursion outright. The guide says why: “Both restrictions keep Bend’s proofs sound, as a function that never returns could otherwise prove anything.”

Values are affineType SystemsUse At Most OnceAffine TypesA variable may be used zero times or once, never twice. Rust’s ownership rules are a cousin. In Bend the same rule is what stops the classic self-referential paradoxes, because a function value can never be copied.Substructural Types →. By default, every variable is used at most once at runtime, and a function value can never be copied. This is less of a style choice than it looks. Bend’s core has no universe levels (Type : Type), which on its own is known to let a clever term prove anything. The design bets that forbidding a function from being copied blocks those terms instead. The project’s Lean model of the core carries that argument; more on its limits below.

Every case must be covered. A match that forgets a constructor does not check.

Put in one sentence each, which is the test this piece set itself:

• Bend’s checking excludes proofs that loop, skip a case, lean on an assumption nobody proved, or copy a function value, so a faked proof does not check, unless a definition is marked @unsafe.
• It does not exclude code that satisfies laws which fail to say what you meant, and it does not check that the compiled binary does what the checked program does.

The first sentence is the valuable part and it holds up. The second is where the rest of this article lives.

Is it the same technique the labs used?

The launch post ties Bend to the results this series covered: machine-checked mathematics, Navier-Stokes included. In the sense that matters most, the claim holds. Lean and Bend both follow the same idea: a claim is a type, a proof is a program of that type, and a small checker accepts or rejects it with no trusted automation in between. That is a different family from tools like Dafny or Verus, which hand proof obligations to an SMT solver and trust its answer.

Three differences are worth knowing before you lean on the comparison.

The logic is new. The BendTT paper describes a theory with “one sort with Type : Type, no universe hierarchy and datatypes with no positivity restriction, and it is consistent.” Lean avoids the known paradoxes with a tower of universes; Bend avoids them with the affine rule, which the paper sums up as “Affinity constrains what runs, never what is said.” That is a genuinely interesting design. It is also a young one, and logics earn trust slowly.

The evidence is about a model. Consistency is argued in a Lean file of about 21,000 lines that the paper’s disclosure calls “human-specified, AI-proven, and verified by a computer.” It checks cleanly: our research run compiled it under Lean 4.32.1 with no sorry and only Lean’s standard axioms. But the paper’s own limitations section is precise about its reach: “the theorems are about the calculus, not the code.” The code that checks your laws is a 3,734-line TypeScript file, and the Lean model’s header says it “doesn’t fully match the implementation (bend.ts) yet.” Fairness requires the other half: Lean’s kernel has not been proved faithful to its theory either, and Lean 4 has had kernel soundness bugs of its own (Carneiro, Lean4Lean: “Lean’s record is no longer spotless”). The difference is years of use, a far larger community looking for problems, and a set-theoretic model behind Lean’s logic.

The library is not there. The mathematics results stand on Mathlib’s analysis. Bend has no real numbers, and its floating-point operations are assumed rather than modelled. A Navier-Stokes development would have nothing to stand on in Bend today. That is not a criticism of a language aimed at programs, but it makes “the same technique” a statement about method, not about what has been checked with it.

The candour, taken seriously

The launch thread’s replies carry the caveats, and they are worth quoting at length rather than in fragments:

In particular, there is still WAY more AI slop than I am comfortable with. On the paper, website, computer. We’re a small team, and there is just too much hard code to catch up. But the critical parts (like the kernel) are deeply human audited, and the rest will be soon.

— @VictorTaelin, September 17, 2026

And the opening of his post about the paid agent launched alongside the language:

Also, in a last hour decision, we’re launching Bender, an AI agent specialized in Bend proofs. For now, it is just a thin wrapper over public models. I don’t recommend buying it yet.

— @VictorTaelin, September 17, 2026

It would be easy to turn the first quote into a gotcha: a language that blocks AI mistakes, shipped with AI-written material in it. That reading gets the point backwards. The source files say exactly where human attention went. The checker’s header: “this file was 99% human-designed and audited. It includes Bend’s trusted kernel, including interpreter and checker. It has a bit of AI slop, but it is the most robust file in the repo.” The compiler’s header: “mostly written by AI’s … bugs ARE expected.” The paper’s disclosure: written by an AI model “from the author’s code and design choices, and reviewed by the author.” That is the right split. The kernel is where a bug would let a false proof check, and it is the part the author says he read. It is not the whole trusted path, though: the gate problems in the fact check live in the command-line wrapper and in convention, not in the kernel.

There is a neater point underneath. Bend’s safety story for itself uses its own method. The core is modelled in Lean, and the header of that model says the specification part is “what humans must read and audit,” while the proofs “were written by AI, and checked by Lean.” That is LAWS.bend and PROOF.bend applied to the language itself. It inherits the same weak point, stated in the same header: the model “doesn’t fully match the implementation (bend.ts) yet.” A human-audited specification that does not quite describe the running code is precisely the limitation this series keeps arriving at.

Bender, for the record, is described on its own page as “a thin harness around models from Anthropic, OpenAI and others,” with its own proving technology promised in “future updates.” Credits are sold at a 50% founder price and, after a reply in the launch thread pointed it out, no longer expire. The author’s own advice not to buy yet is the advice to take.

The crucial limitation: specification risk, relocated

Part one’s law, one more time:

A formal proof guarantees that the encoded conclusion follows from the encoded assumptions. Nothing more.

For a theorem, the encoded conclusion is the statement, and it is usually short enough for a room of mathematicians to argue over. For a program it is the set of laws, which is longer, written by the same person who wrote the code, and, increasingly, by the same model. Bend’s proposition is that laws are “much more precise than natural language,” and they are. Precision is not the same as completeness. A wrong law is proved as happily as a right one, and wherever the laws are silent the AI is free.

We ran four small experiments on Bend 2.0.5 to make that concrete.

A law that is right. The repository’s insertion-sort demo states two laws: the output is sorted, and the output is a permutation of the input. Swap the real sort for one that returns its input unchanged, and the check fails. No proof can exist, because the law is false for that code. This is the pitch working exactly as advertised.

A plausible law that is not enough. Keep only “the output has the same length as the input,” a weaker stand-in for the permutation law, and the do-nothing sort checks clean: “All terms check.” The program prints [3n, 1n, 2n]. Keep only “the output is sorted,” and a sort that returns an empty list checks clean too. Each partial law admits a program any reviewer would reject on sight. It takes the whole specification.

The website’s own example. The homepage’s law is “winning is impossible”: replaying any sequence of moves never produces a board where is_won is true. The trouble is that is_won lives in the game code, which the AI owns. We removed a wall so the player can walk onto the flag, and made is_won always answer false. The law checked, with a proof one token long, while the game’s own state recorded a win.

The authors had seen this coming. The demo’s full LAWS.bend, in the repository and in the website’s live lab, adds a second law, bound to the board the page actually draws: the player never stands on a cell drawn as a flag. That law rejected our broken game. But it is satisfied by a board with no flag drawn on it at all, and the instructions the lab gives its AI rule that out in plain English:

Bad solution: remove the flag. That is trivially unwinnable.

And a few lines later: “turning the flag into a wall is technically valid but unsatisfying.” Technically valid means the laws allow it. The last piece of this specification lives in a prompt, which is the thing laws were meant to replace. That is not a failure of Bend’s authors, who wrote better laws than most people will. It is what specification risk looks like when handled well: you can push it back, law by law, and each push is checkable, but it does not reach zero.

Who writes the laws. The guide says the human writes LAWS.bend and “the AI does not touch it.” The README’s first instruction for using it is “Ask your AI to formalize your app’s rules in LAWS.bend.” Both are reasonable. Put together, they describe the situation this section is about: the same model drafting the specification and then proving its own code against it. The laws are where a human’s review time now has to go.

Two more gaps from part one’s list carry straight over.

The compiled binary. Part one listed implementation identity: a proof about the source says nothing about the machine code unless the compiler is verified. Bend erases proofs before compiling, and its compiler, by its own README, “is 99% AI-written and has not been fully audited yet.” Two gaps are already on record. A checked theorem about floating-point bits is false on the JavaScript backend (issue #797, open). And a natural number is unbounded in the checker but aborts past 2⁴⁸ − 1 at runtime, which the guide states plainly. An abort is the right failure. It is still a place where the model and the machine differ.

What the laws can see. Floating-point operations are primitives the checker assumes rather than models (“F32 is axiomatic: nothing about floating point can be proven,” says the README), which is how a checked statement about floating-point bits can still come out false on one backend. Effects are outside the proofs too: files, sockets and the network are host code that “proofs, termination and the GPU never touch.” A law about your ledger covers the ledger as your Bend code models it. The author’s example of a law worth writing is “the sum of all balances in this app is zero,” which, he wrote, would have prevented The DAO hack. Conservation laws like that are exactly the kind worth writing. Whether one would have caught The DAO depends on whether the money leaving the contract is one of the balances the law sums, which is part one’s semantic-fidelity question in a new place.

Is the GPU story part of the proof story?

Mostly no, and it is worth keeping them apart. Proofs are erased before compilation, so how fast the binary runs has no bearing on what was proved. The performance claims are a separate proposition that shares a release.

One speed claim does belong to the proof story: the checker’s. The homepage says proof checkers like Lean “can take minutes on a mid-sized codebase,” while “Bend takes a second at most, so an AI agent can check after every change.” That matters, because a gate an agent can run after every edit is a gate it will actually run. The evidence is a chart of generated stress files (thousands of definitions or instantiations), not mid-sized codebases, and the Isabelle column in the underlying data was carried over from an earlier run and is marked “not measured.” Plausible, promising, and not yet shown on real code.

The baseline question has history. Bend 1 launched in May 2024 with a GPU speedup measured against its own single thread, and when a Hacker News commenter read it as “100x faster than in C,” another replied with the correction: “Note that it’s not 100x faster than C, but than bend running on one CPU thread.” Within days the README said so itself: “its single-core performance is still extremely sub-par.” Bend 2 is a rewrite from scratch (“No file of Bend 1 or HVM carries over,” in the rewrite commit’s words), and by its own published numbers its one-core speed is now close to C. That is a real change, and a better headline than the ratio the chart leads with.

The DIY field guide: laws that bind and a gate that holds

You can use most of this without adopting Bend. The discipline is the product; Bend is one way to enforce it.

1. Write the law pair, not the law

For every function you hand to an AI, write down what the output must satisfy and what it must preserve. Sorted, and a permutation of the input. Balances sum to zero, and every transfer appears in the ledger. Player never reaches the flag, and the flag is still on the board. The sort experiment above is the whole lesson: a sorted-only law admitted a sort that returns nothing, and a length-only law admitted one that does nothing.

2. Test your laws with a wrong implementation

Before you trust a law, hand the checker code you know is wrong: a sort that returns its input, a sort that returns nothing, a game with a wall removed. If the law still checks, it is too weak. This is mutation testing aimed at the specification instead of the tests, and it takes minutes. Keep the wrong implementations in a folder so you can rerun them whenever a law changes.

3. Make the gate fail closed

Until the fixes proposed in issue #776 land, the gate should not trust the exit code alone. In CI, from the project root:

set -euo pipefail
# 1. PROOF.bend must really import the laws (a commented-out line does not count).
grep -qE '^[[:space:]]*import[[:space:]]+\./LAWS\.bend([[:space:]]|$)' PROOF.bend \
  || { echo "gate: PROOF.bend does not import ./LAWS.bend"; exit 1; }
# 2. No main in PROOF.bend: with a main, bend runs it and never prints a verdict.
if grep -qE '^[[:space:]]*def[[:space:]]+main[[:space:]]*\(' PROOF.bend; then
  echo "gate: PROOF.bend defines main"; exit 1
fi
# 3. The only success output is this exact line. The checker prints an
#    "annotated as unsafe" notice instead if any @unsafe def is reachable.
out="$(bend PROOF.bend)"
[ "$out" = "All terms check." ] || { echo "gate: laws not cleanly checked"; exit 1; }

The last check covers @unsafe anywhere the proof reaches, including imported packages, because the checker counts every one in its notice. That means this gate forbids @unsafe outright. For a server loop, the guide’s alternative is a Nat fuel argument that counts down. If your program genuinely needs @unsafe (shared atomics do, today), its laws come with a disclosed exception, and that is a decision for a human to write down, not for the gate to wave through.

4. Guard LAWS.bend like a security policy

The guide says the AI does not touch LAWS.bend. Make that true in your tooling rather than in a sentence. Require human review on the file (a CODEOWNERS entry plus a branch rule that requires code-owner approval does it on most forges), tell your agents it is read-only in their instructions, and put the LAWS.bend diff at the top of every pull request that changes it. A law change is a spec change; review it like one. The website’s own lab already does the tooling half: its file tools answer the model with “LAWS.bend is the human’s file: read-only.”

5. Bind laws to what the user sees

The website’s first law bound a helper function the AI owned; the repository’s second law bound the board the player sees, and that is the one that caught our broken game. When you choose what a law talks about, prefer the output a user or another system actually consumes over an internal flag the AI can redefine.

6. Read every benchmark by its baseline

“Up to a hundred times” was Bend on the GPU against Bend on one core, on one Apple M4 Max. Against C on one core, Bend was a little slower. Both numbers are useful. Neither is the other.

The bottom line: part three of the verification stack

Part one closed on a six-step loop. Part two added the physics half. Bend adds the program half, and it is worth writing out where each step’s trust comes from:

1. A human writes the laws. Nothing checks this step. It is the specification, and it is now the job.
2. The AI writes the code and the proofs. Untrusted, and that is fine.
3. A small kernel checks every proof, by the vendor’s figures fast enough to run after every edit. This is the part Bend has built well.
4. A gate refuses the merge unless every law is imported, closed and free of @unsafe. On launch day this is yours to build (see the field guide).
5. The compiler erases the proofs and emits C, Metal, CUDA or JavaScript. Trusted, not verified.
6. Benchmarks score the result, on stated hardware, against a stated baseline.

Bend moves the hard part of AI-assisted programming to where it belongs: writing down precisely what you mean. It makes that part precise enough to check, and it checks the proofs against it. It does not do that part for you, and its best-written demo shows the limit clearly, in its own words, in a prompt.

The smallest next step works whether or not you install anything. Pick one function your AI edits often. Write its law pair. Then hand your checker, or your property tests, a deliberately wrong version, and see whether the laws notice.

---

Part three of the machine-checked proofs series. Start with The Practical Value of Machine-Checked Proofs, then Navier-Stokes Blowup. All Bend material read September 18, 2026 (release 2.0.5, commit 0b7e2b1). Sources: bend-lang.com · Bend repository · Guide · BendTT paper (PDF) · Launch post · Author’s caveats · Issue #776 · Issue #797.