TLC Caught Our First Consensus Bug: Why We Do Formal Verification
TLC model checking found a subtle Agreement violation in our VSR specification—before we implemented it. Here's the bug, the fix, and why formal verification is worth the investment.
Deep dives into Kimberlite's architecture, design decisions, and progress.
TLC model checking found a subtle Agreement violation in our VSR specification—before we implemented it. Here's the bug, the fix, and why formal verification is worth the investment.
We fixed 18 critical bugs, promoted 38 production assertions, and fundamentally changed how we test Byzantine fault tolerance. Here's what we learned from transforming VSR from working code to production-grade consensus.
A subtle bug in our key encoding broke index ordering. Here's how we fixed it with null-terminated strings and escape sequences—and saved 3 bytes per key in the process.
Our deterministic simulation tester uncovered five subtle bugs in linearizability checking. Here's how we hunted them down and what we learned about testing distributed systems.
A compliance-first, verifiable database for regulated industries. Built on a single principle: all data is an immutable, ordered log.
The story behind Kimberlite starts with a clinic management system, a lot of compliance headaches, and a search for the database that didn't exist.
Diamonds form under immense pressure over geological time. This is about writing code with the same property—forged under pressure, built to endure.