Anecdote – Erlang designer Armstrong does contract work for formal verification with high-assurance applications. A widget-maker for a large European car manufacturer wanted to ensure their widget was fully compliant with all of the specifications as issued by the overseeing administrative authority (ISO, ANSI, whatever). He and his team of engineers sat down and took 1k +/- .2k pages of written specifications, translated them into invariant properties, and let 'er rip. Of the ~foo bugs they found, ~40% of the bugs were internally inconsistent bugs within the specification. [An average car of model year 2016 has somewhere between 500-800 MCUs within them. Scary prospect…] So, lets say LDAP's RFC has 3 'bugs' in them (a proposition: p in section one, then a proposition: ~p in section 3). Microsoft wants to implement Active Directory to have LDAP compliance to work with Kerberos, Apple devices, etc etc. By definition, this implementation will be buggy. These bugs are of a class which have no fix!

... if you want to read some formal proofs from the software and mathematics worlds, see https://www.isa-afp.org/