[UltraSane]

It is a lot like how you have to trust the core proving kernel in a theorem prover but if you do then you can trust every proof created using it.

[burnt-resistor]

https://github.com/CertiCoq/certicoq can prove (most of) itself.