Correctness by Construction

Correctness by Construction is a radical, effective and economical method of building software with high integrity especially for security-critical and safety-critical applications. It produces software with extremely low defect rates — fewer than 0.1 defects per thousand lines of code — with good productivity — up to around 30 lines of code per day.

At Praxis Critical Systems Anthony Hall and colleagues developed Correctness by Construction to unify a number of ideas:

It brings these strands together into a process framework and a set of principles for developing software intensive systems. It has been applied successfully in several projects such as the MULTOS CA.

To learn more about Correctness by Construction, see