No, this isn’t about formally verifying benchmarking (BM) crimes. It’s about the use of misleading statistics in papers that apply formal methods (FM) to verify (prove correct) operating systems (OS) code – something that has been bugging me for a while. NameLanguageSpec. Lang.Proof:CodeseL4C+AsmIsabelle20:1CertiKOSC+AsmCoq15:1SeKVMC+AsmCoq7:1IroncladDafnyDafny5:1XXXRustVerus10:1YYYRustVerus7.5:1Table 1: Language and (incomplete) proof-size statistics of a number of verified systems [Anonymous]....