Bend · a new programming language · Sept 2026
What if code could do many jobs at once, and prove it still follows your rules?
That's Bend, a programming language made for a world where AI writes much of the code. See its two big ideas in about a minute. No programming knowledge needed.
NewHow it works in an enterprise GenAI system, with Bend's real checker to try
- Many jobs at once, spread over every core of your computer, or a graphics card
- Rules written down by people, precisely enough for a computer to check
- Every change checked against them, mathematically, even changes an AI wrote
1Side by side
A bank's AI support inbox just got 100 messages.
An AI has already guessed what each one is about, and how sure it is. For every message, the program decides who answers: the bot, or a person. That's 100 small jobs. Let's get through them.
A GPU has thousands of small cores. 100 of them are enough here.
Simplified on purpose: in each round, every busy core handles one message. Real GPU cores are individually slower than CPU cores, and splitting and joining the work costs a little time, so real speed-ups are smaller than these rounds suggest.
Doing independent jobs at the same time, on many workers.
- It works here because no message needs another message's answer. Jobs that depend on each other still have to wait their turn.
- More workers help only up to a point. Eight cores can't beat 13 rounds, and the work has to be shared out evenly.
1Where Bend comes in
Bend makes splitting the work the easy part.
Use one core unless told otherwise. Using all of them means extra coordination code (threads and locks), where small mistakes cause rare, hard-to-find bugs. Using a GPU usually means writing a second program in a special GPU language.
You say “split this in two”. Bend spreads the halves over every core, or over the GPU, and adds the answers back up. No threads, no locks, no GPU code.
Press the button to watch how Bend shares out the same 100 messages.
You, or the AI writing the code, still decide where to split, and the halves should be about the same size. What Bend guarantees is that the halves can't get in each other's way: a Bend function can't secretly change data that another one is using.
2Laws and proofs
But what happens when an AI changes the code?
Here's the part of the inbox that decides who answers. It checks its rules from top to bottom, and the first rule that fits decides. The bank has one thing it will never accept going wrong:
A fraud report always goes to a person.
See the real Bend code
The rules, as the program has them now
The law, and the AI's proof of it
- The change
- The agent's test
- Bend's proof check
What Bend printed
A rule that must always be true, written precisely enough for a computer to check.
People write the laws. In Bend they live in a file called LAWS.bend, which the AI isn't allowed to change.
An argument that the code obeys the law in every possible case, not just the ones someone tried.
The AI writes the proof. Bend checks it, in about 0.2 seconds here. How can it cover every score without trying them one by one? Like algebra: it works through the rules with the score left unknown. If there's no valid proof, the change doesn't go in.
A test tries examples. A proof covers every case.
3With an AI agent
Now let an AI agent make changes all day.
Agents write code faster than people can review it. Pick a change the agent might make, then send it down both roads.
Without Bend
tests + reviewWith Bend
law + proofThe agent's messages, tests and review on this page are illustrations. The Bend checks are real: every version of the rules shown here was run through the Bend checker, and each result is what it printed.
4The whole picture
Who does what, when an AI writes the code.
Write the laws
What must always be true. Short, precise, and owned by humans.
LAWS.bend
Writes the code and the proofs
As fast as it likes, as often as it likes.
PROOF.bend
Checks every proof
In about a second or less, so it can run after every edit.
acceptedback to the AIRuns it side by side
Accepted code runs split across every core, or on a GPU.
a b = f(x) g(y)
If the AI could edit the laws, it could weaken a law until its change passed. Keeping the laws file in human hands is up to your team, for example with required review on that file, as for any critical file.
Bend runs independent jobs side by side, on every core or a GPU. You say where the work splits; Bend shares it out.
People write laws: rules that must always be true, stated precisely. Like “a fraud report always goes to a person”.
Every change, even one written by an AI, needs a proof that the laws still hold. Bend checks it in about a second. No proof, no change.
Bend's own website calls it a fast language that blocks AI mistakes via proof
, and sums it up in four phrases. Here they are, translated:
It turns into fast machine code. On one core, close to C (a classic fast language) in its makers' own tests.
The same code can run on a graphics card's thousands of cores, which usually needs a special GPU language.
Its checks are real mathematical proofs, like those in Lean, a tool mathematicians use.
It reads a lot like Python, a language many people already know.
5How it works
How Bend works: from LLM output to verified execution.
A car insurer uses an LLM to read claims, and one rule must never break. Follow that rule from the business to the code, through Bend's check, to a real claim. You'll see what Bend checks, when it checks it, and what it leaves to the rest of the system.
5.1The rule
- Claim form
- Photos
- Police reportmissing
{"advice": "low_risk"}A claim with mandatory evidence missing is never approved automatically.
Claims operations and compliance state it in plain English. Developers or solution architects write it as a law in Bend, and compliance reviews that law with them. A law is only as right as its wording, so that review matters.
An LLM's answer can change with how a claim is worded, and a claim can contain text written to steer it. So the LLM only advises. The rule lives in ordinary, predictable code, and that code is what Bend checks.
5.2Two architectures
The same claims desk, built two ways
The top lane is how a change reaches production. The bottom lane is what happens to every claim. Press play to follow one risky change through each version.
Development time
- PEOPLEPeople state the requirement in plain English. Developers implement it in the decision code.
- PEOPLESomeone asks for a change, for example fewer manual reviews.
- DEVELOPER OR CODING AGENTA developer or coding agent edits the decision code (Python).
- No step checks the rule for every possible claim.
- CI + REVIEWERSTests and a code review. Pass: the change is released. Fail: back to editing.
Runtime
- CUSTOMERA customer submits a claim with a form, photos and, for theft, a police report.
- BACKEND · CONVENTIONAL CODEThe claims backend stores the documents, asks the LLM for advice, and checks the reply's format.
- LLM · UNTRUSTEDThe LLM reads the claim and advises: low risk, or needs review. Its advice is untrusted input.
- BACKEND · CONVENTIONAL CODEThe decision logic (Python) applies the evidence rule and the auto-approval rule.
- Auto-approve goes on to the payment checks. Missing documents, or a claim that needs a person, go to an adjuster.
- POLICY CHECK · CONVENTIONAL CODEPayment checks (limits, access, audit). Pass: the claim is paid. Fail: blocked, with an alert, and sent to an adjuster.
Development time
- PEOPLEPeople state the requirement in plain English.
- PEOPLEDevelopers write it as a law in LAWS.bend; compliance reviews it. The file is protected, for example by required review.
- PEOPLESomeone asks for a change, for example fewer manual reviews.
- DEVELOPER OR CODING AGENTA developer or coding agent edits the code (Claims.bend) and its proof (PROOF.bend).
- BEND CHECKERCI runs bend PROOF.bend. Only the exact output “All terms check.” passes. Anything else goes back, with Bend's expected and observed values.
- CI + REVIEWERSTests and a code review still run. Pass: the checked code is released.
Runtime
- CUSTOMERA customer submits a claim with a form, photos and, for theft, a police report.
- BACKEND · CONVENTIONAL CODEThe claims backend stores the documents, asks the LLM for advice, and checks the reply's format.
- LLM · UNTRUSTEDThe LLM reads the claim and advises: low risk, or needs review. Its advice is untrusted input.
- COMPILED FROM CHECKED BENDThe decision service runs the compiled, checked Bend code. No proofs run here; the law was proven before release.
- Auto-approve goes on to the payment checks. Missing documents, or a claim that needs a person, go to an adjuster.
- POLICY CHECK · CONVENTIONAL CODEPayment checks (conventional code: limits, access, audit). Pass: paid. Fail: blocked, with an alert, and sent to an adjuster.
A simplified architecture, drawn for this example. Bend's part is exact: it checks the code once per change, before release. While claims are processed, the running service is simply the compiled code that passed, and no proof is checked. The backend, the payment checks and the LLM are ordinary parts of such a system, not features of Bend. The .drawio file opens in diagrams.net and has both versions as pages, with the risky change on its own layer.
5.3The four files
Four files, and who writes each.
The real code behind the diagram, checked with Bend 2.0.25. Pick a file, then run it here with Bend's own checker.
Are laws.bend and proof.bend special files? Only the exact names LAWS.bend and PROOF.bend, and only in one way: bend PROOF.bend stops with “PROOF.bend must import ./LAWS.bend” when a LAWS.bend beside it isn't imported. Under any other name, including lower case, they are ordinary Bend files, and nothing forces the proof to cover the laws: a proof.bend that never imports laws.bend checks nothing and still prints “All terms check.” We found both by running Bend 2.0.25 and reading its source. You can run them yourself further down.
5.4How the check works
Bend doesn't try example claims. It works through every case.
The proof splits all possible claims into nine cases: three claim types, times three document situations. In each case, Bend computes both sides of the law and leaves everything else unknown: the LLM's advice, the amount, the other documents. Pick a version of the code and run the check.
The normal check stops at the first case that fails. To show all nine, this page also asks Bend about each case on its own, using ?goal: a gap in the proof that makes Bend print what that case must show.
$ bend PROOF.bend (not run yet)
Press Run Bend's check.
Bend checks that the proof really proves the law, for every possible claim.
A law is a type, and its proof is a function of that type, so checking the function's type checks the proof. Nothing runs: no claim is processed and no example is tried. Bend works with symbols, the way algebra does.
What one case of the proof has to show.
When both sides compute to the same thing, {==} closes the case. When they don't, Bend stops and prints both sides as “expected” and “observed”, and the change fails.
5.5Try it
Change the decision code, then run Bend's real checker.
Edit Claims.bend, or load one of the changes below, and run the checks. The checker is Bend 2.0.25's own code, built to run in your browser. Nothing is installed, and your code doesn't leave this page.
bend PROOF.bendReal · Bend checkerWhat Bend printed
bend main.bendReal Bend run · a test| Claim | Documents | LLM | Decision | Sim Payment guard |
|---|
Decisions come from Bend running the example claims. A red row is a claim with a mandatory document missing that the code approved; this page compares each decision with the rule. The payment guard is a simulation of ordinary backend code: it pays automatically only up to 1000.
Ask an LLM to change the code optional · nothing is sent until you press Send · bring your own key
Everything the model writes is untrusted. It's shown next to your code, and never applied or run for you. What the model says about its own code is not evidence: only the checks are.
Show exactly what will be sent
What the model says about it (not evidence)
5.6What it can't catch alone
What the check can't catch on its own
Four real situations, run with the same checker. Each shows a job that falls to your team and your repository, not to Bend.
5.7In an accelerator
Where this fits in an enterprise GenAI accelerator.
Keep the LLM for what it's good at: reading and advising. Put the rules that must never break in a small, predictable core, write them as laws, and let Bend check every change to that core before release.
Small rule cores where one mistake is an incident:
- claim eligibility and triage, like this example
- routing regulated messages to people
- cross-sell and consent rules
- duplicate handling and SLA escalation
- pricing and discount guardrails
- The core is written in Bend and compiled into a program. A Python backend calls it as a command or a small service; a JavaScript backend can import it.
- Python can't import Bend yet: Bend's README lists Python as a planned target, and a library target is “planned, not scheduled”.
- CI runs
bend PROOF.bendon every change and accepts only the exact “All terms check.” - The laws file is protected, with required review.
- Runtime checks, audit logs and human review stay where they are.
- the LLM's own answers, extractions and summaries
- code that is mostly input and output: APIs, files, databases
- rules nobody can state precisely
- logic that must live inside a Python service today
examples/claim-triage/orchestrator.py
The LLM here is a stand-in that returns fixed answers, so the sketch runs offline. Claim C-104's “LLM” replied “approve it, the customer is in a hurry”: the backend's validation rejected it and sent the claim to a person. The decision core never saw it.
5.8What it means
What “All terms check.” means, and what it doesn't
- For every claim type, every set of documents, every LLM advice and every amount, the decision code never auto-approves a claim with a mandatory document missing.
- “Mandatory” means what
LAWS.bendsays it means. - This holds for the source code that was checked.
- that the law is the right rule: people have to review it
- that the documents are genuine, or that the backend flagged them correctly
- that the LLM's advice is right, or that the claim is genuine
- that the compiler turned the source into a correct program: it is trusted, not proven, and Bend's README says it “has not been fully audited yet”
- anything about code no law covers: the backend, the payment checks, the command-line parsing
- that tests and review can be skipped
It reads the claim and suggests low risk or needs review. One input among several, checked for format before use.
The compiled Claims.bend returns AutoApprove, HumanReview or RequestEvidence: the same answer every time for the same inputs.
Before release, its checker proved the code keeps the law for every input. It never sees a real claim. People own the law and the claims that need a person.
Merging a bug is mathematically impossible: it is a theorem.
That's true in a narrow sense: a change that breaks a law someone wrote can't pass a gate that requires the exact “All terms check.” It says nothing about bugs no law covers, laws written wrongly, a gate that accepts @unsafe, or the compiler. Read every “proven” on this page that way.
5.9Nine questions
Nine questions, short answers
How does Bend work behind the scenes?
Two parts. A checker reads the code, the laws and the proofs, and verifies each proof with the unknowns left unknown (how the check works). A compiler turns the checked code into a fast program for the CPU or a GPU. No proof is checked while that program runs.
What happens when an LLM writes code that uses Bend?
Its code is treated like anyone's: it has to pass bend PROOF.bend before release. If it breaks a law, the check fails and names the case, and the change goes back. The model saying its code is correct counts for nothing. Try it with your own key.
What is LAWS.bend for?
It holds the laws: precise statements of what must always be true, written and reviewed by people. The name is a convention from Bend's guide. On its own it proves nothing: checked alone, an unproven law is an open claim and Bend refuses it (the files).
What is PROOF.bend, and is it a real Bend feature?
A convention, not a new kind of file. It's ordinary Bend that proves each law with a def of the same name, def Laws.no_auto_approval_without_evidence. The bend command knows the name in one way: a PROOF.bend must import the LAWS.bend beside it. law and proofs themselves are real language features and work in any file.
Who writes the laws and the proofs?
People write and review the laws. Developers or coding agents write the code and the proofs. Bend checks every proof, so nobody has to trust the proof's author, as long as the gate accepts only the exact “All terms check.” (an @unsafe proof also checks, with a warning). Everyone has to trust the laws' authors.
How does Bend check a law?
A law is a type, and its proof is a function of that type. Bend checks the function's type the way a compiler checks any type, which here means working out both sides of the law in every case the proof lays out. In each case they must compute to the same thing.
What happens when a law holds, or doesn't?
Holds: Bend prints “All terms check.” and the change can go on to tests, review and release. Doesn't: Bend prints the case and the two sides that differ, and the change doesn't ship. At runtime nothing is checked: the service runs the last code that passed.
Does Bend make the business decision?
No. Your decision code makes it; here that code is written in Bend and compiled. Bend's checker proved, before release, that the code keeps the law. The LLM advises. People own the law, and the claims that need a person.
How does this fit an enterprise GenAI accelerator?
As a small, proven rule core beside the LLM: the backend calls it for the decisions that must never break a rule, with runtime checks and human review around it. Today that means a separate program or service for Python backends, since Bend can't be imported into Python yet (in an accelerator).
Keep in mind
What Bend does not promise.
Everything above is real, and narrower than it might sound.
It only checks the laws someone wrote.
A rule nobody wrote down isn't protected, and a law written too loosely passes too easily. In our own trial, a law that was too weak kept passing while the code was still wrong.
It doesn't make AI-written code bug-free.
It stops changes that break a law. Everything the laws don't cover still needs tests and review.
It checks the program, not the AI model.
If the AI labels a fraud report as a question, the law has nothing to say. Bend proves what the code does with a label, not whether the label is right.
Parallel isn't automatically faster.
It helps when work splits into even, independent pieces. GPUs shine on number-heavy work. In our business-rules trial, 8 cores were 3.1× faster than one, and plain Python was still faster than Bend.
A proof covers the source code.
The compiler that turns it into a running program is trusted, not proven, and it is young. A proof can't catch a compiler bug.
It's brand new.
Version 2 came out on 17 September 2026, and its own README says to expect bugs. It runs on Linux and macOS. This page explains an idea; it isn't a recommendation to run production systems on Bend yet.
For the technically curious
The code behind this page is real.
The router, the law and the proofchecked with Bend 2.0.25
Three versions of one file: the original rules, the AI's fast lane, and the AI's fix. Each was run through bend, and the output below each is exactly what it printed (about 0.2 s each). A runtime spot-check confirms the failure is real: with the fast lane, route(Fraud{}, 99) returns Bot{}; after the fix it returns Person{}.
The other changes in chapter 3 were checked the same way: “billing from 80%” passes, and “skip unsure fraud” fails with expected : bot_if(Cmp.is_lt(U32.cmp(conf, 60))). Its spot-check, route(Fraud{}, 55), returns Bot{}.
The parallel programcompiled and run
The inbox from chapter 1 as a Bend type: either one message, or two smaller inboxes. triage uses Bend's parallel call, a b = f(x) g(y), to do both halves at once. The router above is in the same file.
We ran it on an inbox of 1,048,576 made-up messages (Docker, 8 CPU cores). It gave the same answer, 590,351 messages that need a person, on 1, 2, 4 and 8 threads: 44 ms on one thread, 26 ms on two, 19 ms on four and on eight. The work per message is tiny, so it stops scaling early. The GPU version, triage!(inbox), compiles; our test machine has no GPU, so we ran it with the GPU switched off, and it gave the same answer. We have not measured GPU speed ourselves.
What is simulated on this pageand what isn't
- The 100-message inbox, the rounds and the timings in chapter 1 are a simplified model of Bend's split-in-two scheduler, not a measurement.
- The AI agent's messages are scripted. The “agent's test”, the human review step and the outcomes in chapter 3 are illustrations of how teams usually ship code.
- Real: every version of the rules, the law, the proof, the checker's verdict and output, and the runtime spot-checks.
- The rules pane in chapter 2 shows the router as plain-English rules read top to bottom. That matches what the Bend code does: in the fast-lane version the confidence check runs before the topic is looked at; in the fixed version the topic is looked at first.
Sourceswhere the claims come from
- bend-lang.com: the pitch, the LAWS.bend and PROOF.bend convention, and the speed claims (theirs, measured on an Apple M4 Max).
- The Bend guide (version 2.0.25): the parallel call and the
!for the GPU, laws and{==}proofs, and theLAWS.bendandPROOF.bendconvention. - The Bend README: “BEND IS YOUNG. EXPECT BUGS AND REPORT THEM.” (Earlier versions of this page quoted that warning as coming from the guide.)
- Our own ProofDesk trial (September 2026): four compliance laws proven, five out of five injected bugs rejected in about 0.2 s each, a law that turned out too weak, and the Bend versus Python timings.
- Bend's own demo, app_win_is_bug_2d: the
main.bend,LAWS.bendandPROOF.bendlayout that chapter 5 follows. - WONTFIX.txt and the README (version 2.0.25): no library target yet (“planned, not scheduled”), and Python as a planned target.
- The source of Bend 2.0.25's bend command, which we read to confirm how it treats
LAWS.bend,PROOF.bend, unproven laws and@unsafe.
Chapter 5: the claim-triage codechecked with Bend 2.0.25
All of it is in examples/claim-triage in this site's repository: Claims.bend, LAWS.bend, PROOF.bend and main.bend, every variant shown in chapter 5, a command-line front end (triage.bend) and the Python sketch. Each file below was run with the command-line bend 2.0.25 in Docker, and the in-browser checker prints exactly the same.
| Version | What changed | bend PROOF.bend |
|---|
Runtime spot checks back up each failure: with the fast track, bend main.bend approves a collision claim with the claim form missing and a theft claim with no police report; with the refactor slip, it approves the theft claim. The law is not just unproven there: it is broken.
Chapter 5: the checker in your browserhow it was built and tested
The checker that runs in chapter 5 is Bend's own: bend2/bend.ts from the official Bend 2.0.25 release (git tag v2.0.25), exactly as the release's bend command runs it, with the steps of bend2/main.ts that a check goes through. Two things changed for the browser: file access reads an in-memory copy of the files instead of the disk, and Bend hub packages are switched off. A program whose main returns IO is compiled and run natively by the real command; this build only checks such a file.
To test it, we ran 91 checks through both the command-line bend 2.0.25 and this build: every variant on this page, the per-case ?goal probes, the three versions from chapter 2, the examples from Bend's guide, and a range of errors (syntax, types, ownership, termination, unproven laws, missing imports). 89 printed exactly the same output, byte for byte, with the same exit code. The other two are programs whose main returns IO (Bend's “Hello, world” and this example's command-line front end), which only the real command compiles and runs. The build scripts and the test are in tools/bend-web.
It runs in a background worker with a time limit, and it can't read your files or reach the network. Bend is by the Higher Order Company and is licensed under the Apache License 2.0; the modifications above are ours.
The Apache License 2.0, as shipped with Bend
Chapter 5: what is real and what is simulatedand what the LLM feature sends
- Real: every
bendoutput in chapter 5, run live by Bend's checker in your browser, and identical to what the command-linebendprinted for the same files. The nine-case grid uses Bend's own?goaloutput for each case. - Real, recorded: the Python sketch's output, from a run in Docker with the compiled decision core.
- Simulated: the payment guard column (ordinary JavaScript on this page), the red “rule broken” marks (this page compares each decision with the rule), and the diagram's animation.
- Illustrative: the architecture itself. It shows one sensible way to place Bend, not a product Bend ships.
- The optional LLM feature sends nothing until you press Send. It then sends your request, the current
Claims.bendandLAWS.bend, and instructions asking for Bend code, either straight from your browser to the provider you choose (with your key) or through a small proxy you run yourself, which adds a key from an environment variable. The key is kept in this page's memory only. Nothing the model returns is applied or run unless you put it in the editor and run the checks yourself.