Anyone wanting to see their Correct by Construction method in action can Google Tokeneer. It was a demo sponsored by NSA and open sourced to inspire more companies to write tobust software that could meet EAL5 at least. Simple enough for beginners go understand too.