[bassp]

Minimally, the two examples I cited: Shardstore and Shuttle. The former is a (lightweight) formally verified key value store used by S3, and the latter is a model checker for concurrent rust code.

Amazon has an entire automated reasoning group (researchers who mostly work on formal methods) working specifically on S3.

As far as I’m aware, nobody at cloudflare is doing similar work for R2. If they are, they’re certainly not publishing!

Money might not be the bottleneck for cloudflare though, you’re totally right

[zild3d]

S3 has touted 11 9's for many years, so before shardstore definitely.

The 11 9's is for durability, which is really more about the redundancy setup, erasure coding, etc. (https://cloud.google.com/blog/products/storage-data-transfer...)

fwiw availability is 4 9's (https://aws.amazon.com/s3/storage-classes/)

[bassp]

That’s a good point!

I think I overstated the case a little, I definitely don’t think automated reasoning is some “secret reliability sauce” that nobody else can replicate; it does give me more confidence that Amazon takes reliability very seriously, and is less likely to ship a terrible bug that messes up my data.