I don't know much about formal verification, but I had expected that it considers the most basic behaviour of the most basic data types we have at the very leas

I don't know much about formal verification, but I had expected that it considers the most basic behaviour of the most basic data types we have at the very least. Integer overflow as one of wrap-around, saturation or invalid state (UB in the real world) is a bar so low that I do not know what formal verification that doesn't consider it would be useful for all.