Large publicly traded tech companies seem to no longer consider their customers – that is, people and organizations who actually buy their products or pay for access to their services – their core focus. The focus has instead turned towards the stock price.

Their real clients, the entities they really care about, are the stockholders. Reasons are many, perhaps one of them being that people making decisions tend to own stock options or have bonuses tied to stock performance of the companies they run.

This means that for a large, established tech company the product or service it offers does not matter all that much anymore. It needs to be just barely good enough to keep people using it. The easiest way to do this is some form of a monopoly.

Monopoly is the business model of Silicon Valley, and they are not even shy about that.

Cloud databases face a fundamental challenge: how to remain available and durable under node failures? Modern cloud databases approach this by separating two concerns that used to be tightly coupled: compute and storage. The database engine becomes stateless, while the write-ahead log gets replicated across multiple nodes to guarantee durability. If a database server dies, another one can pick up exactly where it left off by reading from the replicated log.

Distributed log services are thus at the heart of cloud databases. In this blog post, we will explain some drawbacks of the predominant design for distributed logs to motivate a new elegant design. We will also explain why it is necessary to verify this design with formal methods.