You can write a formally verified, simple Hello World program and prove that it adheres to both your design and implementation specifications. You can this all

You can write a formally verified, simple Hello World program and prove that it adheres to both your design and implementation specifications. You can this all the way down to how the specific processor will run the resulting machine code. The catch is that this is difficult and the time and cost both scale non-linearly with the complexity of the software. But if you can do it for dead-simple programs running on hardware you understand very well, you can do it for complex software as well. Just be prepared to pay millions of dollars for it.