Honestly? I don't know for sure.

On one hand, my understanding is that they used TLA+ to validate the model[0]. One would assume that if they went to that trouble there is at least a specification for how it should work.

OTOH, Specifications can be flawed. This security issue appears unrelated to the design of Cosmos DB itself tho.

[0] - https://en.wikipedia.org/wiki/TLA%2B#Industry_use

For formal verification to catch the bug, the bug would have to be at the design level and the model would have to have enough detail to include the design bug.

TLA+ is used to design the database itself, including the storage layer, distributed operations, and consensus/consistency models.

This bug is a security issues in an entirely separate component. No formal logic is going to warn you about exposed read/write keys.

In principle it sounds good, but from what I've heard it is over-priced and far too slow compared to typical IaaS-hosted solutions.

Notably, some of the customers mentioned in the security researcher's blog are the type that have exploding wallets.

As in: "My wallet is bursting open because there's too much money in it! Mr Cloud Sales Guy, can you help me with this problem?"