SlateDB WAL protocol gets an open-source TLA+ spec

blaizedsouza · x · 2026-09-09

vanlightly released a TLA+ formal specification of the SlateDB WAL (write-ahead log) protocol, open-sourced under s3-wal-collection/slatedb on GitHub. It includes the main .tla file, config, and design notes; he plans to experiment with a CAS-write manifest variant next, purely for fun during an extended vacation.

Original post →

More from Research

Research channel →