These programs are executed in environments. Which are run on a hardware. Big part of which is hidden software.

And in general you can have 5 boxes verified and be surprised what comes out of them calling each other. Number of boxes is growing and possible interactions is exp. I don't think formal verification solves much.