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://gith

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 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 integer overflows can't happen (!). So I'm not impressed.