Hacker News Reader

Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.

View on HN

We know that they correctly implement their specification*

No, they are correct, because the deciders themselves are just a cog in the proof of the overall theorem. The specification of the deciders is not part of the TCB, so to speak.

Reply on news.ycombinator.com