They've done a really good job documenting it in their papers and online docs, but the general flow is to verify equivalence of the generated binary and the formal specification, then to prove properties like memory safety of the formal spec.

I'd start here if you want to learn more: https://sel4.systems/Info/FAQ/proof.pml

Let me know if you have any other questions.