[xelxebar]

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend.

Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.

[i2talics]

Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?

[poizan42]

Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.