Bend 2 and the Vibe-Coding Trap

Bend 2 is presented as a language for the AI-coding era where humans write high-level “laws,” a model generates implementations and proofs, and the compiler checks those proofs. Bend’s demo requires about 58 lines just to state simple invariants (the player can never touch the flag or win), while the machine-produced proof file runs to roughly 442 lines. The demo design even allows the LLM to redefine core game subprograms, and the Bend project’s webpage and repository do not mention formal verification as an existing discipline.

Recreating the same game in SPARK (an established, open-source language and toolchain for formal verification) produces a compact implementation with annotations that let GNATprove discharge all checks: “Success: all checks proved (12 checks).” That demonstrates the central critique: vibe-coding enabled building a substantial new language and compiler without recognizing decades of prior work, reinventing verbose specifications and proofs that established tools already automate. Vibe-coding therefore risks producing solutions that are needlessly complex or behind the state of the art, because a model will happily construct proofs from first principles instead of recommending existing, more effective verification infrastructure.