[aksdlf]

I'm glad to hear that Meta and Google code is "rigorous". I'd prefer INRIA, universities that fund theorem provers, industries where correctness matters like aerospace or semiconductors.

[chc4]

Windows doesn't use the Linux eBPF verifier, they have their own implementation named PREVAIL[0] that is based on an abstract interpretation model that has formal small step semantics. The actual implementation isn't formally proven, however.

0: https://github.com/vbpf/ebpf-verifier

[SoftTalker]

Also that lines of code is a proxy for rigor, something new I learned today. /s

[sunnyps]

I think they mean that the code base is small enough to be audited thoroughly. Maybe they should reword it to be clearer.

[lmm]

> I think they mean that the code base is small enough to be audited thoroughly.

They wouldn't say it was "over 20,000 lines" in that case. And 20,000 lines of C is far too big to audit.