May 2024's Bend is no proof assistant

Higher Order Company shipped Bend in May 2024. The pitch was narrow and it held up: write ordinary-looking functional code, and the runtime spreads it across a CPU or a CUDA GPU with thousands of cores. You write no threads, no mutexes, no CUDA kernels. A recursive function that would pin one core can saturate a graphics card, because Bend compiles down to HVM2, a runtime built on interaction combinators. In that model, independent work parallelizes without you asking for it.

The topic that brought you here, Bend blocking AI mistakes through proof, folds two true things into one claim that isn’t right. Bend is a parallel language. It is not a proof assistant. But the family Bend comes from, and the idea sitting one step to its left, is where the actual AI-safety story lives. The two are worth pulling apart before anyone builds a control on top of the wrong one.

Three kinds of AI mistake, and only some take a proof

AI systems fail in at least three separate ways, and a proof reaches some of them and not others. First, free-text errors: a model states a false fact, cites a paper that does not exist, or misreads a contract. Second, code errors: a model writes a function with an off-by-one, a SQL query missing its WHERE clause, an infrastructure change that opens a port. Third, action errors: an agent holding real tools sends the wrong email, deletes the wrong row, or wires money to the wrong account. Proof does nothing for the first class, because there is no machine-checkable definition of “true.” It does a great deal for the second and third, because generated code and generated actions can be checked against properties you write down. When someone tells you proof stops AI mistakes, ask which of the three they mean.

A proof is a spec the compiler won’t let you lie to

In a dependently typed language, the type carries a claim, and the compiler refuses code that can’t back the claim up. Idris lets you write a type like Vect 3 Int, a vector whose length of exactly three lives in the type itself. Append a wrong-length list and the program does not compile. Push this further and a sort function’s type says “returns a permutation of the input that is ordered,” and you cannot ship the function until you hand the checker a proof.

This is not academic. Gerwin Klein’s team at NICTA verified seL4, a microkernel, down to a machine-checked proof that the C implementation matches its specification, with no buffer overflows and no undefined behavior. Xavier Leroy’s CompCert is a C compiler carrying a proof that it preserves program meaning. When Xuejun Yang’s group fuzzed compilers with Csmith, they found miscompilation bugs in GCC and LLVM and found none in CompCert’s verified core. Amazon runs Dafny, TLA+, and the Zelkova SMT engine against S3, DynamoDB, and IAM policies. Proof-based tools already hold up systems you used today.

Bend is the fast language; Kind is the proof language

Higher Order Company builds both. Bend targets performance and rides HVM2. Kind, the same team’s dependently typed language, is the proof tool, and it compiles to the same runtime. The lineage is real: interaction combinators trace back to Yves Lafont and, before him, to Jean-Yves Girard’s work in linear logic, where proofs and programs are the same object. So the proof heritage attached to Bend is genuine. It just lives in the sibling project, not in Bend itself. If you want Bend for what it is, use it to make parallel code run on a GPU. If you want proof, you are reaching for Kind, or Lean, or Agda, or Dafny.

Bend removes one bug class by construction

Parallel code usually drags in its own failures: race conditions, deadlocks, results that depend on which thread finished first. Bend’s runtime avoids that class. Interaction combinators are confluent, so the computation reaches the same result no matter the order the machine evaluates it, and no matter how many cores run at once. The thousand-core run computes what the single-core run would compute. This is not a proof that your program is correct. It is a guarantee that parallelism did not corrupt it, which is a separate promise from the ones a type checker makes, and a valuable one, because concurrency bugs are among the hardest to reproduce and the easiest for an AI to write. This is also the closest Bend itself gets to the safety claim in the title.

You cannot prove a neural network won’t be wrong

A proof needs a formal specification, a predicate a machine can check. “Don’t hallucinate” is not one. For open-ended text there is no formal definition of a correct answer, so there is nothing for a checker to verify against. This is the ceiling, and no language moves it.

What you can verify is narrower and still useful. Guy Katz and collaborators built Reluplex and then Marabou to prove bounded properties of neural networks: that within an epsilon-ball around an input, the output label does not flip. The α,β-CROWN tools win the annual VNN-COMP benchmark doing exactly this at scale. The standard test case is ACAS Xu, an aircraft collision-avoidance network, where you can state and prove “in this input region the system never advises a turn into the intruder.” That works because the property is formal and the input space is bounded. None of it promises a chatbot won’t invent a citation, because “invent a citation” has no spec.

The checker is the safety mechanism, not the model

Here is the pattern that actually reduces AI error: stop trusting the generator, and trust the checker. The model proposes a candidate. A proof system decides whether the candidate is admissible. When an AI writes code in a dependently typed language, “it type-checks” means “it satisfies the specification you wrote.” DeepMind’s AlphaProof made this concrete in 2024, generating candidate proofs in Lean for International Mathematical Olympiad problems and keeping only the ones Lean’s kernel accepted. The generator failed on most single attempts. The output was still sound, because a wrong proof never survived the checker, and the system reached a silver-medal score anyway. That result is about architecture, not about a smarter model. The idea is older than the current wave: George Necula formalized proof-carrying code in 1996, shipping a program alongside a proof its host can check before it runs.

Picture an agent that manages cloud infrastructure. It proposes a Terraform change to open access for a new service. With no gate, a hallucinated CIDR block of 0.0.0.0/0 ships to production and exposes the database. With a gate, the plan first runs through a policy checker that proves every security group rule satisfies your declared property, deny anything wider than a /24 reaching in from outside the VPC, before apply runs at all. The model still makes the mistake sometimes. The mistake never reaches the network.

You can build this without a research budget. Three concrete moves.

State the property you care about, in a form a machine checks. “This function never returns a negative balance.” “This generated firewall config opens no port except 443.” A proof is worth exactly as much as the spec behind it, so write the spec first.

Put the model behind a verifier that runs before anything executes. If the AI writes SQL, run it against a schema and constraint checker before the query touches the database. If it writes an IAM policy, run it through Zelkova before you apply it. If it writes a state machine, run a model checker over the properties you declared.

Keep the trusted core small. A hundred-line checker you can read beats a hundred-billion-parameter model you can’t. The whole point is to move trust off the thing you can’t inspect and onto the thing you can audit line by line.

The cost, stated plainly

Proof is slow to write. The seL4 effort ran to roughly 200,000 lines of proof for about 10,000 lines of C, a ratio near twenty to one, and it took years. Dependent types carry a learning curve most teams never climb. Bend and HVM2 are young: the runtime is fast on paper, but the ecosystem is thin, error messages are rough, and automatic parallelism carries real per-interaction overhead that can erase the GPU win on the wrong workload.

You spend this budget where a class of error is expensive enough to earn it. Kernels, compilers, cryptographic code, financial invariants, aircraft and medical control loops. You do not spend it proving a marketing form validates an email address. The skill you are buying is not writing proofs. It is deciding which properties are worth the tax and stating them clearly enough that a machine can hold you to them.

Bend will not stop an AI from being wrong, and nothing will, because a probabilistic model can always emit a wrong token. Proof-based languages change where the wrong answer lands. Instead of reaching production and costing you a breach or an outage, it hits a checker that says no. The safety does not come from the model getting smarter. It comes from you refusing to trust it, writing down the property that matters, and building a gate strong enough that “it passed” is a sentence you can defend to an auditor.