Bend 2 Wants AI Coding Agents to Prove Their Code Obeys Your Rules Before It Merges. Here's What That Does and Doesn't Guarantee

The takeaway: Bend 2, an open-source programming language whose most recent commits on GitHub are by Victor Taelin, has launched with a pitch aimed squarely at AI coding: its website calls it "a fast language that blocks AI mistakes via proof". You write rules, which it calls laws, in a file named LAWS.bend. According to the site, an AI agent then has to write a proof that its code keeps those laws before the code will pass. The site says: "LAWS.bend is AGENTS.md backed by proof." In our view the idea is serious. But, also in our view, a proof only guarantees what the laws say, so the hard part moves from reading the code to writing the right laws.

How it's meant to work

According to Bend's website, the workflow is:

• Declare laws. For example, the site's demo game has a law that no sequence of moves can win the game.
• Let the AI write code and a proof. The site says that once laws are declared, "no AI can ship one line that breaks them, ever."
• Check before committing. The suggested instructions for your agent include running bend PROOF.bend before committing.

In the demo, an AI is asked to make the game board wrap around. Without the laws file, the site shows the change breaking the rule and being merged. With it, the site says "the AI had to retry until it built a wall and proved the law holds."

In our reading, this is a form of formal verification. The site says Bend's type checker "is a proof checker, as in Lean and Rocq".

The speed claims

The site also makes performance claims. It says that on one core, Bend "runs nearly as fast as C", and that the same binary also runs on sixteen cores or on the GPU, "running up to a hundred times faster than one core". It says Bend's proof checking "takes a second at most, so an AI agent can check after every change", where it says Lean and Rocq can take minutes on a mid-sized codebase. The charts on the site are labelled as Apple M4 Max results. We haven't tested these claims ourselves.

What a proof does and doesn't give you

In our view, this is the part worth understanding before you rely on it:

• A proof checks the code against the laws, not against what you meant. If a law is wrong, or you never wrote one for a behaviour you care about, the proof won't catch it. One commenter on the Hacker News discussion made the same point: "The issue is I'll have to vibecode all the laws and the laws could be wrong."
• "Bug-free" is a strong claim. The site promises "bug-free, fast vibe-coded apps" and says merging a bug "is mathematically impossible". That's only true for bugs that break a law you've written down.
• It's early. The site's own references section says: "Bend is still evolving. Expect bugs, and please report them." It also says Bend "works best on the back-end, on Linux and on macOS".

The reaction

The launch drew about 380 points and nearly 200 comments on Hacker News. Some commenters were enthusiastic, while others questioned the "post-AGI" framing on the site, asked how Bend compares with established verification tools, and doubted that formal verification scales to large real-world programs.

Several also questioned the repository itself, noting that its history had been squashed to a single commit and doubting its star count of about 20,000. The account that identified itself as the author replied that the old history contained "a lot of private data and even proprietary code", which is why it was squashed, and said it plans on "putting the history back". The same account said the stars came from Bend's first launch, before this version. One commenter also said that, in their experience, agents "just modify the law itself to fit the new feature", which, in our view, is the risk to watch if an AI is allowed to edit the laws file.

Why it matters

In our view, Bend is one of the clearer attempts to answer a real question: how do you trust code an AI wrote that nobody has read? Its answer, to make the AI prove the code obeys rules you set, is a serious one. It also shifts the job. Instead of reviewing code line by line, you'd be responsible for writing laws that capture everything that must never break. Whether developers can do that well, at scale, is the thing to watch.