I do not quite get it: seL4 is verified. Is the rest of the code as well? I understand that verification of Rust is just starting to gain traction (compared to C, Java or Ada), or did they make major progress here?