I was considering the interaction between the network layers, various modules such as routing, crust. Also the interaction between various personalities of the nodes. This is where the work of defining precisely the all the conditions that can happen in the protocol, does each module using the protocol interact with the protocol the same way (understand the protocol states precisely the same).
It is one thing to have all modules interact correctly (mathematically proven) when using a particular communications protocol, but do all modules interpret/"understand" the protocol the same? That is a simple example, but when you have a number of communications occurring for a module, does the order of packets affect the module one way and the sending nodes expected another effect. Race conditions can occur, such as two nodes trying to update an SD object at the once address. If the nodes handling the SD object do one thing yet the sending nodes expected another (say error messages) then issues arise and the effectively the whole network has not been proven, even though it may still work correctly.
So its not like its too difficult, but when you are running a full network as compared to a singular control program the complexity increases dramatically. And this is on the core network side of any APIs to the client s/w, which is another set of things needed to be proven.
I expect for the current development that formal verification of modules is feasible, but traditional testing of the protocols will ensure.