Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think a

Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).