Five months ago I wrote that Gleam was the best language for LLM-assisted development, and that the argument had an expiry date. It would hold until a proof checker got fast enough to sit inside the agent's retry loop. After that, code would carry a proof instead of a test suite and the post would be obsolete.

Well. Three days ago Bend 2 shipped with a proof checker fast enough to run on every edit. Five days ago, a company called TypeSafe put a model into early access that returns typed decisions with probabilities instead of text. I'd been waiting for the first one since April. The second one I didn't know to wait for.

What I want

I write down the things that have to be true and that I don't trust a test to cover. Stuff like: money only ever moves, it never appears or disappears. If a request times out and gets retried, the second run can't do anything the first one didn't. Nobody reads another user's rows, ever. If the process dies halfway through a write, the ledger still adds up. A test pokes at a few cases of those and hopes. A type doesn't even see them. A law says it for every input, and the agent has to hand over a proof before the checker lets the code through. I don't read the implementation. I read the law file, which is short, and I read it because it's the only thing that's mine.

Then there's everything I can't write as a law. An upset customer deserves a person. A question a canned answer can settle shouldn't cost one. Two messages from the same person about the same thing are one escalation, not two tickets. Those are principles, and a principle decides nothing on its own. It's a reason. A law gets checked. A principle gets weighed against the other reasons, and that takes two things. How strongly the reason bears on this message, how upset this customer is, is a judgment. How much that reason counts against the others is a choice, and the choice is mine.

Agents run for days. They pick up a responsibility, chew on it, and I hear from them when there's a decision only I can make, and not every time something happens (please).

And my job becomes deciding the invariants. What must never happen, which states are valid, what the agent gets to decide alone and what it has to bring to me. That's the part of engineering I like most, and it's the part agents are worst at, so it's a good trade.

None of that comes from a smarter model. A smarter model still samples, so its output still has to be read by something, and if that something is another model, congrats, it's another sample. Whatever reads it has to give the same verdict every time for the same input. That's a compiler, or a proof checker, or an if-statement with a threshold in it, and it isn't another model. The model gets the search space. It doesn't get to say whether it succeeded.

Bend, where laws get checked

Bend 2 is a dependently typed language with Python's syntax that compiles to C, CUDA, Metal and JavaScript. I'm going to skip the parallelism (very cool btw, go read about it) and talk about the proof loop.

A law is a proposition. A proof is a def with the same name whose type is that proposition. From the launch demo:

# LAWS.bend
law you_cant_win:
  for moves: List<Game.Move>
  board = Game.replay(Game.start(), moves)
  {Game.is_won(board) == False{} : Bool}

Bend pairs the checker with a convention for agents, and the convention is the good bit. LAWS.bend is yours. An AI can help you draft it, but you read it, you keep it, and the agent doesn't touch it. PROOF.bend and the code belong to the agent. bend PROOF.bend fails while any law is unproven, and the agent runs it before every commit until it passes. "AGENTS.md backed by proof" is how the README puts it.

The benchmark made me sit up. 12,800 definitions checked in 0.295 seconds, where Lean takes 36. It's their number on their fixture, but the order of magnitude means fifty retries in under a minute, which is the loop I said in April didn't exist.

In April I also wondered whether an agent could get a proof past a checker at all. Turns out yes. Last September, off-the-shelf models given one shot got 27% of Lean specs past the checker. This May, given fifty tries each, GPT-5.4 got 95%. The checker says no, the model tries again, and that's enough, apparently. It also means the model doesn't have to be the expensive one. It only has to search well enough to satisfy the checker, and I stop caring which model wrote the code (I already mostly don't).

I'd heard about SupGen and NeoGen, the synthesizers that were supposed to fill holes in programs so the LLM wouldn't have to. Neither is in the release, and neither is the HVM runtime they ran on, and I don't know whether they're coming back. I hope they come back. April's post named NeoGen as the other half, and a synthesizer that enumerates programs finds proofs a model wouldn't guess. But the part I needed was the blazingly fast™ checker, and that shipped.

A checker proves the law as written. Whether the law is the one you meant stays your problem. This has always been the hard part.

Jev, where principles get a number

Most of what an agent decides is a principle, not a law. Here's how you handle one today:

prompt = f"""You are a support agent. Read the message and decide what to do.
If the customer seems upset, pick "support" even if they asked for something
else, unless a canned answer will settle it. If you're unsure, pick "support".
Reply with JSON only:
{{"action": "check_balance" | "approve_transfer" | "support",
  "confidence": 0.0 to 1.0}}.

Message: {user_message}"""

reply = llm(prompt)
decision = json.loads(strip_code_fences(reply))  # usually fine
if decision["confidence"] > 0.9:
    do(decision["action"])

Three things are wrong with this and everyone who's shipped it knows all three. The JSON isn't always JSON, so there's a strip-the-fences helper and a retry, and one day it returns "approve_transfer " with a trailing space. The confidence is a number the model typed. It says 0.9 for nearly everything, being wrong doesn't lower it, and nothing about the number gets better when you plead with it in the prompt. And there are two decisions here, not one: what does this customer want, and how much does that count against everything else. The model should only be making the first. But "if they seem upset, pick support, unless a canned answer will do" hands it the second, and the confidence field hands it the second again, because your 0.9 is checked against a number the model chose. The model is doing the weighing, upset against trivial against what they asked for, and you never see the numbers it used. The only thing your code decided was to trust it.

DSPy gets you halfway. Typed signatures kill the parsing, and GEPA, its prompt optimizer, makes the action right more often. I burned a lot of tokens on that. Worth it, I tell myself. The confidence is still a number the model typed, just with a float annotation now, and the policy is still in the prompt. GEPA's own confidence adapter doesn't ask the model for a number at all. It reads logprobs.

Jev doesn't generate text. You send it a state and typed questions, and it returns a probability for a yes/no, or a distribution over options you declared plus a confidence. There's nothing to parse because it can't return anything outside the options. The probabilities are trained to mean something: across all the calls where it puts an option at 0.9, that option is the right one about nine times in ten. The confidence is a separate number that says how peaked the distribution is. For principles, that changes what you can do with them. Each principle turns on a question about the message, and Jev answers the question. The principle itself, and how much it counts, stays in your code:

answers = client.system_one(
    state=user_message,
    questions={
        "action": Choice(
            instructions="What is the user trying to do?",
            criteria={
                "check_balance": "View account balance",
                "approve_transfer": "Approve the pending withdrawal",
                "support": "Get help with an issue",
            },
        ),
        # principle: an upset customer deserves a person
        # so: how upset is this one?
        "upset": Noul(
            instructions="Is the customer upset?",
            criteria={
                "true": "repeating a complaint, or threatening to leave",
                "false": "asking a question, or annoyed but still asking",
            },
        ),
        # principle: a question a canned answer can settle shouldn't cost one
        # so: would a canned answer settle this?
        "trivial": Noul(
            instructions="Can a canned answer settle this?",
            criteria={
                "true": "a balance, a due date, a link to a page",
                "false": "anything that needs a decision or an apology",
            },
        ),
    },
).answers

action, upset, trivial = answers["action"], answers["upset"], answers["trivial"]

# the weighing: mine
needs_person = 0.7 * upset.noul + 0.3 * (1 - trivial.noul)

if needs_person > 0.6:
    route_to_human(user_message)
elif action.confidence < 0.5:
    route_to_human(user_message)
elif action.choice == "approve_transfer" and action.confidence > 0.9:
    confirm_then_execute(account_id)
elif action.choice == "approve_transfer":
    ask_user_to_confirm(account_id)

Before, the principle was a sentence in the prompt, and everything about it happened inside the model: how upset it thought the customer was, how much that mattered against a balance request, how it settled the clash with the canned-answer rule. You got a verdict and nothing else. Now the principle is a question Jev answers and a coefficient you own, and each of those things is yours to see and change. How upset it thought the customer was is in the log, 0.82. How much upset counts is 0.7, and you change it by editing 0.7, not by rewriting English and re-testing the prompt. A third principle is a third question and a third coefficient, and the first two don't move, because Jev doesn't know the other questions exist. And when two principles conflict, the resolution is a line of arithmetic you wrote, not whatever the model felt like that time. The model still does the reading. The principle, its weight, and every conflict between principles moved out of the prompt and into code. Not mine as in typed once and left forever. I can tune the coefficients from what happened last month, or fit them, and then they're fixed, and the model's read of this message can't move them.

What this does to the job

Every one of these gates already exists for humans: compilers, schemas, tests, database constraints, permissions, budgets. A human proposes a few changes a day and an agent proposes thousands, so gates that were optional for us stop being optional for them. A law or a threshold applies to every attempt at any volume without getting tired, and my review moves from the output to the rule.

The work moves up, from implementation to interfaces to tests to invariants to laws to intent. The law file and the weights under each principle are the same kind of artifact, small and mine, and they're where the bugs live now. A wrong law is wrong on every run, which is a better place for a bug than spread across ten thousand lines nobody read.

Since April

Then, the excuse was that the checker didn't exist. Now it does and the model can iterate against it, so the remaining work is writing the laws and the weights, which was always going to be the job. Good.

The model gets the search space. The system keeps the verdict.