A linearizable metadata log for Materialize, built on PostgreSQL READ COMMITTED isolation, with 3x write throughput and a Lean 4 proof.