Skip to content

Verification

A tested foundation

fdyno's correctness argument is short, and most of it is not about fdyno. The server is a thin, stateless translator: it maps the DynamoDB wire protocol onto FoundationDB transactions and holds no durable state of its own. Isolation, durability, atomic commit, and crash recovery are not properties fdyno implements; they are properties it inherits. So the interesting question is why FoundationDB's guarantees can be trusted, and the answer is an unusually rigorous methodology: deterministic simulation.