I've been doing a lot of low-ish level programming with video hardware on an embedded system. I mmap a buffer, which gives direct access to the hardware. I trust that the driver reports the correct size of the buffer, and that the hardware puts the bits in that buffer in the way its spec promises. How the fuck do you formally prove any of that? I can prove that my software, for example, moves bits from offset x to offset y in the buffer correctly, but how do I prove that it makes sense to move those bits in that way? Or that I have interpreted the driver's documentation correctly, or the v4l2 API correctly, or that the hardware or driver does what it says it does? Keep in mind that this is C++ of course, so there's no mathematically rigorous type system; I just have a uint8_t pointer to a place in memory.

I can potentially lay down a bunch of assumptions, and prove that, given those assumptions, my program acts correctly. However, most of the bugs arise from incorrect assumptions.

One concrete example: When feeding pixel data to the onboard hardware h264 encoder's driver, after having set a resolution of 1920x1080, the resulting h264-encoded frame will be displayed in a h264 decoder with a resolution of 1920x1080. This turned out to be wrong, because the hardware can only deal with blocks of size 16x16, so the width and height must be a multiple of 16, and the driver isn't smart enough to add the necessary metadata to make a decoder crop it, so there's 8 green (because YCbCr) pixels on the bottom of the video. The solution to this is to manually splice the h264 bitstream, to insert my own metadata which has the correct cropping. How the fuck do you formally prove any of that?