https://github.com/opencontrol/ https://github.com/opencontrol/compliance-masonry
To apply formal methods to software development, you do one of two things:
* You transform code in conventional programming languages into machine-readable formats understood by model checkers
* You write your code in a language that itself admits to being model checked.
I appreciate this link, though; I was unaware of what 18F was doing here.
The reason all that "formal methods" stuff is in there as well (and indeed it's what the more prominent repos in there are about) is so that we can eventually connect the dots between effective security practices in code and the management of the security controls on the administrative side, and at least until the former catches up to the software methods, take the manual work of generating the copious documentation regarding all of this out of the developers' hands. Case in point: https://compliance.cloud.gov/ (<- all auto-gen, AFAIK)
Rigorously define security goals ("no user can see another user's file; no input can cause this handler to access variables other than this specific list").
Convert all or, more likely, part of your program into a model; for instance, predicate logic.
Run analysis tools to verify that the model achieves the security goals. Once expressed in a mathematical model, "proving" it becomes a search problem, achievable with code. Intuition and cleverness can, if your model is accurate and complete, be eliminated.
It's sort of the software security equivalent of teaching a computer to play chess.