The "Just Use Postgres" Trap
How The Heck Does Shazam Work?
Verifying distributed systems with Isabelle/HOL
Why not use Lean?
Turing Award Winner: Postgres, Disagreeing with Google, Future Problems | Mike Stonebraker
The Log is the Database
Why Queues Don’t Fix Overload (And What To Do Instead)
The Tokio/Rayon Trap and Why Async/Await Fails Concurrency
The Future of Everything is Lies, I Guess: Bullshit About Bullshit Machines
Scotty, I need warp speed in three minutes
Event Loops Internals And How Redis Handles Multiple Connects on a Single Thread | Redis Internals
Good and bad sharding keys (for databases)
Our own worst best customer
What are skiplists good for?
Things you didn't know about indexes
Antithesis is not enough
Raft is so fetch: The Raft Consensus Algorithm explained through "Mean Girls"
Absurd Workflows: Durable Execution With Just Postgres
Absurd In Production
Introduction to ClickHouse's Data Storage Architecture (George Larionov)
lean implicits
Controlling Nondeterminism in Model-Based Tests with Prophecy Variables
A Dumb Introduction to z3
Lean proved this program was correct; then I found a bug.
Workload isolation using shuffle-sharding
reublog: Fast CASPaxos
MODERN-DAY ORACLES or BULLSHIT MACHINES?
The Future of Everything is Lies, I Guess
reublog: CASPaxos
Giving LLMs a Formal Reasoning Engine for Code Analysis
Formal Verification in Any Language for Everybody
The secret lives of data
Generating Unique IDs with Raft Consensus
You Can’t Sacrifice Partition Tolerance
Notes on Distributed Systems for Young Bloods
Your RAM Has a 60 Year Old Design Flaw. I Bypassed It.
Sam Altman May Control Our Future—Can He Be Trusted?
Row Level Security: Defense in Depth
search engines at scale from a beginners pov
The Iran economic shock is coming. How to protect yourself
The Moment that Reset Robotics
Why Lean?
A pretty-printer for TLA+
Quantization from the ground up
how to make programming terrible for everyone
frameworks for understanding databases
the broken economics of databases
Video Conferencing with Durable Streams
The Cost of Concurrency Coordination with Jon Gjengset
Correctness Anomalies Under Serializable Isolation
Strict-serializability, but at what cost, for what purpose?
TLA+ for Single-Page Web Applications
To be a better programmer, write little proofs in your head
Hypothesis, Antithesis, synthesis
Crust of Rust: Send, Sync, and their implementors
Specification Refinement
TLA+ mental models
Notes on Paxos
A hands-on Introduction to Program Verification in Lean 4
Every layer of review makes you 10x slower
A Trillion Transactions
Qdrant: Open Source Vector Search Engine and Vector Database (Andrey Vasnetsov)
FPGAs Aren’t Processors (Unless You Want Them to Be) || FPGA Deep Dive and Use
This Speaker Has No Moving Parts
Who Watches the Provers?
Modeling Token Buckets in PlusCal and TLA+
lean4.dev: Theorem proving
From Zero to QED
Every minute you aren't running 69 agents, you are falling behind
TLA+ as a Design Accelerator: Lessons from the Industry
The Alien Signal That Looked Intelligent
Prediction: AI will make formal verification go mainstream
The Lean FRO Year 3 Roadmap
A Lean Syntax Primer
Beyond Booleans
The Math Is Haunted
Functional Programming in Lean
Specifying and simulating two-phase commit in Lean4
Why Lean 4 replaced OCaml as my Primary Language
Gabriella Gonzalez on "Monad transformers are good, actually" @ZuriHac2023
Running an Engineering Papers Reading Guild at Zalando
Building a Database on S3
The Question Nobody Ever Explains: Where Does the Kernel End
Multi-Modal Program Verification in Velvet
When AI Writes the World’s Software, Who Verifies It?
How is hardware reshaping LLM design?
Why study statistics? | Stats From Scratch, Chapter 1
The inner workings of TCP zero-copy
Search Engines from Beginners POV
The Fascinating Neuroscience of Hitting a Baseball
Why THIS Curve? The Deep Reason Behind Sigmoid and Softmax
From Noise to Image
one up on LRU
Verification For Dummies: SMT and Induction by OCamlPro
Evolution in Higher Dimensions
Resolution Proofs in Logic
Verifying Safety of Rust's CStr
AWS re:Inforce 2024 - Verifying code using automated reasoning (APS402)
Making Even Safe Rust a Little Safer: Model Checking Safe and Unsafe Code
Can you reverse engineer our neural network?
Satisfiability Modulo Theories: A Beginner’s Tutorial
Attacking a random number generator
Let's Prove Leftpad
Detecting server failure in a distributed system
Formal methods for the unsafe side of the Force
Some Silly Z3 Scripts I Wrote
Turing Award Winner On Thinking Clearly, Paxos vs Raft, Working With Dijkstra | Leslie Lamport
The Night Watch
Karpathy: microgpt
Databricks: Data Lakehouse
Two Bits Are Better Than One: making bloom filters 2x more accurate
Blast Through the Mountain - Practicing Fearless Engineering
Why JSON isn't a Problem for Databases Anymore
Specifiability is the Leverage
Browse code by meaning
Virtual Database Sharding: A Flexible Approach
NEVER run Postgres without a replica (failovers + high-availability)
M.A.(KEN) CLEMENTS TERENCE TAO
Practical Uses of Synchronized Clocks in Distributed Systems
how do I stop participating?
Monitoring Data-Dependent Temporal Patterns
Re-Designing Data-Intensive Applications: The Shift to Cloud-Native Storage
Common prefix skipping, adaptive sort
ignore the rumors, computer science is still cool
Data Centers Behaving Like Sonic Weapons
What's The Difference Between Matrices And Tensors?
Simulating Atoms in C++
The Incredible Evolution of Computers
Markov Chains Explained Visually
Monte Carlo Simulation Explained Visually
My colleague Julius
How CPUs Run Functions
The Data Structure that's allowed to Be WRONG
Russ Cox on CLs containing AI generated content
How did bacterial flagella evolve? 01: Here's what we know
How to build a distributed queue in a single JSON file on object storage
ARC: A SELF-TUNING, LOW OVERHEAD REPLACEMENT CACHE
99.9% is easy, 100% is hard
A Rock Is Trapped Light
Kubernetes Explained: 3 Core Features You Must Know
Skip Lists - a perfect structure for LSM databases!
The Insecure Evangelism of LLM Maximalists
Building a Correct-by-Design Lakehouse
False Sharing: Why your multi-threaded code is mysteriously so slow!
How to optimize (almost) anything
The Great Golden Age of Antibiotics
Why are diffusion LLMs so fast?
The MOST Underrated WW2 Hero You've Never Heard Of
The perfect structure for merging data quickly (the priority queue)
FAST database writes with LSM (Log-Structured Merge trees)
Data Structures - Bloom Filters, Count-Min Sketch, HyperLogLog
Bryan Cantrill: Andreessen’s Folly - The False Dichotomy of Software and Hardware
OSTEP Chapters 6,7
Git Sync: Observability as code built for scale | Demo | Grafana Labs
Network Basics - Transport Layer and User Datagram Protocol Explained - Computerphile
The Birth of SQL & the Relational Database
Kubernetes Networking: NodePort, LoadBalancer, Ingress, or Gateway API?
Three Lenses on Coordination
Your Idempotent Code Is Lying To You
Approximating Data with the Count-Min Data Structure
Towards Automated Cross-domain Exploratory Data Analysis through Large Language Models
Apriori data mining algorithm in plain English
Using COW in Unix processes and database B-trees (Copy-on-write)
Hypergrowth isn't always easy
OSTEP Chapters 4,5
Uncover slow database queries with p50, p95, and p99
The Japanese AI Boom Needs A Little More Ambition
Write-Ahead Logs. The secret to fast database queries.
Can humans make AI any better?
Logical Time and Deterministic Execution
Formal Methods Beyond Correctness: Isolation & Permissiveness of Distributed Transactions in MongoDB
The Importance of Diversity
sorted string tables (SST) from first principles
Why Are Elites Degenerate Hypocrites
The Refragmentation
Monster Scale Summit 2025 | Time Travelling at Scale by Richard Hart
Experiences with Semi-Formal Proofs with Justin Moore
Our own worst best customer
On presenting well
How to present your work
How to speak (by Patrick Winston)
Clear communication
What Does a Database for SSDs Look Like?
Killing transactions in databases (deadlock detection and resolution)
A Critique of ANSI SQL Isolation Levels
Caching algorithms (LIFO vs LRU vs CLOCK)
How OpenAI Handles 800 Million ChatGPT Users on a Single PostgreSQL Primary
Jepsen: Linearizability
Jepsen: Sequential Consistency
Jepsen: Causal Consistency
Jepsen: PRAM
Jepsen: Read Your Writes
Jepsen: Monotonic Writes
Jepsen: Monotonic Reads
Jepsen: Writes Follow Reads
Jepsen: Strong Serializability
Jepsen: Serializability
Jepsen: Repeatable Read
Jepsen: Cursor Stability
Jepsen: Monotonic Atomic View
Jepsen: Read Committed
Jepsen: Read Uncommitted
Jepsen: A5B (Write Skew)
Jepsen: Snapshot Isolation
Snapshot Isolation vs Serializability
Assembly: SIMD Optimization in Go
using RAM to make databases FAST (the buffer pool)
ParadeDB – Postgres for Search and Analytics (Philippe Noël)
Lock-free linked lists using compare-and-swap
wal3: A Write-Ahead Log for Chroma, Built on Object Storage
Availability Models
Jepsen: Sequential Consistency
Silicon Chips Are Built One Atomic Layer at a Time
How AI works in Super Simple Terms!!!
The Remarkable Computers Built Not to Fail
How HTTP/2 frees connections
How similar are Italian and Latin?
Reliable system call interception.
Databases in 2025: A Year in Review
Delta Electronics: Taiwan's Power Supply Giant
Making Sense of RF Sensing
Faixas de operação da comunicação LoRaWAN
Gadgets For People Who Don't Trust The Government
Proving liveness with TLA
How MySQL's Midpoint Insertion Strategy Prevents Cache Pollution
TLA+: Proving Distributed Systems Correct
The genius logic of the NATO phonetic alphabet