Be that as it may, seL4 cannot currently be automatically verified, and it's not due to code size (8700 lines of C and 600 lines of assembler). It's hard to see what the obstacle to mechanisation could be but logical complexity.
Model theory is not some magical deduction-free paradise. The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent. Building models of Peano arithmetic in ZFC for example, but also relating constructive and classical logic through double negation or embedding type theory in set theory, are all about relative consistency. It's easy to make a FOM (= foundation of mathematics) unsound, and logical luminaries including Frege, Church and Martin-Lof managed to do so. Those soundness proofs in essence transform a proof of falsity in one system to the other, and relative consistency is the best we can get in order to increase our confidence in a formal system. It is true that traditional model theory, as for example done in [1, 2, 3]. doesn't really foreground the deductive nature of ZFC, it's taken for granted, and reasoning proceeds at a more informal level. If you want to mechanise those proofs, you will have to go back to deduction.
[1] W. Hodges, Model Theory.
[2] D. Marker, Model Theory: An Introduction.
[3] C. C. Chang, H. J. Keisler Model theory.