Isn't this what matlab and other tools like it try to deliver to? Most programs I've seen in the industry use matlab and simulink for formal verification (of c

Isn't this what matlab and other tools like it try to deliver to? Most programs I've seen in the industry use matlab and simulink for formal verification (of course, still ignoring the hardware design part) and I'm asking myself how many dependencies the verification should have. I mean, even a simple Hello World program could escalate really quickly once you have to deal with TTY quirks or say, %X as a printf parameter. The issue I see with matlab's approach is that it has a huge set of assumptions in its own compiler chain, which I guess is the core problem of all ABI compatible outputs.