Bend 2 and the Vibe-Coding Trap

A green checkmark can make a new language feel inevitable. You give an AI coding agent—a tool that writes and edits software from instructions—a small game, ask it to make winning impossible, and soon you have a compiler, the program that translates source code into a runnable or checked form, plus a law file and a proof file. The demo runs. The checker approves it. For a moment, it feels as if the hard part of software engineering has been automated.

Bend 2 is aimed at exactly this moment. A human writes laws, meaning precise statements about what a program must never violate; an AI writes the implementation and the proof. Beneath that pitch is formal verification: using logic to show that specified properties hold across every execution covered by a model, rather than testing a sample of inputs. Bend's current workflow places those claims in LAWS.bend, their proofs in PROOF.bend, and treats a proof as a definition written in the language itself. (github.com)

The interesting criticism is not that this idea is useless. The more uncomfortable problem is that an AI-assisted project can become substantial before its author has learned enough about the field to choose the right approach.

The proof is the product

Imagine the game law in ordinary language: no sequence of moves can take the player into the winning state. As a specification—a precise description of permitted behavior—it might look like this:

law never_wins(moves):
 result = replay(start, moves)
 assert result.won == false

The statement is short. Proving it may not be. A proof written from first principles has to reason about the starting state, every movement command, wall collisions, the flag, and every possible list of moves. If the language expects that reasoning to appear as ordinary program definitions, a modest game can produce a surprisingly large proof.

That verbosity is not automatically a flaw. Constructive proofs can be valuable because the checker sees the reasoning rather than trusting an opaque answer from an external tool. Bend's design also has a clear internal logic: a law is a claim, and a proof is code that inhabits that claim. The project even avoids separate step-by-step proof scripts, known as tactics, in favor of definitions and pattern matching. (github.com)

But there is a difference between choosing a new proof style and rediscovering an old engineering problem. Before building a language around machine-checked claims, it helps to examine the tools that have spent decades deciding how specifications, invariants, solvers, and trusted assumptions should fit together.

What a mature verifier changes

SPARK is an Ada-derived language and toolset designed for software whose behavior must be analyzed precisely. Its verification tool, GNATprove, divides the work into flow analysis and proof. Flow analysis checks issues such as initialization and data dependencies. Proof checks contracts and the absence of many run-time errors, including problems such as overflow, invalid indexes, and division by zero. (docs.adacore.com)

A small SPARK-style model might express the important part like this:

procedure Step (G: in out State; Key: Character)
 with Post => (if Safe (G'Old) then Safe (G));

for Key of Keys loop
 pragma Loop_Invariant (Safe (G));
 Step (G, Key);
end loop;

The Post expression is a postcondition, a promise that must hold after Step returns. Safe (G) is the property we want to preserve. The loop invariant says that the property remains true after every iteration of the replay loop.

The programmer still has to design the model and choose a useful invariant. That is the difficult intellectual work. The difference is that GNATprove can translate the code and contracts into verification conditions—logical statements generated from the program—and pass them to automatic provers, programs that try to solve those statements without requiring the developer to write every logical step by hand. (docs.adacore.com)

A shorter proof does not mean a weaker proof. It means the proof burden has moved. Instead of manually reconstructing arithmetic and induction inside a new language, the developer writes a contract and lets an established verification pipeline handle routine deductions.

There is an important warning here. A successful checker run only proves that the implementation satisfies the laws as written, under the assumptions supplied to the tool. It does not prove that the laws capture the user's real intent. SPARK's documentation also warns that an inconsistent contract—such as a precondition that can never be true—can make later claims appear provable. Contract consistency and the trusted parts of the toolchain still need attention.

How vibe coding creates the trap

Vibe coding is prompt-driven development where the first goal is to get a working artifact, often before the developer understands the surrounding discipline. That workflow is powerful because it removes the blank page. It is risky for the same reason: a convincing artifact arrives before the questions that should have shaped it.

An AI model is very good at local coherence. Ask for a proof language with laws, recursive proofs, and a compiler, and it can produce a coherent answer. It may not stop to say that formal verification already has contracts, automatic provers, counterexamples, proof levels, and mature workflows. It will satisfy the prompt rather than challenge the premise.

That is how a project can become decades behind the current state of the art while still looking impressive. The code compiles. The demo is novel. The checker flashes green. Yet the system may be solving a problem that an existing tool solves with less machinery, better diagnostics, and a clearer account of what has actually been proved.

The danger also applies to the laws themselves. A law can be too weak, accidentally describe the wrong state, or make the interesting behavior unreachable. In that case, a proof may be perfectly valid and still tell us very little about the program people meant to build.

A better first pass

Before asking an AI to invent a compiler or verification framework, spend a short research cycle mapping the field:

1. Name the problem using established terms such as formal verification, deductive verification, contracts, invariants, and proof automation.
2. Rebuild one tiny benchmark in an existing tool and in the proposed design. Compare specification size, proof effort, diagnostics, and the assumptions each result depends on.
3. Keep the human-written specification separate from AI-generated implementation and proof. Otherwise the same system can quietly weaken the rule while claiming to satisfy it.
4. Audit the trusted base: the compiler, libraries, imported code, and any unchecked escape hatches that the proof does not cover.

Bend's law-driven approach remains an interesting attempt to make AI-generated software answer to precise rules. New languages can expose better ideas, and writing proofs directly in a programming language may be the right trade-off for some projects. The lesson is not to avoid invention. It is to investigate before inventing.

When AI can assemble a compiler in an afternoon, research is no longer separate from coding. It is the step that keeps us from shipping a clever answer to the wrong question.