Bend 2 and the Vibe‑Coding Trap: Why Skipping Prior Research Leads to Redundant Formal Verification Efforts

The Core Takeaway

Bend 2 attempts to let humans write laws while an LLM generates implementations and proofs, but the approach requires 58 lines of law specifications and a 442‑line AI‑generated proof. By contrast, the same correctness properties can be expressed and automatically verified in SPARK with under a dozen lines, showing that neglecting prior research can produce unnecessarily complex solutions.

What Bend 2 Claims to Offer

  • Human‑written laws: Developers encode high‑level invariants (e.g., “the player can never touch the flag”).
  • LLM‑generated implementations: An AI fills in the game logic.
  • LLM‑generated proofs: The AI also writes a formal proof that the implementation respects the laws.
  • Compiler verification: The Bend compiler checks the proof’s soundness.

The demo on the Bend homepage includes a LAWS.bend file (58 lines) and a corresponding PROOF.bend file (442 lines). The author of the blog post argues that this verbosity signals a design flaw.

The Vibe‑Coding Trap Explained

"Vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists."

Vibe coding refers to prompting an LLM to produce a complete system based on a vague idea, without first surveying the existing literature. The trap manifests when:

  1. Research is skipped – developers rely on the LLM’s output rather than checking whether the problem is already solved.
  2. Redundant effort is incurred – the resulting system duplicates functionality that mature tools already provide.
  3. Complexity balloons – the LLM must generate extensive boilerplate (e.g., a 442‑line proof) that could be avoided with existing automated provers.

A Concrete Comparison: Bend 2 vs. SPARK

The blog author recreated Bend’s demo in SPARK, an Ada‑based language designed for formal verification. The SPARK version includes:

  • Type definitions for columns, rows, and game state.
  • A Safe ghost function expressing the invariant.
  • A Step procedure with a post‑condition guaranteeing safety preservation.
  • A Replay function with a post‑condition that the player never wins.
  • A simple driver program to display the game.

Running gnatprove on this code yields:

Success: all checks proved (12 checks).

Only a dozen verification conditions are generated, and no manual proof script is required. The entire correctness argument is handled automatically by the underlying SMT solver.

Key Differences

Aspect Bend 2 SPARK
Specification size 58 lines of laws ~30 lines of Ada types and contracts
Proof size 442 lines of AI‑generated proof 0 lines (automatic SMT proof)
Toolchain maturity New, AI‑heavy, 99% AI‑written compiler Decades‑old, audited, integrated with GNAT toolchain
Community support Small, largely experimental Established Ada/SPARK community, extensive libraries

Community Reactions on Hacker News

  • @pu_pe noted the discussion around Bend’s author’s reputation, suggesting the debate focused more on personality than technical substance.
  • @z7 corrected the claim that the author was unaware of formal verification, pointing to the author’s prior posts on the topic.
  • @captainmuon argued that existing verification languages are often too syntactically heavy, and that developers desire a more familiar language (e.g., C# or JavaScript) with built‑in contracts.
  • @mentalgear emphasized that any LLM‑driven project should start with a “run prior work research first” step to avoid reinventing the wheel.
  • @LightMachine defended the design choices, stating that explicit proofs are intentional for performance and that the language’s kernel is deliberately thin.
  • @simonw shared a personal workflow: ask a search‑enabled LLM to surface prior art before beginning a project, which saved him time.
  • @thomasahle clarified that SPARK’s automatic proofs rely on SMT solvers, which are brute‑force and do not scale to the expressive power of interactive provers like Lean or Bend.
  • @mccoyb highlighted that Bend 2 is a quantitative type theory (QTT) system, placing it in a different part of the verification spectrum than Ada/SPARK.

These comments illustrate a split view: some see Bend 2 as an unnecessary reinvention, while others view it as a purposeful exploration of a different verification paradigm.

Lessons for Developers Using LLMs

  1. Start with a literature survey – Ask the LLM to list existing tools, languages, and libraries relevant to your problem before writing code.
  2. Identify the verification model – Decide whether you need automatic SMT‑based verification (e.g., SPARK, Dafny) or interactive theorem proving (e.g., Coq, Lean, Bend 2).
  3. Measure the effort saved – Compare the size of specifications and proofs against known baselines; excessive boilerplate may indicate a missed existing solution.
  4. Leverage community resources – Established ecosystems provide audited compilers, standard libraries, and tooling that reduce risk.
  5. Treat LLM output as a draft – Review generated proofs for correctness and for alignment with best‑practice idioms in the target verification framework.

Conclusion

Bend 2 showcases a promising vision of AI‑augmented formal verification, yet its verbose proof generation underscores a broader vibe‑coding hazard: building elaborate systems without first understanding the state of the art. By conducting even a brief prior‑art search, developers can often replace thousands of lines of AI‑generated proof with a handful of automatic verification conditions, saving time, tokens, and potential bugs. The discussion around Bend 2 serves as a reminder that LLMs amplify both productivity and the risk of reinventing well‑solved problems.

Sources

Related