Ah sorry our contractor did all that highly illegal stuff. Too bad we can't pierce the corporate veil anymore... shucks.

That would be like saying that you can verify the software that CERN uses to measure the Higgs Boson because we verified general relativity.

Basically the modern web uses orchestration, for pretty much everything. Usually Kubernetes is doing that. Theoretically protocols like RAFT are formally verifiable, but their implementations in orchestration tools like etcd have not been, and I would go so far as to say that that is an impossible task. Therefore, the entire exercise is kind of silly.

You can't formally verify anything that uses consensus, which is the backbone of the entire web. It's a complete non-starter.

I laughed out loud when he said Cloudflare should have formally verified its systems.