[fwip]

A browser is possibly the most difficult application to formally specify. 99.somemorenines% of software has less complex specifications.

The formal specification for something like Redis is likely much more akin to your car bridge spec. And to continue your analogy, I imagine the specifications for big bridges (Golden Gate, etc) are much more thorough than the ones you built.

[quatrefoil]

A browser is one of the most consequential attack surfaces in the lives of billions of people. Redis isn't. Having proofs where said proofs don't matter much in the first place is not a particularly good use of our time. And FWIW, the correctness specs for Redis would be pretty intractable too.