Bend 2 reached 275 Hacker News points and 138 comments in under five hours. Yet the launch's most revealing line sits near the bottom of the project's README: the compiler is "99% AI-written" and has not been fully audited. That tension makes Bend more interesting than its promise to stop AI mistakes. It asks a small, human-reviewed set of laws to govern a much larger body of agent-written code, while a young toolchain enforces the boundary, according to the launch discussion and the project's own limitations.
The proposal is concrete. A person writes invariants in LAWS.bend. An AI can write the program and the matching proof in PROOF.bend. Running bend PROOF.bend fails while a law is open or false. A passing check establishes that the implementation satisfies the stated law within Bend's type theory, as the official guide explains. It cannot establish that the person wrote every law the application needed.
A new language built around a merge condition
Bend 2 is an Apache 2.0-licensed language with Python-shaped syntax. It combines dependent types with affine values. The latter can be consumed at most once unless their type permits copying. That restriction supports both its proof system and its parallel runtime. Bend 2 is also a clean break: the README says Bend 1 programs and its HVM runtime do not carry over, and the new language performs little inference, so developers should expect more annotations than in similar languages.
The same source can target C, JavaScript, CUDA or Metal. Parallel calls split independent work across CPU cores. Adding ! to a call sends suitable work to a GPU. Purity and affine values let the compiler know that two branches do not share mutable state. The programmer still has to divide work evenly, and the JavaScript target runs sequentially, according to Bend's parallelism documentation.
That combination is the project's unusual move. Existing proof assistants can verify formal claims, and GPU languages can run parallel kernels. Bend tries to put the specification and proof beside an executable program in one language that a coding agent can use. Its repository includes two papers, a Lean model of the core calculus, runtime benchmarks and proof-checker benchmarks. The public branch currently arrives as a single root commit labeled version 2.0.5, which makes the initial code drop harder to review as a sequence of changes.
The law is the part a human must get right
A Bend law is a type-level proposition. The guide's smallest example states that adding zero to any natural number returns the same number:
law add_zero:
for x: Nat
{Nat.add(x, 0 n) == x : Nat}
A definition with the corresponding name supplies the proof. Bend uses case analysis and recursion for induction, and the checker refuses an unfinished claim. The guide's convention keeps laws in a file the human controls while allowing the agent to edit the application and proof. That gives code review a smaller target: the specification and the trusted checking machinery.
The project suggests laws such as keeping the sum of all balances at zero or requiring a sort function to return values in ascending order. One compact invariant can cover many inputs that an ordinary test suite never enumerates. Bend's own materials go further and describe this as a route to bug-free agent code. The evidence supports a narrower claim: a valid proof rules out implementations that violate the encoded proposition, provided the checker and its assumptions are sound. The project demo shows that mechanism with a game whose law says the player cannot win.
That game also exposed the specification problem within hours of launch. In the Hacker News thread, one developer reported asking the agent to remove the walls. The result changed movement so that the character still could not win, satisfying the one law while damaging the game. Bend's author replied that the demo was deliberately under-specified and agreed that laws protect only the behavior someone remembers to encode. This is a community test, so it does not serve as an independent evaluation. Still, the exchange neatly locates the limit: the proof checked the written rule, not the user's unstated intent.
For an engineering team, that shifts the hardest review upstream. Someone still has to decide whether balances may be created, how rounding works, which callers are authorized and what happens during failure. A proof can cover each property after it becomes a precise proposition. The guide says Bend has no tactics or automated proof search, so writing and maintaining those propositions and proofs takes work even when an agent supplies the first draft.
The trusted base is still moving
Bend's repository separates the language kernel from the compiler. Its agent instructions identify bend2/bend.ts as the human-written parser and checker, including its type theory, while bend2/comp.ts contains the compiler plus the C, Metal, CUDA and JavaScript runtimes. The README's 99% AI-written disclosure applies to the compiler, not the kernel. This distinction matters because a source program can pass the checker and still depend on the compiler to preserve its meaning in the emitted executable.
The formal model has a gap of its own. A comment at the top of the Lean formalization says the specification does not yet fully match the bend.ts implementation and that implementation bugs could create inconsistencies. It calls for independent audits. The file models five properties for the live fragment, including progress and consistency, but it explicitly excludes several pipeline concerns and refuses unsafe definitions or unfinished proofs.
Bend also provides deliberate exits from the proof boundary. Marking a definition @unsafe disables the termination checker. Floating-point behavior is axiomatic, so the project says nothing about F32 can be proven. Host effects implemented through foreign C or JavaScript stay outside proofs and termination analysis. These are documented engineering choices in the language guide and limitations list, but they mean a green proof check cannot stand in for reviewing every unsafe or foreign component.
The surrounding developer experience is early too. Bend has no native Windows build, though WSL works. Its base library currently lacks TLS, HTTP, JSON and regular expressions. Strings are linked lists of characters. There is no language server, formatter, debugger or built-in test framework. The README states these gaps plainly. The current release fits research experiments and evaluation, while its missing application features rule out a drop-in stack for most teams.
Performance claims need reproducible runs
Bend aims for C-like single-core speed, CUDA-like GPU speed and faster checking than established proof assistants. The repository does contain runtime and checker benchmark programs, including matched implementations in other languages and hardware-specific reference files. Those are useful materials for reproduction. They remain project-authored measurements, and the README concedes that the checker does not yet have as many benchmarks as its author wants.
The runtime design also narrows where the speed pitch applies. A binary uses one GPU, one event loop and no multi-machine execution. Native compilation is slow, and useful parallelism depends on balanced branches. The project's guide recommends GPUs for uniform numerical work while steering divergent searches toward CPUs. Those constraints are more informative for an evaluator than the broad target of matching C and CUDA.
A sensible trial would pin the current commit, keep the program inside a disposable environment and write laws for one small component whose invariants are already understood. Then ask an agent for adversarial changes, including changes that obey the letter of each law while violating a nearby expectation. That exercise follows the workflow Bend documents and tests the same under-specification exposed in the launch thread.
An independent audit should come next. It needs to close the stated mismatch between bend.lean and bend.ts, then trace a proven law through emitted CPU and GPU binaries. Tagged, incremental releases would also let outside reviewers see how that trusted base changes. The 275-point launch already records developer curiosity. Bend's harder test is whether its laws still protect a program when reviewers treat both the coding agent and the toolchain as possible sources of error.