For seL4, models were used to map all the way from the semantics of the instruction set to the high level model; this included a model of equivalence between the C source code and the machine code. Took them basically from 2006 to 2014 to do that (including the time to author and verify the kernel in particular).