Correct By Construction

This site exists to collect resources that enable the creation of reliable, trustworthy, and secure software that can fix the root cause of cybersecurity issues.

Status of This Site

Initial migration in progress. Currently moving data over from the awesome-weird-machines-and-langsec and rocket-surgery repositories as well as other collections.


Because software as it is currently written is impossible to secure, the costs of insecure software are rising rapidly, and an economic collapse of the industry is rapidly approaching if things do not change.

The cost of poor software quality in the US has grown to at least $2.41 trillion as of 2022, with accumulated software Technical Debt of ~$1.52 trillion. Some insurance companies are no longer offering cyber security insurance due to the increasing severity and incidence of cyber attacks.

Does it Work

For decades projects have been built using these techniques. Not only are the defect rates near zero, but the initial cost to build such projects is far lower (1/3 of the conventional cost for the Tokeneer project).

Two example videos covering such projects:

HACMS MH-6 Little Bird helicopter

HACMS MH-6 Little Bird helicopter (3:43)

Making Software ‘Correct by Construction’ - Professor Martyn Thomas CBE

Making Software ‘Correct by Construction’ - Professor Martyn Thomas CBE (51:46)

More Detail

The rest of this site provides more details and sources about why we must address this issue, the full nature of the problem, solutions to these issues (many of which are decades old), and a list of resources for further reading.