---
title: "Bend 2 and the Vibe-Coding Trap"
slug: bend-2-and-the-vibe-coding-trap
url: https://listedarticles.com/articles/bend-2-and-the-vibe-coding-trap
canonical_url: https://blog.liampwll.com/posts/bend_vibe_coding/
content_type: essay
language: en
published_at: 2026-09-18T12:00:00.000Z
updated_at: 2026-09-18T12:24:41.951Z
author: "Liam Powell"
author_url: https://blog.liampwll.com/
authored_by: human
publisher: "Liam Powell's Blog"
publisher_url: https://blog.liampwll.com/
topics: ["AI", "Programming", "Opinion", "AI Agents"]
license: all-rights-reserved
word_count: 392
reading_minutes: 2
citation: "Liam Powell, Liam Powell's Blog. \"Bend 2 and the Vibe-Coding Trap.\" 18 Sept 2026. https://blog.liampwll.com/posts/bend_vibe_coding/ (all-rights-reserved)"
# The full text follows. The web page shows an extract and sends readers
# to the source above; quote the citation and link the canonical URL.
---

# Bend 2 and the Vibe-Coding Trap

> Liam Powell argues Bend 2's AI-proof workflow reinvented formal verification without naming it—contrasting Bend's 442-line LLM proof with a short SPARK/GNATprove recreation of the same demo laws.

# Bend 2 and the Vibe-Coding Trap

Bend 2 is being pitched as a language for the AI coding era: humans write "laws", AI writes implementations and proofs, and the compiler checks that the proofs are sound. That all sounds quite impressive. There are actually a few major problems with this idea; however, that's not what this article is about. Instead I want to talk about how Bend itself seems to have fallen into a common trap with vibe-coding that I don't see mentioned much.

Bend's home-page demo asks the developer for a substantial `LAWS.bend` (about 58 lines just to state that the player can never touch the flag or win). The LLM-written `PROOF.bend` for those properties is about **442 lines**.

## The trap

The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists. A developer can produce an entire language and compiler while missing an approach that an introductory survey of the field would have put directly in front of them.

The field in question is **formal verification**. Those two words appear nowhere on Bend's webpage or in its codebase. The developer has built an entire language around a field seemingly without realising that said field exists.

## Same demo in SPARK

To demonstrate, the author vibe-coded the same Bend demo laws in SPARK (Ada). The package states an inductive `Safe` invariant and a `Replay` postcondition that winning and flag contact are impossible—then GNATprove reports:

```
Success: all checks proved (12 checks).
```

What was supplied is everything required to prove correctness **without** having an LLM waste tokens building a 442-line proof from first principles.

## Broader lesson

The author of Bend has completely missed that this is the current standard in formal verification. A little research before vibe-coding an entire language and compiler could have substantially improved the result.

This example matters beyond Bend: vibe-coding makes it far too easy to implement a design that's horribly broken or decades behind the state of the art, because you can immediately get a result without research. Ask an LLM for a language where you prove correctness by building proofs from basic principles and it will happily do so—it will never stop to suggest that existing tools already eliminate most of that work.

*Originally published on [Liam Powell's Blog](https://blog.liampwll.com/posts/bend_vibe_coding/).*