Vibe-coding a compiler without knowing formal verification exists
Bend 2 is pitched as a language built for the AI coding era: humans write “laws,” AI writes implementations and proofs, and the compiler checks that the proofs are sound. The pitch sounds compelling on the surface. The execution reveals a problem that goes beyond Bend itself.
The Numbers That Tell the Story
The Bend demo on its homepage requires 58 lines of developer-written law code just to state that a player can never touch a flag or win a game. The LLM then has to produce a 442-line proof file to verify those simple properties.
The author of the article then vibe-coded the same demo in SPARK, an open source language and compiler for formal verification, giving no further guidance beyond telling an LLM to recreate it. Running GNATprove on the result produced: Success: all checks proved (12 checks).
The Vibe-Coding Trap
The words “formal verification” appear nowhere on Bend’s webpage or in its codebase. The developer appears to have built an entire language and compiler around a field without knowing the field exists.
This is the trap the article is actually about. Vibe-coding lets you produce a substantial, working result before you’ve done enough research to know that a much better solution already exists. An LLM asked to build a language for proving function correctness from first principles will do exactly that. It won’t stop to tell you that computers have been doing this without LLM-generated proofs for decades, or that what you’re building already mostly exists as prior work you could build on.
The Operator Takeaway
If you’re using AI to build tooling in any technical domain, a brief survey of the existing field before you start coding can save you from shipping something that’s either broken or decades behind the state of the art. The shortcut of skipping research works fine for utility scripts. It doesn’t work when you’re designing a language or a system architecture from scratch.
I’m founder of BizStack at Cagri Sarigoz LLC and a passionate advocate for entrepreneurs.
With over 14 years in tech, marketing, and AI, including my role as Head of SEO at CitizenShipper and co-founder of TaleBot at Intale AI, I’m dedicated to sharing genuine, useful product insights and tips.
At BizStack, I aim to cut through the digital noise to provide clear, actionable advice.
And more than all else, I’m a father to a (always) little girl and a husband.
Contact me at [email protected] for assistance.
