I already keep an AGENTS.md telling Claude what not to touch, and I already know it’s a suggestion. Bend moves the rules into a LAWS.bend file the type checker enforces, so a change that violates one can’t merge. The demo is a game where winning is impossible; ask the AI to make the board wrap and it either breaks the law or gets blocked.
What makes it usable is the checker running in a second rather than the minutes Lean or Rocq take, so an agent can verify after every edit. I’d try it on a back-end service on Linux — where it’s said to work best — with one law for the invariant I’d actually get paged for. It’s young, so expect bugs.
The story — Bend is a language with Python-like syntax that compiles to native code at near-C speed on one core, spreads work across cores or a GPU without threads or locks, and uses a Lean-style proof checker as its type checker. Rules go in LAWS.bend, proofs in PROOF.bend; agents run bend guide and check proofs before committing (Source).