The Pulse
Bend uses laws and proofs to block AI coding mistakes
Bend presents a programming language that lets developers state important rules in LAWS.bend and require proofs before AI-written code is committed. The project combines Python-style syntax, native compilation and parallel execution across
AI.info Team ·
Bend puts a proof gate between an AI edit and a running program
Bend is a programming language designed to limit mistakes in software written with AI agents. Its central mechanism is LAWS.bend, a file where developers declare rules that should always hold. The project pairs those laws with proofs and asks users to run bend PROOF.bend before committing changes.
The website describes the goal in direct terms: natural-language prompts can be ambiguous, while laws give an AI a more precise specification of the desired behavior. Proofs then check whether the implementation satisfies those declared requirements. Bend presents this process as a way to review code through formal claims rather than relying only on a person to read every generated line.
LAWS.bend turns requirements into checked claims
Bend’s demonstration uses a game with a law stating that no sequence of moves can produce a winning state. The example shows an AI agent being asked to make the board wrap around. Without the law, the site says, the resulting mistake can be merged. With LAWS.bend in place, the agent must retry until it produces an implementation and proof that preserve the declared rule.
The example law quantifies over a sequence of moves, replays those moves from the starting position and checks that the resulting board is not a winning state. The companion PROOF.bend file defines a proof for the law. Bend describes the arrangement as an AGENTS.md instruction backed by proof: the developer records what must not break, and the checking process prevents code that violates that requirement from passing.
The project’s setup instructions tell agents to use LAWS.bend for important rules and run bend PROOF.bend before committing. They also ask agents to parallelize code whenever possible. The system does not decide which requirements matter; developers must identify the behavior they want to protect and express it as a law.
A fast language with native and parallel execution
Bend describes itself as a fast language with Python syntax, C speed, CUDA parallelism and Lean-style proofs. Its compiler produces native code. The site says that a program can run on one core at close to C speed, while the same binary can also run across sixteen CPU cores or on a GPU.
Its parallel model is based on splitting work into calls that Bend distributes across available cores before joining the results. The project says this avoids requiring programmers to write threads, locks or GPU kernels. A demonstration runs a pow2.bend program on 4,096 GPU cores.
Bend also presents its type checker as a proof checker, comparable in purpose to the checkers used by Lean and Rocq. According to the website, those systems can take minutes on a mid-sized codebase, while Bend is intended to complete its checks in at most a second. The stated aim is to let an AI agent check its work after each change.
A young project aimed at AI-assisted development
Bend’s installation instructions provide a shell command for installing the language and recommend Linux and macOS for the best experience. The site says Bend works best on the back end and asks users to report problems because the project is still evolving.
The project links to a language guide, a paper on Bend’s affine dependent type theory and a paper on its parallel runtime for CPUs and GPUs. It also warns users to expect bugs. Bend’s central promise is therefore limited but specific: when a developer states an important rule and supplies a valid proof, the checker can block an AI-generated change that breaks that rule. The usefulness of the process depends on whether the declared laws accurately describe the behavior the application needs.