# Bend

> A compiled language whose type checker is also a proof checker, so an AI edit only builds if it proves your declared laws still hold

- Category: AI Coding / AI Code Review & Security
- Language: TypeScript
- Licence: Apache-2.0
- Repository: https://github.com/bendlang/bend
- Website: https://bend-lang.com
- Canonical page: https://ai-tldr.dev/tools/bend/
- Updated: 2026-09-17

## In short

Bend is a compiled programming language built around the idea that you should be able to state, once, the rules your program must never break — and then have a machine enforce them on every future edit. It sits in the AI Code Review & Security category of the AI Coding tools and is open-source, written in TypeScript and licensed Apache-2.0.

## Overview

Bend is a compiled programming language built around the idea that you should be able to state, once, the rules your program must never break — and then have a machine enforce them on every future edit. Those rules live in a file called `LAWS.bend`. A law is written as a quantified statement about the program's own functions (the README's example declares that replaying any list of moves in a game can never reach a won board), and Bend's type checker doubles as a proof checker: after a change, the compiler demands a mechanical proof that every law still holds, and produces no binary if it cannot get one.

That design is aimed squarely at code an AI wrote. A model can be asked to retry until the proof goes through, which converts the usual review question — does this diff quietly break an invariant somewhere else? — into a compile error. The language itself has Python-like syntax with dependent types, is affine (values are not shared), requires recursion to terminate, and compiles to C, Metal, CUDA and JavaScript. The project reports targeting C-level speed on CPUs and CUDA-level throughput on GPUs, with parallelism coming from divide-and-conquer structure rather than explicit threads, and claims its proof checker beats other proof assistants by several orders of magnitude.

Bend 2 became publicly available on 17 September 2026 and is Apache-2.0 on GitHub, where the repository carries just over 20,000 stars. It is early software and the README says so at length: everything needs explicit annotation (no type inference, no type classes, traits or macros), there are no proof tactics or search, only Nat, U32 and F32 as number types, a small base library, one GPU per program and no multi-machine execution, and native compilation is slow enough that the JavaScript target is suggested for development. Bend 1 programs do not carry over. The repository also discloses that the compiler — though not the kernel — is 99% AI-written and has not been fully audited.

## What it does

- `LAWS.bend`: declare invariants as quantified statements about your own functions; the compiler re-proves them after every edit or refuses to build
- Type checker and proof checker are the same engine — verification is part of compilation, not a separate tool in CI
- Dependent types with Python-like syntax, so specifications are written in the language rather than in a separate proof assistant
- Compiles to C, Metal, CUDA and JavaScript; the JavaScript target is the recommended fast loop during development
- Parallelism from divide-and-conquer structure, spreading across CPU cores or a GPU without thread or kernel code
- Apache-2.0, installable with a single shell command, with `bend guide` shipping the language tutorial in the binary

## Getting started

Bend installs from a shell script and carries its own tutorial. The documented habit is to run the proof file before committing, so a change that breaks a law fails locally rather than in review.

1. Install Bend

   One shell command from the project site installs the compiler, the base library and the guide.

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

2. Read the built-in guide

   `bend guide` is the project's own tutorial. Bend 2 is not source-compatible with Bend 1, so previous experience does not carry over.

```bash
bend guide
```

3. Declare a law

   A law is a quantified statement about your own functions. This example from the README says that replaying any sequence of moves can never produce a won board.

```python
# LAWS.bend
law you_cant_win:
  for moves: List<Game.Move>
  board = Game.replay(Game.start(), moves)
  {Game.is_won(board) == False{} : Bool}
```

4. Check the proofs before committing

   Run the proof file to confirm the current code still satisfies every declared law. This is the step that catches an AI edit which type-checks but breaks an invariant.

```bash
bend PROOF.bend
```

## When to use it

- Reach for it when an AI agent edits code whose invariants matter more than its style — balances that must be conserved, state machines that must not reach a bad state
- Reach for it when you want a machine-checked guarantee at build time instead of a test suite that only samples the input space
- Reach for it when a parallel CPU or single-GPU workload would otherwise mean writing thread or CUDA code by hand
- Skip it for production systems today: no type inference, a small base library, no multi-machine execution and a compiler the project says is 99% AI-written and not fully audited

## Version history

- 2026-09-17 Bend 2: Bend 2 became publicly available. The release centres on LAWS.bend, where declared invariants are re-proved by the compiler after every edit, and adds dependent types with Python-like syntax plus C, Metal, CUDA and JavaScript targets. Bend 1 programs do not carry over.