It needs to be said that software formal verification is much, much harder than hardware, and it will put much harder limits on they way you design a programs.

It needs to be said that software formal verification is much, much harder than hardware, and it will put much harder limits on they way you design a programs. I suspect it would not be rare for a software project written this way to have more work hours spent on verification, than the development itself. The use of shared code would be even more pervasive to the point whole library will likely be replaced rather than doing a single LOC change. Hardware verification is very much like a pyramid. Verified cells are made of verified, and characterised to death semiconductor devices. Verified gates are made of verified cells. Verified logic components are made of verified logic gate designs. Verified libraries are built upon verified logic components. Verified blocks built upon verified libraries. And verified macroblocks built upon verified blocks.