1. A method comprising: verifying a security property for an operational model of a microvisor adapted for deployment in a node of a network, wherein the operational model is created in a functional programming language; generating an executable of the operational model; initiating a state dump of the executable operational model; initiating a corresponding state dump of the microvisor; iteratively comparing the states of the executable operational model and the microvisor; and continuing iterative comparison of the states of the executable operational model and the microvisor until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the security property is implemented by the microvisor.