Five months ago I wrote that Gleam was the best language for LLM-assisted development, and I gave the argument an expiry date. It would hold until a proof checker got fast enough to sit inside an 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 called Jev into early access. You ask it typed questions and it returns probabilities, no text. I'd been waiting for the first one since April. The second one I didn't know to wait for, and it turns out to be the same idea pointed at a different problem.

The model proposes, and something I wrote decides whether the proposal is any good. For that to happen I need to write down two kinds of rule, and this week each kind got a tool.

What I have to write down

The first kind is a law: something that must be true of every run, no exceptions. 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. If the process dies halfway through a write, the ledger still adds up.

A test checks a few of those cases and hopes, and a type doesn't see them at all. A law states them for every input, and the agent has to hand over a proof before its code gets through. I read the law file instead of the implementation. It's short, and it's mine.

The second kind is a principle: something that's usually true and has to be weighed against other things that are usually true. An upset customer deserves a person. A question a canned answer can settle shouldn't go to a person. Those two collide the moment an upset customer asks for their balance, and no proof settles it. Somebody has to decide how much upset counts against how trivial the question is. That somebody should be me, and the decision should be a number in my code, not a vibe in the model's context window.

In both cases the model does the work and something deterministic does the deciding. The decider has to be deterministic because a smarter model still samples. If the thing reading its output is another model, congrats, that's another sample. The verdict has to come from a compiler or an if-statement with a threshold in it.

Once that's in place an agent can run for days. It picks up a responsibility, chews on it, and I hear from it when there's a decision only I can make, not every time something happens. My job becomes writing the laws and the weights: what must never happen, and what the agent brings to me instead of deciding alone. That's the part of engineering I like most, and it's the part agents are worst at.

Bend is the tool for laws, Jev for principles.

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 skipping the parallelism (cool btw, go read about it) for the proof loop.

A law is a proposition. A proof is a def with the same name, and its type is that proposition. That's the dependent types trick: a proposition is a type, and any value you can construct of that type is a proof of it. Here's the money law from the list above:

# LAWS.bend
law money_only_moves:
  for ledger: Ledger
  for transfers: List<Ledger.Transfer>
  {Ledger.total(Ledger.replay(ledger, transfers)) == Ledger.total(ledger) : Nat}

Any ledger, any list of transfers: replay them and the total is what it was. Not the handful of cases a test author thought of, but every input. The checker won't accept the agent's code until def Laws.money_only_moves type-checks. The other three laws from the list get written the same way.

Bend pairs the checker with a convention for agents, and the convention matters as much as the checker. LAWS.bend is yours. An AI can help you draft it, but you keep it, and the agent doesn't touch it. PROOF.bend, where the proofs go, and the code itself 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 speed is what makes this a loop. 12,800 definitions checked in 0.295 seconds, where Lean, the proof assistant most people would reach for, takes 36 seconds. It's their number on their fixture, but the order of magnitude means fifty retries in under a minute. In April that loop didn't exist.

Fifty retries matters because the model needs them. In April I wondered whether an agent could get a proof past a checker at all. Last September, off-the-shelf models turned 27% of formal Lean specs into code the checker accepted. This May, given fifty tries each, GPT-5.4 got 95%. The checker says no, the model tries again, and that's enough, apparently. If the checker is doing the judging, the model only affects how many tries it takes. I'd bet a cheaper model with more retries gets to the same proof, and either way I stop caring which model wrote the code.

One thing didn't ship. NeoGen, the synthesizer April's post leaned on, and SupGen alongside it aren't in this release, and I hope they come back. And no release will fix this: no checker can tell you that the law you wrote is the law you meant. The checker proves the law as written. Whether that's the right law has always been the hard part, and it's still mine.

Jev, where principles get a number

Back to the same bank, and the upset customer asking for their balance. Two principles pull on that message: a person for the upset customer, no person for a question a canned answer can settle. Here's how everyone handles that 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 no amount of pleading in the prompt makes it better.

And the third: the prompt asks the model for two decisions when it should make one. The first decision is what this customer wants. The second is how much their being upset should count against what they asked for. That second decision is the principle, and the prompt hands it to the model twice. Once in words: "if they seem upset, pick support, unless a canned answer will do" is the model deciding how much upset counts. Once in the number: the model writes the confidence, so the model decides whether your > 0.9 check fires. You never see how upset it thought the customer was, or how much that mattered. You see a verdict.

DSPy fixes the first problem. Typed signatures kill the parsing, and GEPA, its prompt optimizer, makes the action right more often, which is worth having. I burned a lot of tokens on that. Worth it, I tell myself. But the confidence is still a number the model typed, just with a float annotation now, and the principle is still in the prompt. GEPA's own confidence adapter doesn't ask the model for a number at all. It reads logprobs, the model's own token probabilities, which tells you what its authors think of a confidence the model typed.

Jev fixes the first two by not generating text at all. TypeSafe calls it a System One model, in the fast-judgment-no-deliberation sense: you send it a state and typed questions, and it answers without talking. A Noul is a yes/no question and comes back as a probability. A Choice is a question with options you declared and comes back as a distribution over them plus a confidence. 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 right about nine times in ten.

The third problem is fixed by what you ask. You don't ask Jev what to do. You ask it the facts each principle turns on. Is this customer upset? Would a canned answer settle this? Plus the question the old prompt was already asking, what does the customer want. Each question carries criteria for what a yes and a no look like, so the model reads them the way you would:

user_message, account_id = request.message, request.account_id

answers = client.system_one(
    state=user_message,
    questions={
        "action": Choice(
            instructions="What is the customer trying to do?",
            criteria={
                "check_balance": "View account balance",
                "approve_transfer": "Approve the pending withdrawal",
                "support": "Get help with an issue",
            },
        ),
        "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",
            },
        ),
        "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

Three questions, no decisions. For an angry customer asking for their balance, upset might come back at 0.85 and trivial at 0.9. Those are the two numbers the old prompt decided in the dark.

The principle is what you do with them, and that's yours:

upset = answers["upset"].noul      # probability the customer is upset
trivial = answers["trivial"].noul  # probability a canned answer settles it

needs_person = 0.7 * upset + 0.3 * (1 - trivial)

That line is both principles and their collision. "An upset customer deserves a person" is the 0.7. "A canned-answer question shouldn't go to a person" is the 0.3, pulling the other way. Nothing the model read can move the weights.

The rest is a threshold and a dispatch, and a transfer always gets a confirmation:

action = answers["action"]

if needs_person > 0.6 or action.confidence < 0.5:
    route_to_human(user_message)
elif action.choice == "check_balance":
    show_balance(account_id)
elif action.choice == "approve_transfer":
    ask_user_to_confirm(account_id)
else:
    route_to_human(user_message)

Yes, that's a confidence threshold, the thing I complained about in the prompt version. The difference is where the number comes from. The old one was typed by the model. This one is computed from the spread of the distribution over the three actions, and the distribution is what Jev is trained to calibrate.

Before, all of it happened inside the model: how upset the customer was, how much that mattered, which principle won. Now the model answers questions and you own the weights. If too many upset customers are ending up at the FAQ, you raise 0.7, not the English, and you don't re-test a prompt. A third principle is a third question and a third weight. The first two don't move, because Jev answers each question on its own and doesn't know the others exist.

The weights being mine doesn't mean typed once and left forever. I can tune them from last month's outcomes or fit them outright. But then they're fixed, and the model's read of this one message can't move them. That's the same shape as the law file: a short thing I own that the model works inside.

What this does to the job

A proof gate and a weighted threshold are checks, and checks already exist for humans: compilers, schemas, tests, database constraints, permissions, budgets. A human proposes a few changes a day and an agent proposes thousands, so checks that were optional for us stop being optional for them. There's no version of this where I keep up with the output. I couldn't if I wanted to, and I'm not going to pretend a second model reading it for me is any better. The only thing that keeps up is a rule that runs on every attempt and reads the ten-thousandth one the same way it read the first. So that's what I end up reviewing: the law the code has to get past, once.

The work moves up: from implementation to interfaces to tests to invariants to laws to intent. The law file and the weights are the same kind of artifact, 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. 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.