CLawZ enables the automatic independent verification of C source code generated from Simulink models.  Should the autocoder have made a mistake, it will show where in the code the issues lies and relate it to the original design in Simulink.

CLawZ: Automating source code verification