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

We know that they correctly implement their specification*

	▲	meithecatte 4 days ago \| parent [-]
		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.