Bend 2 turns AGENTS.md rules into type errors

Victor Taelin's Bend 2 went public on September 17 and took 502 points on Hacker News. The repo sits at 21,032 stars.

The problem it targets is one anyone running coding agents hits constantly. You write an invariant into AGENTS.md, the agent reads it, agrees, and writes code that breaks it three files later. Prose constraints are suggestions.

The mechanism is a LAWS.bend file where you write theorem statements, like law add_zero: for x: Nat {Nat.add(x, 0n) == x : Nat}. The AI writes the proofs that discharge those laws in PROOF.bend. Running bend PROOF.bend fails until every law is proved. It's a commit gate, not a linter, and the failure is a type error.

The core is BendTT, an affine dependent type theory in the same family as Lean and Rocq. The authors say type checking finishes in about a second where comparable proof systems take minutes. That's the number that makes this plausible inside an agent loop.

Syntax is Python-shaped. It compiles to C, Metal, CUDA and JavaScript with automatic parallelization across cores or GPU, under an Apache 2.0 license.

Bend publishes no hard benchmarks. The C-speed and CUDA-speed claims are qualitative comparisons in the README, and the project describes itself as still evolving. Writing useful dependent-type laws is also a real skill most engineers don't have. The near-term use is narrow: a handful of invariants like "no panics in this module" or "this transform preserves length." That's well short of the broad correctness pitch.

One warning for anyone searching: the launch spawned at least five same-day forks with zero stars that rank high in search results. Pin to bendlang/bend.

If you're not adopting a new language, the transferable move is smaller. Find the invariants your agents keep breaking and turn each into a test that fails loudly instead of a paragraph buried in a markdown file.