⏱️ Lectura: 10 min
Bend 2 needs 442 lines of code to prove that a player can never touch a flag on a 12 by 8 board: SPARK, a formal verification language with decades of history, proves the same property with a package under 40 lines and twelve automated checks verified by GNATprove. Developer Liam Powell documented the comparison on September 18, 2026 on his blog, after reviewing the official demo that Bend 2 publishes as a vibe-coding example in its GitHub repository.
📑 En este artículo
The case exposes something more specific than a simple excess of code: Bend 2 presents itself as the language designed for programming alongside artificial intelligence, but the field that solves exactly that problem, formal verification, doesn’t appear mentioned even once on its website or in its source code.
TL;DR
- Bend 2 is marketed as a language for the AI era: humans write ‘laws’, AI writes the implementation and proofs.
- Bend 2’s official demo uses 58 lines of LAWS.bend and 442 lines of PROOF.bend to prove two simple properties.
- The words ‘formal verification’ don’t appear on Bend’s website or in its code, according to developer Liam Powell.
- SPARK, a formal verification language based on Ada, has existed for decades before Bend 2.
- Powell recreated the same demo in SPARK with an AI without additional guidance, and GNATprove reported: ‘Success: all checks proved (12 checks)’.
- SPARK uses contracts, ghost invariants, and postconditions instead of generating hundreds of lines of proofs from scratch.
- Powell’s article was published on September 18, 2026 on his personal blog.
- The case illustrates the vibe-coding trap: building a complete solution without researching the field before starting.
Introduction
Vibe-coding describes the practice of letting a language model write most of the code while the human guides with high-level instructions. Bend 2 takes that idea to a particular extreme: the developer writes rules called laws in a LAWS.bend file, and an AI must produce both the program’s implementation and a proof file, PROOF.bend, that mathematically demonstrates those laws hold.
The approach sounds appealing: a compiler that rejects code if the AI fails to prove its program is correct. But Liam Powell, in an analysis published on his blog on September 18, 2026, argues that Bend 2 fell into a classic vibe-coding trap: building a complete solution before checking whether the problem already had a better answer.
flowchart TD
A["Human writes the laws in LAWS.bend"] --> B["AI generates the implementation"]
B --> C["AI generates the PROOF.bend file"]
C --> D["Bend's compiler verifies the proofs"]
D -->|"valid proofs"| E["The program is accepted"]
D -->|"invalid proofs"| BWhat happened
Bend’s official repository includes a demo called app_win_is_bug_2d: a simple game where, by design, the player should never be able to touch the flag or win. To declare that rule, the developer had to write 58 lines in LAWS.bend.
The proof file that an AI generated to demonstrate those two properties, PROOF.bend, reached 442 lines. Powell also notes that the Game subprograms can be freely redefined by the model, which opens another design problem his article leaves for another time.
Context and history
The missing keyword in Bend 2, according to Powell, is formal verification: a field of computer science dedicated to mathematically proving that a program meets a specification, instead of relying on trial-and-error testing. That field is neither new nor experimental. SPARK is a subset of Ada designed specifically for writing verifiable software, with decades of history in systems where a software error can cost lives, such as avionics and trains.
Powell doesn’t claim that Bend’s author ignored formal verification on purpose. His argument is more uncomfortable: vibe-coding allows building an entire language, with its own compiler, without going through the literature review stage that any introductory course in that field would have put in front of them.
Technical details and performance
To make his point, Powell recreated the same game in SPARK. He clarifies that he also vibe-coded this version: he asked an AI to reproduce Bend’s demo, without giving it any additional guidance on how to structure the proofs.
The complete specification fits in a short package, because SPARK already builds into the language the mechanisms that Bend 2 asks the AI to reinvent in every project: precondition and postcondition contracts, and ghost functions that exist only to reason about the program, not to execute.
package Game with SPARK_Mode is
subtype Column is Integer range 0 .. 11;
subtype Row is Integer range 0 .. 7;
type State is record
X : Column;
Y : Row;
Won : Boolean;
end record;
function Safe (G : State) return Boolean is
((G.X > 2 or G.Y > 2) and not Wall (G.X, G.Y) and not G.Won)
with Ghost;
function Replay (Keys : String) return State
with Post => not Replay'Result.Won
and Cell (Replay'Result.X, Replay'Result.Y) /= 'F';
end Game;The Safe function is a ghost: it doesn’t compile to executable code, it only serves GNATprove to reason about the program’s invariant. The postcondition of Replay is literally the law that Bend 2 needs 58 lines to declare: the player never wins and never steps on the cell with the flag.
The package body implements the player’s movement and uses a loop invariant so the prover can follow the reasoning step by step:
function Replay (Keys : String) return State is
G : State := Start;
begin
for Key of Keys loop
pragma Loop_Invariant (Safe (G));
Step (G, Key);
end loop;
return G;
end Replay;To confirm the proofs are complete, SPARK’s workflow doesn’t depend on reading 442 lines of justification: it runs a single command and reads the result.
gnatprove -P game.gpr --mode=prove --report=allThe output Powell reports is direct: Success: all checks proved (12 checks). Twelve checks, automatically generated from the contracts, against the 442 lines Bend 2 asked the AI to write for the same two properties.
💭 Key point: the difference isn’t that SPARK is shorter by chance: contracts, ghost functions, and loop invariants have been part of the language for decades, so the AI doesn’t have to reinvent proof theory in every PROOF.bend file.
| Option | When to use it | Advantage | Limitation |
|---|---|---|---|
| Bend 2 | Projects where an AI must generate implementation and proof from scratch | The human only declares the high-level laws | 442 lines of proof generated for two simple properties, without leveraging prior theory |
| SPARK (Ada) | Systems that already have reusable contracts, invariants, and ghost functions | GNATprove automatically resolves proofs from contracts declared once | Requires learning Ada’s verifiable subset and its contract syntax |
How to start testing it
To reproduce Powell’s experiment you need to install the SPARK toolchain, distributed through Alire, Ada’s package manager. The steps are the same on Windows, macOS, and Linux, except for the initial installer:
- Windows: download the Alire installer from its official release and run
alr toolchain --selectfrom PowerShell to choose GNAT and gnatprove. - macOS: install Alire with
brew install alireand then runalr toolchain --select. - Linux: download the Alire binary for the matching architecture, add it to your
PATH, and run the same toolchain selection command.
With the toolchain installed, a new project is initialized and tested like this:
alr init --bin game_win_is_bug
cd game_win_is_bug
alr with gnatprove
alr exec -- gnatprove -P game_win_is_bug.gpr --mode=proveTo review Bend 2’s original case, the repository is public and the demo can be cloned directly:
git clone https://github.com/bendlang/bend
cd bend/demos/app_win_is_bug_2d
cat LAWS.bend PROOF.bend | wc -lThat last command is, literally, the fastest way to confirm the central fact of Powell’s article: counting the lines each approach currently requires for the same property.
⚠️ Watch out: SPARK doesn’t automatically solve any property: you have to write correct contracts by hand, and proving complex properties may require auxiliary lemmas. The advantage over Bend 2 isn’t that no thinking is required, it’s that you don’t need to reinvent proof theory in every project.
Impact and analysis: the vibe-coding trap
Powell’s argument doesn’t attack Bend 2 for being slow or generating too much code: it attacks the design premise. If the goal is for an AI to write proofs alongside code, the relevant question isn’t how to make the model generate more lines of PROOF.bend, but why the language doesn’t give the AI the same tools that already exist in a field with decades of research.
This connects to a broader vibe-coding problem: it’s possible to produce a large, functional artifact (a language, a compiler, a running demo) without the need to search prior literature ever surfacing along the way. A developer who researched formal verification before designing Bend 2 would likely have found SPARK, Dafny, or Coq on the first search.
The comparison also has a measurable practical cost: every line of PROOF.bend an AI generates consumes tokens, and with models that charge per output token, 442 lines of redundant proof aren’t just an aesthetic problem.
What’s next
Powell isn’t proposing that Bend’s team abandon the project, but that it recognize the field it’s competing in and compare its approach against existing formal verification tools. It remains open whether Bend 2 will incorporate ideas from SPARK, Dafny, or Lean, or whether it will keep betting on generating proofs from scratch with every model.
The case also leaves a question for any team currently designing an AI-backed language or tool: if the result looks suspiciously like an already solved problem, it’s worth pausing to search before continuing to build.
📖 Summary on Telegram: View summary
Try it yourself: clone Bend’s repository at github.com/bendlang/bend and compare the line count of LAWS.bend and PROOF.bend against an equivalent contract in SPARK before deciding which approach to use in your next verified project.
Frequently Asked Questions
What is Bend 2?
It’s a language presented as designed for the AI era: the human writes rules called laws in a LAWS.bend file, and an AI must generate both the implementation and a proof, in PROOF.bend, that the program meets those laws.
What is formal verification?
It’s the field of computer science that mathematically proves a program meets a specification, rather than relying solely on runtime tests. SPARK, Dafny, and Coq are tools from that field.
What is SPARK?
A subset of Ada designed for writing verifiable code with contracts, preconditions, postconditions, and ghost functions, used in critical systems for decades.
Why does SPARK need less code than Bend 2 for the same proof?
Because the proof mechanisms (contracts, invariants, ghost functions) are already part of the language. Bend 2 asks the AI to rebuild that reasoning from scratch in every project.
Who made this comparison?
Developer Liam Powell, in an article published on September 18, 2026 on his personal blog.
Is Bend 2 useless, then?
Powell doesn’t frame it that way. His point is that Bend 2’s design ignores an existing field, not that the idea of combining AI with verifiable proofs lacks value.
References
- Bend 2 and the Vibe-Coding Trap: Liam Powell’s original article with the full comparison against SPARK.
- github.com/bendlang/bend: Bend’s official repository, includes the analyzed demo.
- LAWS.bend: the 58 lines that declare the demo’s properties.
- PROOF.bend: the 442 lines of proof generated for the same demo.
- SPARK (programming language), Wikipedia: context and history of the formal verification language used in the comparison.
📱 Like this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day. @programacion
Imagen destacada: Foto de Markus Spiske en Unsplash
0 Comments