Proving formal properties requires formal specifications. “absence of undefined behavior”, the property that Astrée more or less verifies, is one more or less

Proving formal properties requires formal specifications. “absence of undefined behavior”, the property that Astrée more or less verifies, is one more or less formal piece of specification that authors of formal tools for C get for free. In reality, they get to formalize it themselves, because the C standards are written in English and contain much ambiguity, and their interpretation evolves over time. Two decades ago, signed arithmetic overflow was described as undefined because everyone “knew” that the authors of the standard wanted to accommodate 1's complement and sign-magnitude, and therefore everyone assumed that if you knew your architecture was 2's complement, you could expect 2's complement behavior. The issue being discussed here is not one of having undefined behavior, though. OpenSSL is being blamed with not satisfying a property that it wasn't even documented as having, much less formally specified. Your comparison to aeronautics code is also omitting the price of developing to aeronautics safety standards. For one thing, in aeronautics it is decided in advance what the software will do, and the software is implemented to have only these features. This is not how OpenSSL got to where it is today! Astrée is only used to verify one aspect of the safety of part of the code in the aircraft, so it is really not a good example to use here. If you wanted to make a strong case, you could use miTLS: http://www.mitls.org/wsgi/home http://www.mitls.org/wsgi/home And since miTLS already exists, you can ask the question of why it is not used in place of OpenSSL. Part of the answer is that it is F# and is only likely to interface easily with .NET projects. My employer sells formal verification reports for open-source software. One piece of software we have formally verified with a tool comparable to Astrée is PolarSSL: http://trust-in-soft.com/polarssl-verification-kit/ http://trust-in-soft.com/polarssl-verification-kit/ This verification did not check whether the algebraic properties of any key are correctly validated in any of the cases where this would be relevant, because that's outside the perimeter. The verification sets out to verify that the code doesn't have any of the problems of the sort that Astrée would find (and a bit more), and it does exactly that.