I've always wondered how to use formal verification to prove software on 8 bit microcontrollers. There are so many peripherals like PWM/timers/counters, ADC, UART, and complicated configurations like clock prescalers, self-programming, and interrupts.
My most amusing observation of how much this can matter is the obvious obvious pitch/tone change in rail road alerts (at-grade rail crossing signals) on the Metra rail lines around Chicago in the winter. There is a noticeable difference even between 30F and 10F. IIRC correctly (it's been a year since I've been riding the train in the winter), the "beat" of the signal rapidly increases at lower temperatures and the pitch also seems to increase.
Same way it was done long ago: formal specifications with abstract and/or concrete state machines. Each has pre- & post-conditions plus invariants on its behavior. The implementation is simple. Static in terms of memory & such where possible. The resulting FSM's can be analyzed for about all behaviors, including timing. Such a subset is easier to statically analyze for common errors as well. SPARK or Astree can straight-up prove absence of common errors for subsets like that.
I posted a story recently on ASM's that had a simple introduction plus showed some of the temporal logics and such common with them:
Depending on your application domain, but if the software has timers and clocks I bet what I'm going to say applies, the good strategy is to use domain specific languages which offer strong guarantee on the produced code. Here I'm thinking specifically of synchronous dataflow languages. Those are formally defined and are designed for critical real-time system. They come with formal verification tools (often, model checkers) adapted to their semantics.
