7500 sor? Nem lesz az egy kicsit kevés? Amúgy a formális helyességbizonyítás annyit igazol, hogy a szoftver megfelel a specifikációnak. A specifikáció ellen nem véd.