The post-AGI economy has a trust problem. We’re letting AI write more code every day, but very little of it is verified. TypeScript caught some of the errors. Tests caught others. But both operate on the “probably fine” principle. That’s about as comforting as a seatbelt made of duct tape.
Enter Bend, a language built on a simple, slightly unhinged premise: AI mistakes should be mathematically impossible, not merely unlikely.
The Pitch: AGENTS.md Backed by Proof
Bend positions itself as the language for the “post-AGI economy.” The pitch goes: humans will eventually stop writing code, but we still need an ambiguity-free way to tell AI what we want. Natural language is ambiguous. Code is precise. Proofs are unforgiving.
Here’s where it gets interesting. The workflow looks like this:
curl -fsSL https://bend-lang.com/install.sh | sh
Then you add this to your AGENTS.md:
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
That second instruction is the killer feature. LAWS.bend is where you declare invariants that must hold no matter what. From that point forward, no AI can ship a line that breaks them. Not because of a linter. Not because of code review. Because the type checker treats those laws as theorems and your code as a proof of those theorems.
What “Proof” Actually Means Here
Before you scroll past muttering “formal verification is too slow”, consider the benchmark. Bend’s type checker doubles as a proof checker, drawing on the same lineage as Lean and Rocq. Those systems can take minutes on mid-sized codebases. Bend compiles and verifies in under a second:
| System | 3,200 generic instantiations |
|---|---|
| Isabelle | > 5 min |
| Agda | > 5 min |
| Lean | 19.2s |
| Rocq | 6.04s |
| Bend | 0.38s |
That’s the difference between “verification as a pre-commit ritual” and “verification as a keystroke.” An AI agent can check its work after every single change without grinding your CI pipeline to a halt.
This matters because Lean is already becoming the verification layer for AI mathematics. When OpenAI’s internal system proposed a solution to the Navier-Stokes Millennium Prize Problem in September 2026, it didn’t just publish a paper, it released a proof in Lean. The same idea applies to systems code: AI can propose, but verification disposes.
The Game That Proves the Point
Bend’s website includes a live demo: a grid-based game with a law stating winning is impossible. LAWS.bend declares:
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False{} # never leads to victory
You can prompt an AI to modify the game in any way you want. “Make the board wrap around.” “Let the player move twice.” “Add a teleport.” Without LAWS.bend, the AI happily merges a change that breaks the invariant, the classic vibe-coding failure mode. With LAWS.bend, the compiler rejects the change. The AI has to retry until it produces a version that satisfies the law, essentially constructing a proof that its modification is safe.
This is not “we wrote a unit test that checks this one case.” This is “every possible input sequence is exhaustively covered by construction.”
The Performance Story Holds Up Too
Proofs are worthless if the resulting code runs like a slug. Here’s where Bend’s second move lands: it compiles to native code with a parallel runtime that scales from one core to GPU.
| Workload (Game of Life) | Runtime |
|---|---|
| TypeScript | 18.8s |
| Lean | 13.8s |
| C | 6.78s |
| Bend (1 core) | 7.80s |
| Bend (16 cores) | 0.65s |
| Bend (GPU) | 0.06s |
One core: nearly C speed. Sixteen cores: 12x faster. GPU: 124x faster than single-core. You write a high-level, Python-syntax language and get CUDA-level parallelism without writing a single kernel.
This is the “have your cake and eat it too” trifecta: C speed, CUDA parallelism, Lean proofs, Python syntax. The type checker is fast enough for agentic workflows, and the runtime is fast enough for production workloads.
Why This Breaks the Current AI Coding Paradigm
The AI agent teams building entire compilers are impressive. Anthropic’s experiment with 16 AI agents building a Linux-capable C compiler was a landmark. But that $20,000 experiment also produced a 100,000-line Rust codebase that needed heavy review. Nobody is reading all that code. At some point, “trust but verify” stops working because there’s no human left to do the trusting.
Bend inverts this: instead of verifying code after the fact, you state your invariants up front, and the language refuses to compile violations. The AI doesn’t try to obey your laws. It’s physically incapable of generating code that breaks them.
For teams architecting systems that need correctness guarantees, this is a fundamentally different relationship with AI-generated code. You’re not reviewing every line for subtle bugs. You’re specifying the boundaries and letting the compiler enforce them.
The Skeptic’s Objections (Because There Are Some)
“Formal methods never escaped academia.”
True, but that’s changing. Verified software has been quietly running critical infrastructure for years. The novelty here is making the entry cost low enough for AI-driven development. The bend guide command is the entire language reference, not a 400-page specification.
“Writing laws is just writing specs, which nobody does.”
Partially fair. But specs are passive, they describe what should happen. Laws are active, the compiler refuses to produce anything that violates them. One lives in a document nobody reads. The other lives in your build pipeline.
“What if my laws are wrong?”
Great question. That’s a real risk. But wrong laws surface fast because they either fail to capture what you mean (compiler lets bugs through) or they’re too restrictive (AI can’t make progress). The failure modes are visible early, unlike the “ship it, find out in production” approach.
Where This Actually Matters Most
The most compelling use case: durable workflow systems. The SQLite pattern that’s been gaining traction for reliable workflows already emphasizes minimal dependencies and provable state transitions. Bend takes that further by making the invariants explicit in code.
Think about distributed transactions. Think about financial reconciliation. Think about any system where “it might be fine” is an unacceptable failure mode. These are the domains where enforcing reproducibility and correctness in data pipelines becomes non-negotiable. Bend’s laws theorem-ize the guarantees that currently depend on discipline and code review.
The same goes for managing complexity in system architecture. Your hexagonal architecture has boundaries. Your laws should too. Bend encodes those boundaries so that violating them is a compile error, not a code smell.
Bend isn’t asking you to trust AI. It’s asking AI to prove it deserves your trust. The proof checker is fast. The runtime is competitive. And in an era where AI agents are becoming system designers rather than just code writers, we need languages that can hold them accountable.
This language is young. It has bugs. It’s explicitly evolving. But the philosophy, that “make no mistakes” should be type-checked rather than aspirational, is the most important idea in systems programming since memory safety.
Your AI can keep hallucinating code. Bend just won’t let it ship.
