Teach your AI toBEND
An unofficial guide to Bend.
Bend is a brand new, rather amazing language, built for agentic coding: safe, formally verified and massively parallel. Humans state what the code must do and must not do, the AI writes it, and if the code misses the goals the compiler refuses to build it. Everything also compiles to the GPU, so whatever can run in parallel does, with no extra work.
Bend is developed by HOC, led by @VictorTaelin. This site is not affiliated with them.
01 · vibe coding
Bend is for vibe coding.
Bend was built for coding with an agent, and it wants a different shape of work. You do not describe the code. You state what it must do and must never do, and the compiler refuses to build anything that misses.
How it works
A specification in Bend is ordinary code. Write the law, leave the implementation empty, and the build fails until something fills it. The law is in the file, and the file does not compile without it. Bend's convention is two files at the root of a project: LAWS.bend, where you state what must hold, and PROOF.bend, where the AI proves it. bend PROOF.bend is the gate.
How Bend helps
That splits the work into two halves that are not worth the same. Deciding what a thing must obey is the expensive thinking, and it is short. Writing something that obeys it is long, repetitive, and gradeable by a machine.
So have the big model write the laws and stop. Then hand the file to a small, cheap model and let it grind overnight with nobody watching: it cannot claim a success it did not earn, because the checker has no opinion. Whatever is left needs a real idea, which is when you pay for the expensive model again.
How to use it
Give your agent the guide, then ask it for laws rather than code. Bend's syntax is inspired by Python, so your AI already knows how to write it. Bend's makers now sell the second half as a service, Bender, an AI that writes your proofs by the credit; the split is the same whichever model does the grinding.
write the laws, leave the bodies empty
# then the cheap one, in a loop, until the TODO count stops falling
bend PROOF.bend
The panel replays a real session on rat.bend, a rational-number library written for this project and not carried on this site: forty-one claims written in one sitting, most closed overnight by a smaller model, and the last few handed back because they needed an argument rather than another attempt.
02 · math bending
Proofs about every number at once.
The plainest way to see what Bend's checker does is to point it at mathematics, where the claims are unambiguous and the verdicts are not negotiable. You write a claim as a type, and Bend either proves it for every value at once, or it does not build.
How it works
A claim like sqrt2_is_irrational is an ordinary Bend definition whose type says "there are no naturals p and q with p² = 2q²". A program of that type is the proof, and type-checking it is checking the proof. Nothing is trusted because it passed a few inputs.
How Bend helps
The checker gives three verdicts and only three: proved, refuted, or open. An agent can work a claim from both ends, searching small values for a counterexample while trying to build the proof, and whichever lands first settles it. A refutation comes with the number that breaks the claim.
If you have met Lean, this will look familiar, and the difference fits in one sentence: the program you proved is the program that runs, on every core and the GPU, with nothing trusted in between. Lean has no GPU backend, its parallelism is something you ask for, and when a proof is about a model with a fast version swapped in underneath (@[implemented_by], @[extern], native_decide) the kernel does not check that the two agree. That gap is not theoretical: in September 2026 Trail of Bits published a proof of Fermat's Last Theorem that fits the margin, built from exactly one such disagreement, and Lean checked it. In Bend the proved program is the program, so there is nothing to swap and nothing to drift.
Do not read that as immunity. Every proof rests on something; here it is Bend's checker and compiler, both far younger than Lean's, with no second implementation to cross-check them. Lean is far ahead where it counts most: years of kernel work, and Mathlib, a decade of mathematics by thousands of people against this site's one folder. Nobody has benchmarked the two, so this site will not tell you which is faster.
How to use it
Write your claim as a law, run the checker, and read whether every term checks or how many laws are still open. The naturals, integers, reals and proofs these rest on are not in Bend's standard library and are not going to be, so this site keeps them: lib/math.
bend PROOF.bend
# Error: 1 TODO found.
# The code is incomplete, and not a valid proof yet.
The conversation in the panel runs the real script: the Mersenne pattern dies at p = 11, √2 is proved irrational by Euclid's descent, and Fermat is proved for n = 4 and left open in general.
03 · fractal bending
One escape loop, a million times over.
Escape-time fractals are the friendliest parallel workload there is: every pixel runs the same short loop on its own coordinates, and no pixel needs to know what any other found. That is exactly the shape of program Bend was built to spread out.
How it works
The kernel is a handful of lines: iterate z ← z² + c until it escapes a radius or hits a cap, then colour the pixel by how long it took. Mandelbrot, the Burning Ship, the Julia gardens and the Newton basins in the box are the same program with one line changed. Mandelbulb and Mandelbox march a ray through a distance field instead, but the shape of the work is the same.
How Bend helps
You write the per-pixel function and fold it over the image: no kernel, no thread pool, no tile scheduler. The same source compiles to native code for the CPU and to Metal or CUDA for the GPU. Ten cores come out at about seven times one core, roughly all the hardware has to give. The GPU reaches a hundred times on the Mandelbrot dive and the Mandelbox, sixty on the Mandelbulb: a million pixels is a million independent pieces of work, with no blocks to size, no buffers to copy, and no data race available to you. The numbers under each render are medians on an idle M1 Max against a C port of the same kernel.
Bend is like CUDA, but with formal proofs. This section is the CUDA half. The proof half is the same language: the per-pixel kernel and the fixed-point numbers the deep zoom falls back on are ordinary Bend, so a claim about them is written next to them, checked by the same tool, with no rewrite into something else first. The proofs on this site are in the math and chess sections.
How to use it
The Mandelbrot kernel lives in the Bend repo at bench/runtime/mandelbrot, next to the C, TypeScript and Lean ports it is measured against. Past a certain depth 32-bit floats stop resolving the detail, and the dive needs fixed point instead — also kept here, in lib/fixed.
bend main.bend -o mandelbrot
./mandelbrot --threads 10
# or the GPU, when the source calls its kernel with a !
./mandelbrot --gpu 4GB
Keep scrolling to walk through the renders, or use the arrows.
04 · gamedev bending
Rules the code cannot break either.
Every game stops its players breaking the rules. What no game manages is stopping its own code: the rules live in scattered conditionals, and they hold only because the tests caught the cases somebody thought of. A rule is only as true as the last bug you found.
How it works
TinyChess is chess cut down until the whole of it fits inside a proof: a four-by-four board, three pawns and a king a side, and one sentence the build has to keep. White cannot win on the first turn. That is not a test. It is a law, and the compiler will not produce a game that breaks it.
How Bend helps
The law needs no clever argument, because it is about one position, the one the game starts from, and a board this small can simply be tried. The checker plays every first move white has, every reply black has, and finds no mate. That search is the proof. The written argument is two characters long.
law white_cannot_win_on_the_first_turn:
{winning_first_move(position()) == no_move() : Step}
# PROOF.bend
def Laws.white_cannot_win_on_the_first_turn():
{==}
It asks for the move rather than a yes or no on purpose: when the law breaks, the checker prints the mate it found against the emptiness it was promised, and hands you the refutation instead of just refusing.
Which is why the demo is the part where you add a piece. Turn the pawn beside white's king into a queen and the same search finds a win on move one, so the sentence is false, so the file does not build. You did not break a test. You broke the sentence, and the sentence is load-bearing.
How to use it
It is written. Board, moves, captures, check, mate and stalemate all check, and the law above is proved in about a tenth of a second.
# Error: 7 TODOs found.
# The code is incomplete, and not a valid proof yet.
Four of the seven are the movement laws, stated over every natural number rather than the sixteen squares, so the search in the editor is evidence and not a proof. The other three are the general laws, quantified over every board: that you never capture your own piece, that a legal move never leaves your own king attacked, that mate implies check. Those need induction over the rules, and nobody has written it. They are the bounties. Two movement claims are false on purpose: uncomment one in the editor and the search walks the sixteen squares until it finds the pair that breaks it.
Everything in the panel's conversation is real output, and every position in it is a claim the file keeps: that a queen each keeps the law, that white's queen alone destroys it naming Q c1–c2 as it goes, and that a knight alone does not.
05 · raytrace bending
A black hole, one ray at a time.
Gargantua is a ray tracer that bends the rays themselves. Light near a black hole does not travel in straight lines, so each ray is integrated step by step through curved spacetime until it falls in, hits the accretion disc, or escapes to the sky.
How it works
Every pixel launches a ray and marches it through a Schwarzschild metric, picking up colour from the disc as it crosses. The disc is Doppler-shifted and beamed, the sky is lensed into the photon ring, and the whole frame is the same integration run once per pixel with no communication between them.
How Bend helps
Path integration is expensive per ray and perfectly independent across rays, the best case for Bend. The same source runs on one core, on ten, or on the whole GPU: the frame that takes forty-two seconds on a single core takes half a second on the GPU.
How to use it
The black hole in the box is this site's own tracer, written on the pre-release compiler and not yet ported to the released one, so its source is not published. Bend's own ray tracer demo, a ray-marched field of spheres, is the one to start from; it builds and runs the same way:
bend main.bend -o raytracer
./raytracer --gpu 4GB
The clip in the box is this site's own Gargantua render: eight passes per frame, twelve seconds of orbit.
06 · life bending
Every cell, every step, at the same time.
Cellular automata and particle systems are the other classic parallel shape: a grid or a swarm where every element updates from its neighbours, and the whole world steps forward at once. Lenia, Conway's Game of Life and Particle Life are three points on that line.
How it works
Lenia is the Game of Life made continuous: a smooth kernel instead of eight squares, three coupled channels instead of one bit, and creatures that glide and wobble rather than tick. Life itself is the discrete original, a binary grid with a three-line rule. Particle Life drops the grid: a few thousand particles, each attracted to or repelled by every other according to a small table of species rules.
How Bend helps
The trap in all three is layout, not logic. Lenia gets a seven-fold speed-up on ten cores once each cell owns its own halo of neighbours, and is slower than a single core when the fork happens per tile instead of per cell. Bend gives you the parallelism for free, but the data layout is still yours to get right.
How to use it
Lenia and Particle Life in the box are this site's own, written on the pre-release compiler and not yet ported to the released one, so their source is not published. Bend's own Game of Life benchmark is the same shape and builds the same way:
bend main.bend -o life
./life --threads 10
Particle Life ties on the GPU rather than beating the cores — all-pairs forces are memory-bound.
07 · your agent
Teach your AI to Bend.
Bend was built for agentic coding, but it is new, so your agent has not read about it yet. The fix is small: install Bend, and tell the agent to run bend guide, which prints the whole language. Five lines in your AGENTS.md, and it writes Bend.
Each section above has its own version of this button, because each needs something different: Bend itself from bend-lang.com, and the number theory, fixed-point arithmetic and chess from this site's library, where they live since they are not in Bend's standard library and are not going to be.
Paste the prompt into your AI and it sets itself up, reads everything, and then, from what it already knows about you, suggests where Bend would improve your own work. Or pick your agent and install the guide from the terminal in one line.