Bend Can Prove an AI Kept a Rule. It Cannot Prove You Chose the Right Rule.

Bend describes itself as “a fast language that blocks AI mistakes via proof.” Its homepage goes further: give an agent laws, require proofs, and a bug that violates those laws becomes mathematically impossible to merge.

That is both more real and less magical than it sounds.

Bend is a new, dependently typed, affine programming language with Python-shaped syntax. A law states a proposition as a type. A matching function supplies a value of that type—the proof. The checker accepts the program only when every required term is filled and type-correct.

I ran the checked-in insertion-sort proof with Bend 2.0.5. It returned All terms check. That means the implementation accepted the supplied proof of the supplied laws. It does not mean I independently verified the compiler, the benchmark claims, or every behavior of the generated program.

That distinction is the entire story.

The compiler can enforce a property across every input

Tests exercise examples. A proof can cover a quantified property.

Bend’s sort demo does not merely run [3, 1, 2] and compare the result with [1, 2, 3]. Its laws describe properties such as sorted output and preservation of the input elements. The proof is checked for the general function, not a handful of test vectors.

For agent-written code, that is a useful change in the review boundary. An agent may rewrite an implementation, but if the law remains fixed and the proof gate is mandatory, the new implementation cannot pass merely because it looked plausible or satisfied the visible tests. It must still inhabit the required type.

Bend’s game demonstration makes the idea accessible. The law says no sequence of moves can produce a winning state. An agent asked to make the board wrap around accidentally creates a path to the flag. The old proof stops checking. The agent must change the implementation or produce a valid proof for the revised one.

The compiler is not deciding whether the game is good. It is enforcing one statement about reachable game states.

A perfect proof of the wrong law is still wrong software

The same demo quietly shows the specification problem. The agent can satisfy “winning is impossible” by adding a wall, moving the flag, killing the player, or otherwise making the game useless. The law remains true.

That is not a defect in formal proof. It is a precise account of what was proven.

“The sum of balances is zero” does not prove every customer has the correct balance. “This array access is in bounds” does not prove the selected record belongs to the authenticated user. “No move sequence wins” does not prove the game is playable. A proof closes the gap between implementation and formal statement; it cannot close the gap between the formal statement and human intent.

This means LAWS.bend is the highest-value review surface, not a file to let the same agent rewrite casually alongside the application and proof. I would protect it with ownership rules, require human review for changes, and make the proof command a merge gate. Otherwise an agent can weaken the claim until its implementation passes.

The proof file also deserves review. A valid proof is strong evidence under the language’s logic, but maintainers still need to understand which definitions, axioms, unsafe escapes, and foreign effects sit underneath it.

The trusted base is currently young and unusually explicit

Formal verification always has a trusted computing base. In Bend that includes the checker, compiler, runtime boundaries, and assumptions built into primitive operations.

The project’s own limitations section is unusually direct. It says the compiler—not the small kernel—is 99% AI-written and has not been fully audited. It warns that the Lean formalization and the TypeScript implementation can mismatch. Early consistency bugs may exist.

Bend also provides deliberate exits from the proof world. @unsafe disables the termination checker for a definition. Foreign C and JavaScript effects let programs interact with systems the proof kernel does not model. Floating-point operations are axiomatic; the documentation says nothing about F32 behavior can currently be proven.

Those are not reasons to dismiss the language. They are reasons to state the guarantee accurately:

Given the checked law, the accepted proof, the semantics implemented by this checker, and no relevant behavior escaping through unsafe or foreign boundaries, the program satisfies that law.

That is a meaningful guarantee. It is not “the application has no bugs.”

The language is not ready to replace an ordinary backend stack

Bend combines proofs with an interesting execution model. Pure, affine values make independent calls easier to parallelize, and the compiler can target C, CUDA, Metal, and JavaScript. The project reports near-C single-core performance and large speedups on suitable parallel workloads.

Those figures come from the project’s benchmarks. I did not reproduce them, and the maintainers say the benchmark set is still limited.

The practical limitations are larger than the landing page’s “Python syntax” might suggest. Bend currently has no standard TLS, HTTP, JSON, or regular-expression library; no LSP, debugger, profiler, formatter, REPL, or test framework; no Windows target outside WSL; no incremental or separate compilation; and a small base library. Strings are linked lists and text processing is slow. Numbers are limited to Nat, U32, and F32.

Proof development is also work. Bend has no tactics or proof search. It performs little inference, so programs and proofs require explicit annotations. The fast checker helps an agent iterate, but the absence of automation does not make difficult invariants easy to formalize.

This looks more like a research-stage language with a serious executable prototype than a general replacement for Go, Rust, TypeScript, or PHP today.

The agent workflow is the interesting experiment

I would not start by asking Bend to build an entire service. I would start with a small pure component whose failure matters and whose invariant can be stated cleanly: a parser state transition, permission lattice, accounting transformation, protocol state machine, or deterministic scheduling rule.

Then I would separate responsibilities:

• a human-reviewed law file defines the invariant;
• the agent may change implementation and proof files;
• CI runs bend PROOF.bend from a pinned toolchain;
• unsafe definitions and foreign imports receive explicit review;
• ordinary tests cover integration behavior and examples the law does not express;
• the generated binary is still scanned, deployed, observed, and rolled back like any other artifact.

That workflow does not eliminate code review. It concentrates review on the specification and trust boundaries while letting the checker reject a class of implementation errors automatically.

The loud claim is that Bend makes vibe-coded applications bug-free. I do not believe that claim as written. The valuable idea underneath it is better: agents can generate far more code than people can read, so important invariants need a machine-enforced form that survives implementation churn.

Bend is an early, auditable attempt to make that practical and fast enough to run after every agent edit. The proof is not a substitute for judgment. It is a way to make one part of that judgment executable.

Sources

• Bend, project site and proof demonstration.
• Bend 2 source, guide, demos, and limitations, reviewed at version 2.0.5, commit e6676b0.
• Bend project, BendTT paper and checked-in Lean formalization.
• Bend project, BendRT paper.