It doesn't sound like you necessarily disagree. Maybe we use different meanings of "worth the effort"? I meant it in terms of money that a company can save or

It doesn't sound like you necessarily disagree. Maybe we use different meanings of "worth the effort"? I meant it in terms of money that a company can save or make from deciding to expend that effort. You also have an additional cost in terms of "risk" that the effort does not yield desired results. So "they're delusional" would only be true if the people deciding this seriously overestimate the effort to verify something or seriously underestimate the benefits. Do you think that's true in general? Or even in the examples you cite? It seems like Apple and Google know what WUFFS is and what it can and cannot do, so they understand the effort. The maximum conceivable benefits in the cases you mention would be "no security vulnerabilities in said code". I'm not sure that is seen as a huge benefit by those in charge. Even rewriting that stuff in Rust (or even Swift) would significantly reduce the probability of weaknesses being exploited. Nobody seems to think that's worth the effort. The "marketing pitch" of WUFFS is: "as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used". So, presumably, Rust and Go are equally and sufficiently safe, "roughly speaking"? And Rust is neither fast enough nor easy enough to integrate with C code (despite being good enough for drives in the Linux kernel)? This sales pitch makes it clear that the people behind WUFFS are keenly aware that "safety" alone doesn't sell. This problem is generally more endemic of software security in general. The cost of security issues is usually not borne by the people who decide how much to invest into security. Also, security does not contribute to profits, it is only a cost center. By contrast, when you have really important code and you bear the cost of mistakes and outages directly, formal methods are being used where it can be done straightforwardly. AWS and some cryptocurrencies (for whom security and correctness is an above-average part of their sales pitch) have prominent uses.