There are probably orders of magnitude in difference between hardware design output and programming output. At least at the time, seL4's verification was quite impressive for a codebase on the order of 10,000 lines. But we should work towards the goal of improved formal modelling and checking all the same.