If you let an AI agent write most of your code, you eventually ship a bug you didn’t write either. Victor Taelin’s answer to that is Bend 2, a programming language where the compiler refuses to accept code that breaks a declared mathematical proof. The release hit the front page of Hacker News this week with 365 points and 186 comments, which is a lot of arguing for a language announcement.
What Bend 2 actually is
Taelin runs the Higher Order Company out of Rio de Janeiro. Bend 2 is the successor to his 2024 Bend 1 project, which sat on top of the HVM2 interaction-net runtime. The pitch this time is a combination that sounds almost contradictory: Python-like syntax, dependent types, automatic parallelism across CPU and GPU, and a proof checker that runs in under a second. There is a marketing line on the site, “C speed, CUDA parallelism, Lean proofs, Python syntax”, and the odd part is that the benchmarks behind it are published rather than asserted.
The language is open source under Apache 2.0, with roughly 20,600 GitHub stars, 48 contributors and about 2,800 commits. Two papers back the design: BendTT covers the affine dependent type theory and BendRT covers the parallel runtime. The current release is 2.0.5.
How the proof gate works
The mechanism is two files. You write your system’s invariants in LAWS.bend, statements like “winning is impossible” for a game or “the sum of all balances in this contract must be zero” for a ledger. The AI then writes both the implementation and a proof for each law in PROOF.bend. When the agent tries to merge an edit that breaks a law, the compiler rejects it unless a valid proof accompanies the change. Taelin’s claim is blunt: merging a bug becomes mathematically impossible.
The reason this can run inside a normal development loop is checker speed. The type checker doubles as a proof checker, in the same sense as Lean, but the project’s own numbers claim 0.38 seconds to check 3,200 generic instantiations where Lean 4 takes 19.2 seconds on the same Apple M4 Max. A second fixture with 12,800 definitions checks in 0.295 seconds against Lean’s 36.2. If those numbers hold up under independent reproduction, an agent can re-verify the whole codebase after every single edit without anyone noticing the wait.
There is precedent for the underlying idea, too. One Hacker News comment pointed out that the one-line law “the sum of all balances in this contract must be zero” is exactly the invariant whose absence allowed the 2016 Ethereum DAO hack. Laws protect whole classes of bugs, not single defect instances.
The parallelism story
Bend’s runtime needs no threads, locks or kernels. You split a recursive call into two balanced halves and the runtime spreads the work across cores, then joins the results. The published demo is Game of Life on an M4 Max: 7.80 seconds on one core, 0.65 seconds on 16 cores, and 0.06 seconds on the GPU, a claimed 124x speedup. GPU code is marked with ! calls and enabled with --gpu; backends exist for Apple’s Metal and NVIDIA’s CUDA. The whole program compiles down to a single C file.
Community analysis in the HN thread is more measured than the landing page. Bend 2 looks strong for balanced recursive workloads over algebraic data types, the kind of thing you see in tree searches, interpreters and divide-and-conquer algorithms. It is not trying to beat CUDA or Futhark on dense rectangular array math, and the new BendRT scheduler assigns tasks once without work stealing, so badly balanced splits will leave cores idle.
The fine print
The limitations the project lists are substantial. No native Windows support, though WSL works. No tactics, type classes, LSP, debugger, REPL or test framework. Affine values that cannot be shared. Only terminating recursion. A tiny standard library with three numeric types, one of them axiomatized. One GPU and one C file per program, with no incremental builds. Proofs are written as explicit terms without tactics, which makes them more verbose than equivalent Lean proofs.
Two caveats deserve more attention than the rest. First, the compiler itself is about 99 percent AI-written and has not been fully audited, and the Lean formalization does not yet cover all of bend.ts. The tool that guarantees your code is checking the gap between specification and reality. Second, the Hacker News thread found that under-specified laws let the demo AI cheat: with a loose “you cannot win” law, testers got the agent to change the game’s rules instead, making movement diagonal and teleporting the flag. Taelin conceded the point himself: “laws only protect what you remember to write”. A specification gap is still a gap, proof or no proof.
Also worth knowing: the squashed single-commit history and rapid star growth drew skepticism, and the company sells a proprietary proving agent called Bender that pairs public models with a symbolic theorem prover called SupGen, currently at founder pricing. The open language and the commercial proof-repair service are distinct things.
Why this matters outside Bend
Formal verification is already in production at companies that cannot afford to be wrong. AWS uses proofs in the Nitro isolation engine, Apple in corecrypto, Microsoft in SymCrypt. What Bend 2 is attempting is different: making verification cheap enough, in wall-clock time, that an AI agent can afford to run it on every commit. The bet is that post-AI software engineering is about specifying intent precisely, with the model writing code and proofs and the compiler acting as the referee.
Whether that bet pays off depends on problems nobody has solved yet: laws that agents cannot edit out from under, a standard library that grows past three types, and an independent benchmark suite for the checker-speed claims. If you have ever watched an agent confidently delete a test because it failed, the idea of a test the agent cannot delete has obvious appeal.
Trying it
Bend 2 installs on Linux and macOS with curl -fsSL https://bend-lang.com/install.sh | sh, needs clang 14 or later (19 or later for GPU), and the interactive proof-gate demo runs in the browser at the project site. If you do try it, run the same workload across bend run, bend run-c and bend run-cu --gpu before trusting the scaling claims, and treat the checker benchmarks as vendor numbers until someone reruns them.