Your Secret Weapon for Catching the Bugs You Never Saw Coming


PETER MBANUGO

Programmer & Consultant

Hey 👋

Have you ever fixed a bug, or shipped the patch only to have it haunt you in production?

That feeling exists because tests only catch scenarios you think of.

There's another way to approach correctness: specify what the system should do, not how to do it — and let a computer program verify that all possible executions satisfy your requirement.

That’s the idea behind formal verification, and I’ve started a new series where I’m building a new tool to do exactly that.

What I’m building (and documenting step by step):

  • A TLA-inspired model checker
  • Implemented in Odin (a systems programming language similar to Go)
  • With a compiler, VM, and state-space exploration engine
  • No academic hand-waving, just pragmatic systems thinking

In the series, you’ll see:

🧠 The mindset shift from “write tests” → “define invariants”

🛠️ How the tool explore all possible states & timelines, not just happy paths

🐛 Real mistakes I made — and what they taught me

This isn’t about replacing tests. It’s about catching the bugs tests can’t — race conditions, invalid states, edge cases that only appear under just-right timing.

Quick question (hit reply): What’s a bug that once made you lose sleep?

PS: If you know a developer who hates flaky tests or works on complex systems, please forward this — it might permanently change how they think about correctness.

— Peter

600 1st Ave, Ste 330 PMB 92768, Seattle, WA 98104-2246
​Unsubscribe · Preferences​

Hi, I’m a Software Consultant and Technical Trainer

Subscribe to my newsletter if you want to see me write about different stack of software engineering and how to use them to build products. I write about high-performance Node.js/Bun applications, React and Astro, and my journey programming with Zig.

Read more from Hi, I’m a Software Consultant and Technical Trainer

PETER MBANUGO Programmer & Consultant Hey Reader, it's been a while. I've been busy working on Tina, the high-performance concurrency framework I've written about a few times. It's a huge rewrite (from scratch) because I've learned a few new things and I'm expanding the framework from the initial idea of "just an eventloop library", to having a few more components for building robust applications. There's still a lot to do, but I hope to share some update next month. Stay tuned! New Blog Post...

PETER MBANUGO Programmer & Consultant Hi everyone, If you’ve ever tried to build a high-performance backend, you know the pain of the "Concurrency Trilemma." You usually have to pick your poison: Callback, Promise, or Async Hell (Rust/JS) where coloured functions fragment your codebase. Mutex Hell (Go/C++) where shared-state leads to subtle race conditions and deadlocks. The GC Ceiling (Erlang/Elixir) where you get a brilliant mental model, but pay for it in garbage collection pauses and VM...

Peter Mbanugo pmbanugo.me Hello Reader, I've published a new blog post and it is about QUEUES. You have used a queue today. In fact, you have probably used one dozens of times before lunch. Whether it is Spotify loading songs in order, your server processing background jobs, or just waiting at the supermarket checkout, the FIFO (First-In, First-Out) queue is the invisible engine that keeps modern systems running smoothly. You have used Kafka, RabbitMQ, and likely a Queue data types in your...