Building a Reliable Database Protocol with AI, Formal Methods, and a Simulation Framework

Building a critical distributed protocol in 2026 means treating correctness as a continuous engineering practice, not a final verification step.

This talk presents a workflow that combines executable state-machine designs and formal methods with AI-assisted development, observability, and Antithesis testing.

The goal is to move from a protocol model to evidence from real-system executions: expose meaningful events, generate and investigate failure scenarios, and use code together with observability data to validate distributed properties that code alone cannot reveal.

The result is a faster, more practical path to designing, testing, and evolving systems such as databases with confidence.