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
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.
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