Bend 2 and the Vibe-Coding Trap

AI can accelerate implementation before a developer has investigated whether an existing approach would simplify the problem. The Bend 2 critique illustrates this through formal verification: checking whether a program obeys explicitly stated rules. In Bend's demo game, humans state the rules and the AI must write a long proof file that the compiler checks. The author asked an LLM to recreate the demo in SPARK, an existing verification toolchain, and reports that its GNATprove tool proved all 12 checks automatically from the specification.

The useful argument concerns the choice of approach. Generating more code quickly can conceal an avoidable design burden. This example supports researching existing verification methods before building a new system. The SPARK version was itself LLM-written, and the author says they do not know what Bend's creator knew, so the comparison does not settle every tradeoff between the languages.