Bend 2 vs SPARK: Proof-Checked AI Code, 442 Lines vs 40

Bend 2 launched as a language where your agent writes machine-checked proofs, not just code. A rebuttal on Hacker News put the same demo in roughly 40 lines of SPARK against nearly 500 lines of Bend.

The collision happened on 18 September 2026, when engineer Liam Powell published "Bend 2 and the Vibe-Coding Trap" and it hit the HN front page the same day. Both sides are arguing about the same question every team running coding agents will hit: how do you know the 3,000 lines your agent just wrote are correct?

What Bend 2 claims

Bend comes from Higher Order Company, run by Victor Taelin; the original Bend 1 release in 2024 carries about 19,400 GitHub stars. Bend 2 is effectively a different language wearing the same name, and per its official site the pitch has three layers:

• Speed — compiles to native code, and the site claims the same binary scales across 16 cores or the GPU.
• Proofs — the type checker is a proof checker, in the Lean and Rocq lineage. The site claims it checks a mid-sized codebase in a second or less, where comparable provers can take minutes.
• Laws — you write LAWS.bend, a file of machine-checked invariants. The site's own framing: LAWS.bend is "AGENTS.md backed by proof."

The homepage's boldest sentence is that merging a bug becomes "mathematically impossible. It is a theorem." Treat that as vendor copy, not a measured result — the comparison we are drawing on says plainly that both tools are young enough that most claims come from their own marketing.

The critique: 442 lines versus 40

Powell's evidence is a line count on Bend's own demo, which states that the player can never touch the flag or win the game:

Artifact	Lines	Who writes it
LAWS.bend	58	Human
PROOF.bend	442	The LLM
SPARK equivalent	~40	Human; compiler discharges the obligations

The sting is in how the SPARK version was produced: Powell says he vibe-coded it, telling an LLM to recreate the demo in SPARK with no further guidance. An unguided model reached for a decades-old verification tool and landed an order of magnitude shorter than the purpose-built AI-proofing language. His other criticisms from the thread: the LLM can redefine the subprograms the laws talk about, and Bend does not integrate with existing tooling like Why3.

Taelin's answer

Taelin argued in the thread that verbose proofs are the feature, because fully explicit proofs check faster. He reports his own experiments confirming 10x-100x faster checking, with a commenter in the same field reporting 100-1000x. Those are participant figures in a forum argument, not benchmarks anyone has replicated. His structural point is harder to wave off: tactic-style proofs compress the text but pay for it on recheck, while Bend checks cold in about a second with no cache to invalidate.

The gap both sides leave open

Neither side seriously questions whether the laws file deserves your trust. It is the classic specification problem — verifying an implementation against an incomplete spec is worth exactly what the spec covers. The marketing sentence needs a footnote: merging a bug is impossible within the scope the laws cover. That is a real guarantee, just a smaller one than the homepage implies, and it is why the laws file is the one artifact a human has to own and keep small.

Which one, if either

• Safety-critical work today: SPARK. It has decades of deployment, a DO-178C certification story, and SMT automation that handles common property classes with no proof burden on you.
• Agents with invariants that must never break: Bend 2 is worth a weekend. Its own site says it is still evolving and to expect bugs.
• Just shipping faster with agents: neither, yet. Put critical invariants in tests, review the risky code yourself.

The thing to watch is not which language wins. It is whether agent pull requests start arriving with machine-checked proof obligations the way they arrive with CI status today — and if they do, whether anyone is reading the laws.