I think the most interesting thing is that they loaded the compiled binary right into lean, if I'm understanding the technical paper correctly. Then they use ARM semantics as the base to prove other properties. That's really exciting that they went all the way to the binary level! It reminds me a bit of metamath-c, in that they verify every step of the process, all the way down to binary, so nothing in-between is missed.