DEV Community

jamilxt
jamilxt

Posted on

Bend 2 vs SPARK: Can You Actually Trust AI-Written Code Without Proof?

#programming #ai #devtools #formalverification

An AI agent writes 3,000 lines of code for you. It compiles. Tests pass. Now the question nobody has a good answer for: how do you know it is correct?

This week gave us two competing answers, and they collided on Hacker News in the most 2026 way possible. Bend 2 launched with a homepage that reads like a manifesto: humans write laws, AI writes code and proofs, and no broken law can ever ship. Within a day, a rebuttal post titled "Bend 2 and the Vibe-Coding Trap" was climbing the front page, arguing that SPARK, a formally verified subset of Ada, had proven the same demo program in roughly 40 lines while Bend needed nearly 500.

I have not used either tool in a real project, and both are young or specialized enough that most claims come from their own marketing. So this is a researched comparison, not a hands-on review. Everything below is sourced from the official Bend site, the critique post and its HN thread, and SPARK vendor material, all linked inline. I will flag where the sources disagree.

What Bend 2 actually claims

Bend is a language from Higher Order Company, run by Victor Taelin, with about 19,400 GitHub stars for the original Bend 1 release in 2024. The pitch back then was parallelism: Python-like syntax that scales like CUDA, no threads or locks, near-linear speedup across cores and GPUs. One documented example: a bitonic sort took 12.15 seconds on a single CPU thread, 0.96 seconds on 16 CPU threads, and 0.21 seconds on an RTX 4090 with 16k threads. That is a 57x speedup "by doing nothing," as the README put it.

Bend 2 is a different language wearing the same name. Per its official site, the new pitch has three layers:

  • Speed: compiles to native code, "nearly as fast as C" on one core, and the same binary scales across 16 cores or the GPU, running up to a hundred times faster than one core.
  • Proofs: the type checker is a proof checker, in the Lean and Rocq lineage. Per the site, it checks a mid-sized codebase in a second or less, where comparable provers can take minutes. Fast checking is the feature: an AI agent can prove every change before it commits.
  • Laws: you write LAWS.bend, a file of machine-checked laws describing what must never break. The site's own framing: LAWS.bend is "AGENTS.md backed by proof."

The workflow the site advertises: ask your agent to write laws for whatever should never break, add a snippet to your AGENTS.md so the agent runs bend guide and re-checks PROOF.bend before every commit, and the compiler rejects any change that breaks a law. The agent retries until the proof goes through. The site's boldest sentence: merging a bug becomes "mathematically impossible. It is a theorem." That claim is genuinely novel packaging: AGENTS.md-style instructions that a compiler actually enforces.

The critique: the vibe-coding trap

On September 18, engineer Liam Powell published "Bend 2 and the Vibe-Coding Trap," and it hit the HN front page the same day. His argument has two layers, and conflating them caused most of the HN mess.

The general point. Vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognize that a better solution already exists. Powell's evidence: the words "formal verification" appear nowhere on Bend's site or repo, yet Bend 2 is, structurally, a formal verification language. He points at Bend's own demo:

  • 58 lines of LAWS.bend just to state that the player can never touch the flag or win the game.
  • 442 lines of PROOF.bend for the LLM to prove those laws.
  • About 40 lines of SPARK to express the same properties, with the compiler discharging the proof obligations automatically.

Powell even admits he vibe-coded the SPARK version, telling an LLM to recreate the demo in SPARK with no further guidance. The irony is the point: an unguided LLM reached for an established verification tool and produced something an order of magnitude shorter than the purpose-built AI-proofing language.

The specific criticisms. In the HN thread, Powell added that the LLM can redefine the Game subprograms, so the laws constrain less than advertised; that Bend does not integrate with existing verification tooling like Why3; and that letting an LLM write all proofs is wasteful when SMT solvers discharge such obligations in under a second. His summary: "a little research before vibe-coding an entire language and compiler could have substantially improved the result."

Taelin's rebuttal, in his own numbers

Victor Taelin showed up in the thread and did not back down. Stripping the rhetoric, his case is:

  • He knows the field exists. He built Kind, a dependently typed language, five years before LLMs, and describes a decade in formal methods. He called the "missed an entire field" framing misleading, and even Powell's sympathizers in the thread agreed that part was unfair.
  • Verbose proofs are a feature. Fully explicit proofs check faster. Taelin reports his own experiments confirming 10x-100x faster checking, and a commenter in the same field reported 100-1000x. Lean-style tactics compress proof text at the cost of slow rechecking; change a deeply nested constant in a big Lean project and, per Taelin, you wait hours while every transitive dependency gets rechecked. Bend checks in about a second, cold, with no cache to invalidate.
  • The LLM writes the proof, not you. In the demo, the model produced its proof in one shot and it checked in about a second, mostly startup time. Humans read laws, not proofs, the same way nobody reads a checksum.
  • Existing tools can fill proofs too. He invites exactly what Powell wants: point SMT solvers or other automation at Bend's obligations while the language stays a thin, fast proof kernel.

This is not a crank versus critics story. Both sides agree on the core technical claim: fast proof checking is what makes AI-written, proof-checked code economically possible. They disagree on whether Bend 2's particular kernel is the right design.

Side by side

No tables here, so the comparison in bullets:

  • Goal: SPARK proves industrial Ada codebases correct for aviation and rail. Bend wants to be the native language of agent-written code, with proofs as the trust layer.
  • Maturity: SPARK has decades of deployment, a DO-178C certification story, and industrial case studies. Bend 2 is months old; its own site says "Bend is still evolving. Expect bugs, and please report them."
  • Proof style: SPARK leans on SMT solvers that discharge most obligations invisibly, but struggles past linear arithmetic and array-heavy properties. Bend uses explicit proofs your LLM writes, checked by a fast kernel.
  • Learning curve: SPARK means learning Ada, contracts, and a proof mindset. Bend has a Python-like surface syntax, so onboarding looks deceptively gentle.
  • AI workflow integration: SPARK has none built in; you bring your own agent. Bend ships AGENTS.md integration and a "tell your agent to use Bend" section in the official docs.
  • Parallelism: SPARK has nothing here. Bend's same-binary scaling across cores and GPUs is carried over from Bend 1 and remains unique among proof languages.
  • Ecosystem: SPARK has AdaCore, commercial support, and real avionics users. Bend has a small team and a Discord.

The problem both sides gloss over

Here is what the launch and the takedown both treat as given: that the LAWS file is where your trust should live. It should not, entirely. A law is only as good as the human who wrote it.

Remember that detail from the HN thread: the demo proves the player can never touch the flag, but no law stops the agent from redefining the Game subprograms the laws talk about. That is the classic specification problem, and formal methods has known it for 50 years. Verifying an implementation against a bad spec is worthless, and verifying it against an incomplete spec is only worth what the spec covers. So the marketing sentence needs a footnote: merging a bug is mathematically impossible within the scope the laws cover. That is a real guarantee. It is just smaller than the homepage implies.

There is a cultural risk in Powell's piece too. If proofs are written by LLMs and never read by humans, the proof layer becomes another artifact nobody audits. You have moved trust from reading code to reading laws, but laws have exactly the same failure mode as any other spec: incomplete coverage. And when your reviewer is also an LLM filling in proofs, nobody downstream can tell "proven correct within scope" from "the spec covers everything that matters."

None of this is an argument against the tools. It is an argument about where the human goes in the loop. The laws file is the one artifact a human must own, review, and keep deliberately small, because that is the entire trust boundary of the system.

So should you use it?

Depends on your situation:

  • Safety-critical code today: SPARK, without hesitation. Certification-grade maturity, real avionics deployments, and SMT automation that handles common property classes with zero proof burden on you.
  • Running AI agents with invariants that must never break: Bend 2 is worth a weekend. The laws-plus-fast-proof-checking loop is a real idea, and it is currently the only tool shipping it as an integrated agent workflow. Expect rough edges; the team says so themselves.
  • Just want to ship faster with agents: neither, yet. Standard practice still wins: review the risky code yourself, put critical invariants in tests rather than laws, and treat both tools as early signals, not infrastructure.

My honest take: the interesting question is not Bend versus SPARK. It is whether proof-carrying agent code becomes a default part of the stack. Both stories this week point the same direction. Even the critique's comment section concludes that current best practice is a mix of LLM and traditional automation inside an interactive theorem prover, and Bend is a bet that explicit proofs plus fast checking is the better kernel for that mix. One of these designs will lose, and it will not matter much, because the direction is settled. In five years, agent PRs may arrive with machine-checked proof obligations the way they arrive with CI status today. The open question is who writes the laws. That should be you, and that is the one part no tool can automate.

I write about AI tooling, developer platforms, and programming languages every week. Subscribe, it is free.

Have you tried Bend 2 or SPARK with AI-generated code? Did the proofs hold up in practice?

A save-worthy takeaway, what I would do differently: before adopting any proof tool for agent code, write the laws yourself, first, before the agent writes a line. If you cannot state what must never break in 20 lines, no proof system will save you. Start with one invariant, prove it end to end, and expand only when the loop is boring.

Sources

Top comments (0)