Mostly whether the mechanism for passing data to and from the main program is sound; but also whether things like interrupt priority make sense and whether your re-trigger handling or re-entrancy are going to work properly (an interrupt happens while you're in the handler for the same interrupt). It might be sufficient simply to have a good set of primitives for this, rather than an actual proof.

Basically whether it's going to deadlock or miss interrupts. Deadlock is immediate disaster, but at least the JTAG will help you .. if the device hasn't self-destructed. Missing interrupts is worse because it's extremely hard to debug.

Forcing DMA to behave would also be great, although this isn't strictly a microcontroller issue. I've seen a few war stories where people are trying to debug memory corruption where the program is completely correct - but some other device has simply DMA'd over it. I think this was involved in https://googleprojectzero.blogspot.co.uk/2017/04/over-air-ex... too.