Until now, human dev time has arguably been the bottleneck preventing more use of formal verification methods in software. Making it possible will likely involve completely rearchitecting many components, but that has become more realistic now. It would be interesting to see how close we can get to formally verified Linux if we are willing to make compromises on complexity