Comment by DoctorOetker

It's a bit harsh.

More to the point, and no longer specific to Tailscale: while plenty of companies do have rough "proof sketches" demonstrating the security of a setup under certain assumptions (hardness assumptions of the cryptosystem, threat model assumptions, ...) nobody is doing it formally to check with a general statement verifier. A lot of the advice and recommendations offered on the featured article may or may not be useful strategies for which properties are provable, and all the "security best practices" could be viewed as lego block lemmas from which system architects design a more reliable whole.

This means the community is doing redundant work. If people actually described and refined reusable assumptions say for the metamath verifier, people could download standard machine readable formalized threat models, share proofs that demonstrate the security (conditional on this or that assumption), or proofs that demonstrate the insecurity for specific ways an assumption might be broken, etc.

Whenever an incident happens we can visualize exactly the set of assumptions among which at least 1 must have been violated, so different groups suspect this or that assumption to be violated and thus collectively define variations of security proofs with different assumptions. This diversity allows us to zoom in on the faulty assumption over time as incidents are accumulated.