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