How do I ensure my product is correct the first time? [closed]

Question

Closed. This question needs to be more focused. It is not currently accepting answers.

---

Want to improve this question? Update the question so it focuses on one problem only by editing this post.

Closed 1 year ago.

Improve this question

I am working on a product that will not be able to be updated once released. Furthermore, if the product malfunctions, the results may include death, serious bodily harm, or major financial setbacks. Therefore, my code must be correct the first time, as I will not get a second chance.

What techniques are available for this? I already plan on extensive testing, but I know that testing can only demonstrate the presence of bugs, not prove their absence.

Answer 1

The solution is actually to hire software developers who have been doing that kind of work before, and to prepare for an enormous bill. If you are asking for help here, then frankly you don’t have a chance.

Answer 2

The solution is formal verification. This involves writing not only the software, but also a formal specification. Most importantly, one then writes a machine-checked proof that the program one has written is correct against the specification.

Formal verification is difficult and expensive. However, it can be justified in extremely critical code, and code that could kill someone if it breaks certainly qualifies.