Bend 2's Formal Verification Demo Misses Decades of Research
Bend 2 and the Vibe-Coding Trap
Bend 2 promises AI-written proofs, but its demo requires 58 lines of laws and 442 lines of proof for a simple game. The author recreates the same demo in SPARK, an established formal verification language, using only a fraction of the code. The real issue: vibe-coding lets developers build entire languages without discovering that the field of formal verification already solved these problems.
The developer has built an entire language around a field seemingly without realising that said field exists.