Run-time enforcement of contracts and functional "stress" tests are the cheapest and most efficient way I've found to write correct-enough microcontroller software. Static checks are good (and I wish C was better in this regard) but you can't check the state of the hardware without run-time checks.