tis-interpreter VS coreHTTP

What makes you think they don't understand it? They acknowledge that it is UB. I read them as realistic, since they know that people rely on C compilers work in a certain way. They even wrote an interpreter that detects UB: https://github.com/TrustInSoft/tis-interpreter

I understand why people like the compiler being able to leverage UB. I suspect this philosophy actually makes Trust-In-Soft more money: You could argue that if there was no UB, there would be no need for the tis-interpreter.

So isn't it in fact quite self-less that they encourage the world to optimize a bit less (spending more money on 'compute'), while standing to profit from the unintended behaviour they'd otherwise be contracted to help debug?

One of the examples they gave was an HTTP client, which would be a surprisingly non-toy example, so I looked at what they actually did in the code (https://github.com/FreeRTOS/coreHTTP/tree/main/test/cbmc).

Not that I'm an expert in processing what exactly is being tested, but it basically looks only able to prove that an individual function doesn't overrun buffers. If you tell it to assume that overflows can't happen (!). So I'm not impressed.