> A debugging build I made in December is about 20k lines > before the preprocessor runs and about 30k afterwards. > The formal verification code, written in Isabelle/HOL[2], > is about an order of magnitude greater than that.
Just out of curiosity (since I'm unfamiliar with the concepts), what is the code complexity like? If the verification code is larger, is it also more complex? If yes, can the verification code somehow be checked against possible errors as well?
