Bend 2 wants AI agents to prove their code, not promise it
Today's most consequential AI release isn't a model. It's a programming language built for a world where nobody reads the code anymore.
Victor Taelin released Bend 2 on Thursday, and its central claim is narrow enough to test: an AI agent cannot merge a mistake the compiler can disprove. The mechanism is a laws file — the project's own framing is that it is an agent instruction file with a proof checker standing behind it. You declare the rules your program must never break ("the sum of all balances must be zero", "the sort always returns ascending numbers", "winning is impossible"), and the agent must then supply a mathematical proof for each one. The compiler checks that proof after every edit and blocks the change until it holds. In the demo on the project's site, Claude is asked to make a game board wrap around; its first version opens a path to the flag, the proof fails, and the agent retries until it adds a wall instead. The bug never lands.
The performance claims are equally concrete. On one core Bend compiles to native code it says runs nearly as fast as hand-written C; the same binary scales to thousands of cores or a GPU. The project claims its type checker doubles as a proof checker that finishes in under a second on files that take minutes in Lean, Agda, Rocq or Isabelle — that number decides whether an agent can afford to check after every single change rather than at review time. Syntax is Python-shaped with dependent types and affine values, and the compiler targets C, Metal, CUDA and JavaScript. The GitHub repo sits just past 20,000 stars, the launch reached the front page of Hacker News, and the release is Apache-2.0.
Taelin's honesty about the state of it is the part worth keeping. The repository's own limitations list runs to thirty-odd entries: no Windows, no 64-bit integers or doubles, strings stored as linked lists so text processing is slow, no TLS, HTTP library, JSON or regex yet, no debugger, profiler, formatter, REPL, language server or test framework, and a hub with no names or version search. Two entries matter more than the rest. The compiler — not the human-audited kernel, the compiler — is "99% AI-written and has not been fully audited yet", and the Lean formalization of the core does not match the shipped implementation, so early consistency bugs are expected. The commit history was also force-pushed down to a single commit on release day; the maintainer said he squashed it to strip personal data and proprietary code, and commenters pointed out that 44 contributors' history went with it. Same hour, the team also launched Bender, an agent specialized in writing Bend proofs, which Taelin described as a thin wrapper over public models that he does not recommend buying yet.
The direction is still the interesting part, and it points opposite to where most agent tooling went this week. Bend does not ask you to trust evidence the agent produced about its own work — the failure mode we called out in An agent grading its own homework is an alibi, not proof. It puts a mechanical checker between the agent and the merge, and a proof is not an opinion you can talk around. Two holes are already visible. Asked whether the agent will simply edit a law to fit the feature it just built, the project's own commenters conceded laws need a frozen tier — so judgment sits with whoever decides what is frozen. And a proof shows that the law holds, never that the law says what you meant. Bend 2 enforces correctness inside the boundary you drew.
What to watch: whether a laws file survives first contact with a product team's change requests, and whether the compiler — the one unaudited, mostly AI-written part of the tool that blocks AI mistakes — gets the audit the kernel already has.
Would you trust a proof checker your agent wrote the proofs for — and would you know if a law had quietly changed? Tell us in the comments.
Sources: bendlang/bend (GitHub)
