I don't think many open source projects do, no. Most of them aren't extremely quality-focused, and don't spend the money to develop or purchase some of the static analysis and formal verification tools that help a code base reach the level of quality I'm referring to.

But if I tried hard enough, I'm sure I could find a few that have been run through some sort of formal verification tool.

Whether I could or not doesn't change my assertion at all though.

I cannot see the language being at fault in cases such as the ones pointed out by the article:

> SQLite’s vdbe struct has a member called aMem that uses 1-based array indexing. To avoid wasting an element, this array is initialized like this: p->aMem = allocSpace(...); p->aMem--;

In its deep history, the C language was defined by what the implementations did. Only later was it standardized, with an attempt to permit existing implementations be viewed as conforming or easily updated to be. Even decades later, though, the culture of developers tends to the view that something which has always worked in every important implementation should be allowed and continue to work in new implementations. This is such an example. Only a new generation of compiler writers are challenging this, trying to shift to a language-lawyer interpretation of the standards.

  > the culture of developers tends to the view that something which has
  > always worked in every important implementation should be allowed and
  > continue to work in new implementations

Yes, and X3J11 stated as its first guiding principle,

  > Existing code is important, existing implementations are not.

But then they committed the original sin against “simple C” by inventing ‘volatile’, breaking systems code written when p[0]=x was expected to write to location p. Unlike ‘const’, with which the programmer grants additional license to the compiler, C89 granted the non-‘volatile’ license to the compiler by default. In retrospect, I think C would have been better off retaining do-what-I-wrote as the default, and requiring the programmer to grant the compiler license to do otherwise. C already had the ‘register’ keyword to indicate that a variable should be compiled for speed and need not be literally preserved according to a naïve reading of the code.