Not having a formal kernel module system does not actually mean the kernel is secure. Exploits to create module loading systems out of kernel vulnerabilities are approximately as old as stack overflow exploits.
NX enforced kernel W^X, SMEP/SMAP, always-on stack protector and a limited attack surface (..say, from pledge(2)), only serve to make such theoretical attacks impractical against OpenBSD.
I'm glad you're saying it, too, as I get tired of this myth. I wrote a scheme on Schneier's blog for disproving it a while back. Basically, you counter the mitigations which look awfully similar to the one's that got countered in Linux and Windows. Once you have that, wait until a bug is mentioned on mailing list that can lead to memory attack. Weaponize it. Profit.
Leads me to what I claim is dirty secret behind "only 2 holes in..." claim they have: OpenBSD just fixes bugs they find without serious attempts to determine if they'd be exploitable vulnerabilities. They just do accounting differently than the rest. So, by their numbers, they only had 2 vulnerabilities because they didn't assess whether other bugs were vulnerabilities in the first place.
They have good code quality but they're full of shit about how vulnerable it is or isn't.
What really annoys me with OpenBSD is that users are expected to download the CVS source and compile it to fix problems rather than upgrade to a dot-release.
For a normal user that's fine, but if you have a bunch of servers you'll need a sophisticated build/deploy infrastructure to stay updated.
That means no Internet-facing service has ever had a bug of the sort that often becomes code-injection. Or they didn't test for exploitability in the case of mitigations being bypassed. Neither one makes the claim stand up as it has hidden implication of "only two remote holes for amateurs and people ignoring mitigations."
"What really annoys me with OpenBSD is that users are expected to download the CVS source and compile it to fix problems rather than upgrade to a dot-release."
Yeah, that sounds like it could be annoying. They should have both options available given they already have to trust OpenBSD team to not backdoor their stuff.
"Only two remote holes in the base install". That's because the base install contains very little in terms of remotely accessible services (only OpenSSH I believe?).
Even as an OpenBSD fan, I'm not sure why tptacek was downvoted here. W^X etc. make it harder to write an exploit, but sufficiently-bad bugs can still yield arbitrary code execution. (Or confused-deputy problems allowing escalation to root, etc.; there's more than one way to pwn a box.)
And - architecturally - OpenBSD's kernel isn't that different from Linux, both being UNIX-style kernels; to the extent that OpenBSD's kernel has better security than Linux, it's mostly because OpenBSD tends to have fewer (and, sometimes, better-considered) features.
(There's an interesting argument to be had about Linux+grsecurity vs. OpenBSD - focusing on having some cutting-edge parts vs. solid engineering throughout - but that's not the argument we're having.)
Do you need a "truly wonderful proof" for "the mainstream OS OpenBSD has not managed to render kernel vulnerabilities unexploitable, or to rid itself of those vulnerabilities entirely"? Because: that's an extraordinary claim for an OpenBSD supporter to make.