Vibe-coding bug-free apps (expect bugs)

Issue #523.September 23, 2026.2 Minute read.
Bytes

Today’s issue: A slop-cannon comment battle, Vinod Khosla’s real motivation behind fixing the tax code and how to help systems engineers emotionally regulate.

Welcome to #523.


Eyeballs logo

The Main Thing

A man wearing a suit covered in Mountain Dew logos

Formally verifying my vibe-coded app

Vibe-coding bug-free apps (expect bugs)

Nothing prepares you for when your co-worker (yes the one with blue hair and snakebite lip rings) sits down next to you at lunch and starts telling you about “type theory”. And as much as I tried to forget, I got to relive that moment when Victor Taelin released a new language called Bend that uses type theory and formal verification to allow you to “enjoy bug-free, fast, vibe-coded apps”.

If you haven’t had the pleasure of getting a type theory lecture before, I’ll spare you, but the main thing you need to know is that you will hear the word “verify” a LOT. There are several formal verification languages like Lean and Rocq (formerly Coq) but they require a PhD in math and are really slow, taking minutes to check a full codebase.

Bend, in contrast, has a Python-esque syntax, a fast compiler, and is designed to do work in parallel. The big idea is that instead of you, a normie, trying to write proofs, your agent does it for you.

Here’s how it works:

  • Laws: Write the application function, then state a rule it must obey. For example, authorize must deny access between different tenants, regardless of permissions.

    def authorize(same_tenant: Bool, has_permission: Bool) -> Bool:
      match same_tenant:
        case True{}:
          has_permission
        case False{}:
          False{}
    
    law deny_other_tenants:
      for has_permission: Bool
      {authorize(False{}, has_permission) == False{} : Bool}
    
  • Proofs: Show why the rule holds for every value of has_permission. {==} works because the False{} branch of authorize always returns False{}.

    def deny_other_tenants(has_permission):
      {==}
    
  • Compiler: Checks the proof alongside the code. If a change makes the law unprovable, the check fails, letting your agent know that it needs to keep vibing.

Bottom line: Bend says “to expect bugs” which is uh… ironic given that it’s the solution for vibe coding related bugs. But bugs or not, it’s looking like I’m going to have to mute the word “verifiable” for the foreseeable future.


Oracle Developers logo

Our Friends
(With Benefits)

A man wedged between canyon walls looks upward

When you've severely underestimated what it takes for your agent harness to survive prod

Building an agent harness that survives production

“Agent harness” is an S-tier buzzword these days, but it’s just the configured layer around an LLM that decides what it sees, what it can do, where those actions land, and what counts as proof that the work actually got done.

Lots of teams are building their own custom harnesses, but getting them to work is notoriously painful. That’s why Casius Lee wrote this technical breakdown on the Oracle Developers Blog about Building your own harness that can actually survive prod.

It covers:

  • The 6 harness parts and the specific failure each one absorbs

  • Why prompt-level injection defenses fall apart under adaptive attacks

  • A 3-question audit for grading your harness

Read the blog post to become your team’s harness expert.


Cool Bits logo

Cool Bits

  1. TJ Zhang wrote a blog post teaching systems engineers frontend web development. Using Dune references to help them emotionally regulate after seeing React for the first time was probably a good call.

  2. Angelique Nehmzow and Emma Guo did a deep dive into how Notion handles concurrent editing with CRDTs.

  3. Sentry Logs, Beyond the Basics is a free workshop on Oct 1st that’ll show you how to use logs alongside traces and errors to get to a root cause faster and how to log across service boundaries. [sponsored]

  4. Joe Bell published version 1.0.0-beta.12 of cva, a tiny library for building type-safe, variant-driven class names with Tailwind.

  5. Sunil wrote about “the senior engineer death spiral”, or, as I like to call it, how to speed run getting fired.

  6. Alec Larson made a comparison table showing the differences between Octane and Solid 2 and which one wins. Nothing like a TMBB to get framework authors to load up their slop cannons to do battle in the comments.

  7. Only idiots write manual tests – modern engineering teams like Notion, Dropbox and LaunchDarkly use Meticulous to maintain e2e UI tests that cover every edge case of your web app. [sponsored]

  8. Claude, SpaceXAI, and OpenAI all released updates to their models. Does this mean we’re slowing down or accelerating?

  9. As of Chrome 154, iframes can now automatically resize to fit the content 🙏.

  10. Vinod Khosla wrote about how we need to change the tax code in the age of AI. The people still need money to buy Seahawks tickets.