You can and should check your specs like they're code. For instance, you can write the spec in TLA+, which lets you specify temporal properties (e.g. "can the s

You can and should check your specs like they're code. For instance, you can write the spec in TLA+, which lets you specify temporal properties (e.g. "can the stall recovery procedure take an unbounded amount of time?") and liveness properties (e.g. "can any non-majority of disagreeing sensors cause the wrong trim actuations?") To test your invariants, you should sabotage the spec and check that invariants break. Once your spec passes model checking (or perhaps theorem proving with TLAPS), you can codify it in e.g. ADA-SPARK contracts. Once you have that, you've validated your spec, your contracts and your code. Bugs can only occur in your invariants and the seams of your subsystem. This level of rigor should be standard by now for safety-critical systems.