>is it really that high of a skill barrier?
Last time i checked seL4 was about 20,000 lines of code and 1.3 million lines of proof, so yes, it's hard.