We have plenty of functions that convert one byte array to another byte array. Both arrays have specified bounds. The functions are total (an error return indicates if the input or output arrays are incomplete). Most of them do not even have state that is preserved between calls. Complete source code is available in the same build for all the functions they call.

In theory, this should be very straightforward to prove correct with many of the current tools. In practice, no one has shown us how to do it. We could even rewrite the code from a macro/#include maze to proper function calls if that's a prerequisite for analysis. At this point, I would even take a one-off analysis.