A few weeks ago I was cleaning up a checkout flow in a SwiftUI app I've been maintaining, and I asked Claude to help me tighten up the validation logic before an order could be marked confirmed. It happily generated a pile of guard statements spread across six functions, plus a matching pile of unit tests to back each one up. It worked. Tests were green, the demo looked fine, and I moved on to the next ticket without thinking too hard about it.

Then I read Liam Powell's post about Bend 2, the new language that markets itself as built for the "AI coding era" — you write the rules, the AI writes the implementation and a machine-checked proof that it obeys them. Powell went and counted what Bend actually makes you produce for its own homepage demo, and then rebuilt the same demo in a formal-verification language that's been around for decades, just to see what the gap looked like. Reading his numbers made me go back and look at my own checkout code, and I didn't like what I found.

This isn't really a post about Bend. It's about a specific failure mode that vibe-coding makes way too easy to fall into, on a language design project or on a Tuesday-afternoon Swift ticket: you can ship a working solution before you've done the five minutes of research that would have told you a much better one already exists.

Vibe-coding doesn't just risk bugs — it risks skipping the research step entirely, so you build a big, working, and completely obsolete solution to a problem the field solved years ago.

Bend 2's Blind Spot

Bend 2 is pitched as a language for humans and AI to split the work: you write "laws" describing what a program must never do, an LLM writes the implementation and a proof that it satisfies those laws, and the compiler checks the proof. For the flagship demo on its homepage — a tiny terminal game where the whole point is that you can never actually reach the win state — Powell went and counted the code required. The LAWS.bend file that states the two invariants ("never touch the flag," "never win") runs 58 lines. The PROOF.bend file the LLM has to write to convince the compiler those laws hold runs 442 lines.

Powell's actual point isn't that 442 lines is a lot of code, though it is. It's that Bend's entire design assumes proofs get built from first principles every single time, because nowhere in Bend's marketing copy or its codebase do the words "formal verification" show up. That's a field that's existed since before most of us were born, with tooling that already handles exactly this kind of invariant, and Bend seems to have been built without anyone on the project realizing it exists.

"far too easy to implement a design that's horribly broken or decades behind the current state of the art"— Liam Powell, on what vibe-coding makes possible

To make the point concrete, Powell vibe-coded the same demo in SPARK, a formally verified subset of Ada that's been used in avionics and rail signaling for years. He gave an LLM zero extra guidance beyond "recreate this in SPARK." The spec, implementation, and terminal driver combined come in under 90 lines, and running GNATprove against it returns a plain "Success: all checks proved (12 checks)." No 442-line proof, because SPARK's whole job is generating and checking that proof for you.

Why This Hits Close to Home in Swift

I don't build compilers for a living, so it's tempting to read Powell's post as a story about a niche academic language and move on. But the shape of the mistake is not niche at all. It's the exact same mistake I make every time I let an LLM generate validation logic without stopping to ask whether Swift already has a language feature built for this.

Swift's type system is, in a very real and boring sense, a lightweight formal verification tool. Optionals eliminate a whole category of null-pointer proofs other languages need at runtime. Exhaustive switch statements over enums with associated values let the compiler check, at build time, that you've handled every state a value can be in. None of this requires an LLM writing 442 lines of anything — the checking already happens for free, every time you hit Cmd+B.

The pattern here has a name in the functional programming world: "making illegal states unrepresentable." Instead of writing code that checks a state is valid after the fact, you design your types so the invalid state simply cannot be constructed in the first place.

When you ask an LLM to "add validation" to a struct full of optional fields, it will do exactly that — add validation. It will not, unprompted, suggest restructuring the data as an enum so the validation becomes unnecessary. That's the same gap Powell found in Bend: the tool happily builds you a bigger proof machine instead of pointing out you don't need one.

The Checkout Validator I Vibe-Coded

Here's what the LLM actually gave me when I asked it to make sure an order couldn't be confirmed without a valid address and a valid payment token. It's not bad code by the usual metrics — it compiles, it's readable, every branch has a test. That's exactly why I didn't question it at the time.

The Guard-Clause Version

The model represented checkout state as a struct with a bunch of optional fields, then layered guard clauses on top to enforce the ordering between them:

struct CheckoutState {
    var items: [CartItem] = []
    var address: Address?
    var paymentToken: PaymentToken?
    var isConfirmed: Bool = false
}

func confirmOrder(_ state: inout CheckoutState) throws {
    guard !state.items.isEmpty else {
        throw CheckoutError.emptyCart
    }
    guard state.address != nil else {
        throw CheckoutError.missingAddress
    }
    guard state.paymentToken != nil else {
        throw CheckoutError.missingPayment
    }
    state.isConfirmed = true
}

There are fifteen of these guard clauses spread across six functions in the real file, plus a test asserting each one throws under the right conditions. It looks thorough. But nothing here stops another part of the codebase from setting state.isConfirmed = true directly, and nothing stops confirmOrder from running twice back to back on the same state, since isConfirmed is just a mutable Bool anyone can flip. I only caught that second problem because a coworker triggered it by double-tapping the confirm button during a demo.

The Enum Version

Rewriting it as an enum removes the need for most of those guard clauses entirely, because the invalid states just don't exist as values you could construct in the first place:

enum CheckoutState {
    case cart(items: [CartItem])
    case addressed(items: [CartItem], address: Address)
    case paid(items: [CartItem], address: Address, payment: PaymentToken)
    case confirmed(order: Order)
}

extension CheckoutState {
    func addingAddress(_ address: Address) -> CheckoutState? {
        guard case .cart(let items) = self, !items.isEmpty else { return nil }
        return .addressed(items: items, address: address)
    }

    func authorizingPayment(_ token: PaymentToken) -> CheckoutState? {
        guard case .addressed(let items, let address) = self else { return nil }
        return .paid(items: items, address: address, payment: token)
    }

    func confirming() -> CheckoutState? {
        guard case .paid(let items, let address, let payment) = self else { return nil }
        return .confirmed(order: Order(items: items, address: address, payment: payment))
    }
}

There's no isConfirmed flag to accidentally flip. You can't build a .confirmed case without a payment token, because .paid is the only case that carries one, and you can't reach .paid without going through .addressed first. The double-confirm bug disappears too, since calling confirming() twice on the same immutable value just returns the same result — there's no shared mutable state left to race on. I cut around forty lines of guard clauses and a dozen tests that existed purely to check invariants the compiler now checks for me.

The Pattern Behind the Trap

What bugs me about my own checkout code isn't that it had a bug. Code has bugs; that's not news. What bugs me is that I had every tool I needed to avoid the whole category of bug, sitting in the standard library, and I never asked for it because the first answer I got looked complete. Tests passing gave me false confidence that the design itself was sound, when all they'd actually verified was that the guard clauses matched the guard clauses.

Powell's framing of the Bend situation applies almost word for word here: vibe-coding lets you build a substantial, functioning solution before you've learned enough about the problem space to recognize that a better solution already exists. Line counts make the gap obvious when you put the different approaches next to each other.

ApproachCode to state the ruleCode to enforce itWho checks it
Bend 2 demo58 lines (LAWS.bend)442 lines (PROOF.bend)Bend's compiler, from a proof built from scratch
SPARK rewrite of the same demo~20 lines of spec~70 lines of implementationGNATprove, using decades of existing proof automation
My checkout validator, v10 (implicit in guard clauses)~60 lines of guards + testsNobody, until a coworker found the race by hand
My checkout validator, v24 lines (the enum cases)~20 lines of transition functionsThe Swift compiler, at every build

The common thread isn't "AI writes bad code." Both versions of my validator compiled and passed their tests. The common thread is that an LLM will always answer the question you actually asked, and it will basically never volunteer that you're asking the wrong question. Bend's author asked "how do I get an AI to write and check a proof," and got exactly that, instead of "does a tool for checking proofs already exist."

The Five Minutes of Research I Skipped

None of this means throw out the AI assistant and go back to writing everything by hand. It means the research step has to happen before the generation step, not after, and it has to be a step you actually take rather than something you assume the model did for you. I've started doing a short pass before I let an LLM touch anything that looks like a rule or invariant, rather than after.

The check is short enough that skipping it was never really about saving time — it was about not having the habit yet:

  • Name the actual property you're trying to guarantee, out loud, before describing any code — "the order can't be confirmed without payment" is a different problem than "add validation to confirmOrder."
  • Ask whether the type system can make the bad state impossible to construct, before asking whether a function can check for it at runtime.
  • Search for the specific pattern name, not just the feature — "making illegal states unrepresentable" or "parse, don't validate" turn up prior art that "swift validation" never will.
  • If a whole field exists around this exact problem — formal verification, session types, whatever it is — spend ten minutes finding out what its standard toolchain already does before building your own version of it.
  • Only then ask the LLM to implement the approach you picked, instead of asking it to invent one from scratch.

It's a small habit, and it feels almost too obvious to write down. But "obvious in hindsight" is exactly the trap Powell is describing — Bend's author presumably would have said the same thing about formal verification if you'd asked them directly, and still built the whole language without checking.

Where Vibe-Coding Still Earns Its Keep

I don't want to overcorrect into treating every AI-generated function as suspect. Most of what I ship day to day is plumbing — a network layer, a view model, a settings screen — where the "state of the art" is well understood and an LLM reproducing it correctly is exactly what I want. The trap isn't specific to AI-assisted coding in general; it's specific to problems where a whole field of prior art exists and you don't know it yet.

The tell, in retrospect, was that I was writing something that felt like it should have a name. Anything involving "this can never happen," "these states must occur in order," or "this needs to be provably correct" is a signal worth pausing on, because those are exactly the phrases that map onto decades of existing computer science rather than a one-off feature request.

Tests passing is not the same signal as design being correct. My guard-clause validator had one hundred percent of its invariants covered by tests and still shipped a race condition, because the tests could only check the states I'd thought to write tests for.

If you're prototyping a throwaway script, or the problem really is novel enough that no prior art applies, generate away and don't feel bad about it. The five-minute check is for the code that's going to outlive the sprint it was written in.

Conclusion

I don't think Bend is a bad idea because its author didn't know formal verification existed — plenty of good software gets built by people filling gaps in their own knowledge as they go. What I think is worth sitting with is how far you can get before that gap becomes visible, when the tool doing the building never tells you it's there. My checkout validator worked, shipped, and passed review, and I still would have kept building on top of it if I hadn't happened to read a post about a niche proof language a few days later.

Next time I catch myself asking an LLM to "add validation" or "make sure this can't happen," I'm going to stop and ask what field owns that problem before I ask what code solves it. Most of the time the answer is going to be "just Swift's type system, five minutes ago" — and that's a much better place to start than a pile of guard clauses I'll be debugging in production later.

Sources: Liam Powell — Bend 2 and the Vibe-Coding Trap