As promised, I found the paper readable without too much scientific/academic jargon. It's really impressive what was achieved: verification of an entire general

As promised, I found the paper readable without too much scientific/academic jargon. It's really impressive what was achieved: verification of an entire general-purpose kernel. And the conclusion is also potentially very significant: > This opens an exciting prospect for the future: should we be able to reduce the verification cost by another factor of two, then verified software will become cost-competitive under all circumstances, at least for the scale of systems we have been looking at. We are optimistic that increased automation will achieve this in the near future.