Visible to the public Correctness by Construction of High-Integrity Software