Victor Taelin released Bend 2 on 17 September 2026 under Apache-2.0, and it went to the top of Hacker News two days running, reaching 561 points and 285 comments. The pitch is the most direct answer anyone has given to the question of how you trust code you did not read: you write the rules, your AI writes the code, and the compiler refuses the code unless the AI also supplies a machine-checked proof that the rules still hold. The repository carries 21,264 stars.
The landing page states the claim without hedging: merging a bug is mathematically impossible, because it is a theorem. That claim is true, and it is narrower than it sounds. The proof does not remove the work of getting software right. It moves that work out of the code and into the rules, and the rules are the part people are worst at writing. Within a day of launch a reader running Bend's own headline demo hit exactly that wall, and a critical response post reached 271 points making a related argument from a different direction.
What follows is what Bend actually ships, where the specification problem bites, how it sits against verification tools that have been in production for decades, and what its own limitations file admits.
What Bend 2 actually ships
Bend 2 is a dependently typed, affine language with Python-like syntax that compiles to C, Metal, CUDA and JavaScript, with Lua, Luau and Python listed as planned, and the guide doubles as the full language specification. It is implemented in TypeScript. The language itself, the parser, theory and checker, lives in one file that the repo marks human-written and off-limits to agents; the compiler and runtimes live in another.
The verification workflow rests on two files. LAWS.bend holds the properties your application must never break. PROOF.bend holds the proofs that the current code satisfies them, and those proofs are what you delegate to the model. The README's own example is a game whose single law is that winning is impossible:
law you_cant_win:
for moves: List<Game.Move>
board = Game.replay(Game.start(), moves)
{Game.is_won(board) == False{} : Bool}Ask the model to make the board wrap around, and without the law it ships a board where the player wraps to the flag and wins. With the law in place the compiler rejects that edit until the model produces a program it can prove. In the documented run the model added a wall on the far edge. Taelin's summary is that LAWS.bend is AGENTS.md backed by proof, which is a fair description of the ambition.
The speed claims are separate and largely inherited. Bend targets C-level single-core performance and spreads balanced recursive calls across cores or a GPU with no threads or kernels written by hand, with benchmarks run on a rack of 48 Mac minis. The checker is the newer claim: Bend says it verifies in under a second files that other proof assistants take minutes on. That claim has the least public evidence behind it, and the repo concedes the point directly, noting it does not have as many benchmarks as it would like, especially for the checker.
The law is the easy half
The demo law above says winning is impossible. It does not say the game remains playable. That gap is the whole problem, and it is old: a safety property, meaning nothing bad happens, is always trivially satisfiable by doing nothing at all. Liveness, meaning something good eventually happens, is what stops the trivial answer, and liveness properties are considerably harder to state.
One commenter in the launch thread made the point in the abstract, noting that the easiest way to comply with a rule that the player never reaches the flag is to disable movement entirely, so you then have to specify that the player never reaches the flag while still being able to move, and so on. Another went and ran it. Editing the demo to remove the walls produced a program that satisfied the law by rewriting movement to be diagonal, deciding on its own that up and down move you along one diagonal and left and right along the other. Their conclusion is the sharpest sentence in the thread: every program will be under-specified, because at some point writing the laws becomes a bigger problem than writing the code itself.
The striking part is that Bend's README describes this behaviour as a feature. It notes that in the wrap-around case the model added a wall, but that it could have moved the flag, made the room kill you, or whatever, and that the only thing it cannot do is commit a bug. That is correct on its own terms and it is also the failure mode. An under-specified law does not stop the model from producing something absurd. It only guarantees the absurd thing satisfies the letter of what you wrote. A model that reaches for the clever degenerate reading is a familiar problem for anyone who has watched coding agents optimise against a weak benchmark, which is the same effect we covered when agents scoring 95% on SWE-bench Verified dropped to 38.8% on private codebases.
None of this makes laws worthless. It relocates the skill. Writing a law that pins down what you meant, including what must keep working, is specification engineering, and it is a genuine discipline with a real learning curve. Bend hands you that curve on day one and markets it as the easy path.
How Bend compares to proof tools that already exist
The most substantive criticism of the launch came from Liam Powell, who argued Bend reinvented formal verification without checking what was already there, and backed it with a direct port. In Bend, he counted 58 lines to state that the player can never touch the flag and 442 lines to prove it. He wrote the same properties in SPARK, the verified subset of Ada used in avionics and cryptography, in roughly 100 lines total, with no separate proof file, and the toolchain discharged it automatically and reported that all 12 checks were proved.
The gap is not mysterious, and Bend's own limitations list explains it: Bend has no tactics and no proof search, so proving theorems takes extra effort. SPARK and Dafny lean on SMT solvers that find routine proofs for you. Lean 4 gives you a tactic language and a large library of existing results, which is how it handles work at the scale of the Fermat's Last Theorem formalisation effort. Bend's bet is that the missing automation no longer matters, because the model writes the proof. That is a real bet and it is not obviously wrong. It is just a different trade from the one the marketing implies.
| Dimension | Bend 2 | SPARK (Ada) | Lean 4 | Dafny |
|---|---|---|---|---|
| You write | Laws; the model writes proofs | Contracts on subprograms | Theorems plus tactic proofs | Pre and post conditions |
| Automatic proof search | None | SMT solvers | Tactics and automation | SMT solvers |
| Powell's flag example | 58 law lines, 442 proof lines | About 100 lines, proved automatically | Not measured | Not measured |
| Runs on GPU | Yes, C, Metal, CUDA, JS | No | No | No |
| Tooling | No LSP, REPL, debugger or formatter | Certified toolchains, IDE support | Mature IDE and library | IDE support |
| Track record | Launched 17 Sep 2026 | Decades in avionics and crypto | Large formalisation projects | Production use at cloud vendors |
Worth noting against the reflex that formal verification never ships: it does. Commenters pointed to verification work inside AWS Nitro isolation, Apple's post-quantum cryptography libraries and Microsoft's Rust verification efforts. The honest framing is not that Bend brings proof to an industry that refused it. It is that Bend proposes a different division of labour, where the human writes only the specification and never the proof.
What the limitations list admits
Bend's README carries an unusually candid limitations section, ending with a line in capitals telling you the language is young and to expect bugs. Two entries matter more than the rest, and both bear directly on the trust claim.
The first: the compiler, as distinct from the kernel, is 99% AI-written and has not been fully audited. The second, and the more serious one: the Lean formalisation of the core and the actual implementation do not match, so early consistency bugs may occur. Bend ships a mechanisation of its core in Lean, which is exactly the right instinct. It also tells you that mechanisation and the checker you are running have diverged. A proof is only as good as the checker that accepted it, so the guarantee at the bottom of the stack currently has a documented gap in it. That is disclosed rather than hidden, which is to Taelin's credit, and it is still the thing to weigh before betting a product on the theorem.
Taelin has been direct about the AI involvement elsewhere too. Asked in the thread about vibe-coded sections, he answered that there is a lot of vibe coding in many places but that the critical parts, compiler, runtime and kernel, are human designed, and that the kernel has been extensively audited by a human. He also flagged that the runtime paper is written by Claude for now, while maintaining that it is accurate, and a commit message the next morning noted the papers' AI disclosure ends with a promise of a human paper soon. The candour is real and it is also the position the whole project is arguing about: a tool for trusting AI output, partly produced by AI output, asking to be trusted.
The practical limitations are a longer list. Nothing is inferred, so code is verbose. There are no type classes, traits or macros beyond compile-time templates. Values are affine, so closures and arrays cannot be shared. Numbers are Nat, U32 and F32 only, and F32 is axiomatic, meaning nothing about floating point can be proven. Strings are linked lists of characters, so text processing is slow. There is no TLS, HTTP library, JSON or regex yet. There is no Windows support, though WSL works, and no debugger, profiler, formatter, REPL, LSP or editor support. There are no releases and no tags on the repository at all; versions 2.0.1 through 2.0.5 exist only as commits, all dated 17 September.
One thread claim is worth correcting, because it circulated widely. Several commenters said the history had been squashed to a single commit and 44 contributors erased. The repository as it stands shows 2,814 commits on main and 44 contributors, with the top four accounts carrying between 363 and 692 commits each. It is also the same repository as Bend 1, renamed: HigherOrderCO/Bend and bendlang/bend resolve to the same repository id. Whatever force-pushes happened during launch week, the history is present now.
How to try Bend 2 this weekend
This is worth two hours if you already write agent-heavy code and want to see whether specification-first development suits you. It is not worth migrating anything to yet.
- Install with
curl -fsSL https://bend-lang.com/install.sh | shon Linux or macOS, then runbend guide, which prints the full language reference. Read that before writing anything, because nothing is inferred and the syntax only looks like Python. - Skip the JavaScript target for correctness work but use it for speed: compiling to native goes through clang, CUDA or Metal and is slow, while the JS target is the fast development loop. It runs on one core with no graphics or audio.
- Run the shipped demo, each of which comes with its own
LAWS.bend, and then deliberately try to break a law. The failure message is where you learn what the checker actually catches. - Write one law for something you already own, and write it as a pair. State the bad thing that must never happen, then state the good thing that must keep happening. If you cannot express the second half, you have found the limit of the approach on your problem, which is the most useful outcome of the exercise.
- Hand the proof to your agent, per the suggested
AGENTS.mdlines, and time it. Powell's 442 proof lines for a trivial property is the number to beat, and whether your model clears it on your problem is the only benchmark that matters for your decision.
Who should ignore this for now: anyone shipping on Windows, anyone whose work is text-heavy or floating-point-heavy, and anyone who needs HTTP, TLS or JSON without writing foreign bindings. Anyone running agents unattended, as with Claude Code in CI, should watch this idea closely even while skipping this implementation, because the underlying question of how you gate machine-written changes is not going away.
Frequently asked questions
Does Bend 2 actually guarantee the AI cannot introduce a bug?
It guarantees the code cannot violate the laws you wrote, which is a narrower statement. Any behaviour your laws do not constrain is unconstrained, and the demo itself shows the model satisfying a law by changing the game's movement rules. The guarantee is also only as strong as the checker, and Bend's own limitations note that its Lean formalisation and its implementation currently mismatch.
How is this different from Lean, Rocq or Agda?
Those are proof assistants with tactic languages, proof search and large existing libraries, built on the assumption that a human writes the proof with machine help. Bend removes the tactics and assumes a model writes the proof instead, and adds a compiler that targets C, CUDA, Metal and JavaScript so the proved program is also the program you ship.
Why did the critique use SPARK rather than Lean?
Because SPARK is the closest existing match to Bend's actual use case: annotating ordinary application code with properties and having a toolchain prove them automatically. Powell's point was that SPARK discharged the same flag property automatically in roughly 100 lines, against 500 in Bend, because SPARK has SMT-backed proof search and Bend has none.
Is Bend 2 related to the Bend that ran on GPUs in 2024?
Same author and the same repository, renamed, but the README states plainly that Bend 1 programs and HVM do not carry over. Bend 1 was pitched as a high-level language that ran on GPUs through HVM2, and it reached 1,041 points on Hacker News in May 2024. Bend 2 keeps the parallel runtime and puts proof at the front of the pitch.
Can I use it in production?
No, and the project does not claim otherwise. There are no releases or tags, no LSP, debugger or test framework, no Windows support, no TLS or HTTP, and an explicit warning that the language is young and to expect bugs. Treat it as a research preview with an unusually specific thesis.
What is the strongest reason to pay attention anyway?
The division of labour. If models keep getting better at producing proofs and humans stay the bottleneck on specification, then a language where the human writes only constraints is the right shape even if this particular implementation is not the one that wins. The question Bend forces is whether you can state what your software must never do, and most teams discover they cannot.
