Bend 2: a proof-checked language for AI-written code

The problem Bend 2 is aimed at: trusting code nobody read

The README frames the project around a specific scenario. Humans will eventually stop writing and reading code, but we still need an ambiguity-free language to communicate intents to the AIs building software. Bend is that language. The stated problem is not expressiveness or speed on its own; it is how you trust AI code without reading it. The proposed answer is to force the AI to write a correctness proof.

That framing tells you who the project is for. It is for teams who already let an agent edit a codebase and who want a mechanical gate instead of a review convention. It is not pitched at people learning to program, and it is not pitched at projects that need a mature standard library. The README says Bend works best on the back-end, on Linux or macOS, which is a narrower claim than a general-purpose language launch usually makes.

How LAWS.bend turns a rule into a compiler-enforced obligation

The mechanism is a file named LAWS.bend that lives in the project. You declare rules the app must not break, and the compiler then guarantees those laws always hold by demanding a mathematical proof whenever the code is edited. The README describes LAWS.bend as AGENTS.md backed by proof, which is a fair summary: it is an agent instruction file whose contents the compiler checks rather than trusts.

A law is written as a claim over inputs. The README's example states that winning is impossible, quantifies over any sequence of moves, replays the board from the start, and asserts the game is never won. The proof lives separately in PROOF.bend as a definition named after the law. The workflow the README gives is three steps: ask your AI to formalize your app's rules in LAWS.bend, ask it to run bend PROOF.bend after editing any code, and that is it.

The demo in the README is the clearest statement of intent. Without LAWS.bend, an agent asked to make the board wrap around produced a bug that was merged. With LAWS.bend, the agent had to retry until no bugs were left; in the demo it added a wall, but the README notes it could have moved the flag or made the room kill the player instead. The point is that the specific fix is free, while breaking the law is not. That is a real design position, and it is the part of Bend 2 most worth arguing about.

Parallelism as divide-and-conquer, not threads and locks

The runtime story is separate from the proof story, and the README keeps them apart. There are no threads, no locks and no kernels to write. You split work in two, and Bend spreads the calls over every core it can find, then joins them back. The README's illustration is pow2(20), which divides until one task sits on each of 4,096 GPU cores.

The syntax that triggers this is a single character. A function marked with + on its recursive argument is the parallel one, and calling it with a trailing ! runs it on the GPU. In the README's example, pow2 is defined over a Nat with a +d parameter, recursing by computing pow2(p) twice and adding the results, and main calls pow2!(20n). The README also states that the entire language runs on the GPU, with full memory unification.

This is the part of Bend 2 that is easiest to verify and hardest to fake, because the repository ships bench/ with every bench used to make the charts, plus two papers, BendTT on the type theory and BendRT on the parallel runtime. If you are evaluating the parallelism claims, those are the artifacts to read rather than the animated charts.

Installing Bend 2 and running your first law

The README gives one install command, a shell script fetched over HTTPS and piped to sh. Read the script before you pipe it if that matters to your environment; the README does not describe what the installer does beyond this line.

curl -fsSL https://bend-lang.com/install.sh | sh

After installing, the README's first move is not to write code but to point your agent at the language. It asks you to add a block to AGENTS.md telling the agent to run bend guide to learn Bend, to use LAWS.bend for important rules, to run bend PROOF.bend before committing, and to parallelize where possible.

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

Then you say "use Bend". The guide is also a file in the repository at guide/GUIDE.md, and bend base prints the base library from bend2/base.bend, so you can read both without running anything.

The README's own first program shows the shape of the language: a main returning IO(Unit), a do IO<Unit> block, a typed binding that reads the USER environment variable, and a print. Syntax is described as Python plus dependent types. The parallel example is the shortest thing worth running once you have the toolchain.

import Base

def pow2(+d: Nat) -> U32:
  match d:
    case 0n:
      1
    case 1n+p:
      a b = pow2(p) pow2(p)
      (a + b : U32)

If that compiles and prints a number, your install works. If it does not, the README's own advice is to ask the agent to open an issue.

Where Bend 2 is the wrong tool

The README is unusually candid about age: Bend is young, and the hints section says so directly. Three constraints follow from what it documents.

First, platform. Bend works best on the back-end, on Linux or macOS. Windows is not mentioned as a supported target anywhere in the README, so if your team develops on Windows you are outside the stated scope.

Second, the proof workflow assumes a capable agent. The README's whole loop is ask the AI to formalize your rules, ask the AI to write the proof, and re-run it on every edit. If your agent cannot produce a proof for a law you wrote, the law does not become a safety net; it becomes a blocker. The README does not document what happens when a proof cannot be found, nor does it document rollback, so the failure mode of an unprovable law is something you have to discover.

Third, the release cadence is high. Three releases landed on 2026-09-19 and 2026-09-20 alone. That is a signal of movement, not of stability, and nothing in the README promises syntax compatibility across versions. Pinning a version is your problem, not the project's.

One more thing worth naming: the README asserts the compiler can check files in under a second that other projects take minutes on. That claim is supported by charts and by bench/, not by a methodology section in the README itself. Treat it as a target the project reports, and test it on your own laws.

Bend 2 against Lean, Agda and the proof assistants it benchmarks against

The README's checker benchmarks compare Bend against Isabelle, Agda, Lean and Rocq. Those are established proof assistants, and the difference in approach is the point. In Lean or Agda, the proof is the artifact; you write a theorem, you prove it, and any program you extract is downstream of that. In Bend 2, the program is the artifact and the law is an attached obligation: you write the app, you write LAWS.bend, and the compiler refuses edits that break the law. The README's own example shows a law with a matching def in PROOF.bend, so the proof-writing burden is still there, but it is scoped to the laws you chose rather than to a whole development.

That makes Bend 2 a different tool, not a faster version of the same tool. If you want to formalize mathematics, Lean is the mature choice and the README says as much by benchmarking against it. If you want a guardrail on an application an agent is editing, the law-file model is the one Bend 2 is built around. The repository also ships bend2/bend.lean, Bend's core formalized in Lean, which is a useful place to check what the type theory actually guarantees. The paper BendTT: An Affine Dependent Type Theory is the reference for the affine part, which is what lets the runtime reason about memory without locks.

Licence, maintenance and what an upgrade actually costs

Bend 2 is Apache-2.0. That is a permissive licence with an explicit patent grant, and it means you can ship Bend code in a closed product. It does not tell you anything about the runtime's behaviour or the project's governance; the repository has no separate governance file in its top-level entries. This is not legal advice, and if your organisation has a licence review process, Apache-2.0 is common enough that the review should be short.

On maintenance, the last push was on 2026-09-20, and the most recent release, v2.0.20, landed the same day. The repository is not archived. The practical consequence of that cadence is that upgrading is not a background task. There is a CHANGELOG.md at the top level, and it is the only place in the repository that would tell you what changed between v2.0.18, v2.0.19 and v2.0.20. Read it before you bump.

The upgrade cost that matters most is not the compiler, it is the proofs. If a release changes the type theory or the law syntax, your LAWS.bend and PROOF.bend files are the things that break, and they are the files your agent wrote. Budget for re-running bend PROOF.bend across every law after any version bump, and check the CHANGELOG for entries that touch laws or the checker before you do it. There is also a WONTFIX.txt at the top level, which is worth reading before you file an issue: it tells you what the maintainers have already decided not to change.

Editorial conclusion

Adopt Bend 2 if you are writing back-end code with an AI agent on Linux or macOS and you want machine-checked rules rather than review discipline, and start by running bend guide and reading demos/ before you write a single law. Skip it if you need Windows support, a stable syntax across releases, or a language with a large third-party library ecosystem, since the README only claims strength on the back-end and calls Bend young. Before committing, verify three things yourself: that bend PROOF.bend fails when you deliberately break a law, that the GPU path works on your hardware, and that your agent can actually produce the proofs rather than looping.

Frequently asked questions

Official sources

1. bendlang/bend on GitHub
2. License: Apache-2.0
3. Project website
4. README
5. Releases