The compendia of Metamath proofs us here https://us.metamath.org/

All of theree are formally from axioms or other formal proofs that lead back to their axioms, without any gaps.