Bend 2 Bets Formal Proof Can Catch AI's Coding Mistakes

The pitch: proofs instead of review

Bend 2 went public on Sept. 17, the newest version of a programming language Victor Taelin builds through Higher Order Co, the company Taelin founded. The project's own description calls it "a fast language that blocks AI mistakes via proof," and its central argument is that reviewing AI-generated code by reading it does not scale, so a project should instead state, in a formal language, what must never be true and let the compiler refuse any change, AI-written or not, that would make it true.

The repository, now hosted under the bendlang organization on GitHub, carries 21,186 stars and 564 forks under an Apache-2.0 license.

Bend 2 fact	Detail
Public release	Sept. 17, 2026
License	Apache-2.0
GitHub stars	21,186
Forks	564
Numeric types supported	Nat, U32, F32 only

How a LAWS.bend file is supposed to work

Bend's mechanism is a file called LAWS.bend, where a project states rules as formal, provable statements: the README's own examples include "winning is impossible," "the sum of all balances must be zero" and "players can never pass through solid walls." If an AI assistant then writes code that would let a player reach a victory flag by wrapping around the edge of a board, the compiler will not accept the change until a proof shows the law still holds, forcing the AI to find a different fix, such as adding a wall.

The same parallelism design extends to hardware. Bend uses an affine type system, meaning each value can be used exactly once, which the project says eliminates data races at compile time without a programmer writing threads, locks or GPU kernels by hand; the README's example shows a pow2(20) call marked for parallel execution and split across 4,096 GPU cores, then rejoined.

The proof system is new to this rewrite. According to Bend's own release notes, Bend 1 ran on HVM2, an interaction-net graph-reduction runtime that found independent work to parallelize on its own; Bend 2 replaces that runtime with one the project calls BendRT, which compiles functions into a flat C evaluator instead of executing interaction nets, and asks a developer to mark parallel work explicitly rather than leaving the runtime to find it. Bend 1's published syntax had no way to state a theorem at all, so LAWS.bend and the proof checking built around it did not exist until this version.

The numbers are Bend's own

Bend's README claims its compiled code matches hand-written C on a single core and rivals CUDA on thousands of GPU cores, and that its proof checker verifies files in under a second that "outperform every proof assistant by several OOMs," where rival tools take minutes. AI/TLDR's write-up of the release states plainly that these are the project's own published figures rather than independent measurements, and no outside benchmark of Bend 2 has been published against Lean, Agda or Coq, the established proof assistants Bend's own comparison invokes.

Bend is not the first language written for a world with GPU-native execution in mind: Nvidia's own cuda-oxide and cutile-rs projects let developers write CUDA kernels natively in Rust, though Nvidia has declined to call either production-ready as of September 2026. Bend takes the more radical position that the entire language, not just a GPU-targeting subset of an existing one, should compile to parallel hardware by default.

What the README admits Bend can't do yet

Bend 2's own documentation is unusually candid about what it lacks. Values are affine, so closures and arrays cannot be shared. There is no type inference: "everything is annotated and nothing is inferred, so code is verbose." There are no type classes, traits or macros beyond compile-time templates, no TLS, HTTP library, JSON or regex support, and "strings are linked lists of characters, so text processing is slow." Compilation itself is slow enough that the README recommends targeting JavaScript for rapid development instead of the native path. There is no debugger, profiler, formatter, REPL or language server, and no Windows support outside of WSL. The README's closing line is blunt: "BEND IS YOUNG. EXPECT BUGS AND REPORT THEM."

The compiler enforcing the proof is itself unaudited

The README states that "the compiler (not kernel) is 99% AI-written and has not been fully audited yet." That is the detail Bend's own pitch has to answer for: a tool built to stop AI-introduced bugs from reaching production is, by its authors' own account, mostly AI-written code that has not gone through the audit its marketing tells other projects they need. A bug in Bend's compiler would not just miss a violation the way a linter might; it could let a false proof pass, which is a different failure mode than the one Bend was built to prevent, and a harder one to notice, since the entire pitch is that a passing proof means the property is true.

What would test Bend's claim is not another benchmark from Higher Order Co, but a LAWS.bend file written by a team with no stake in the project, protecting a real system, that catches a real AI-introduced regression before it ships. Taelin's own project pitch is exactly the kind of capability claim OpenAI's own disclosure of a model that wrote its own jailbreak persona into training summaries argues for treating with more scrutiny than a demo video provides: the failure modes that matter are the ones nobody wrote a benchmark for yet. Neither the README nor AI/TLDR's coverage names a team outside Higher Order Co that has used LAWS.bend to protect a system it did not build itself.