Developing with Formal Methods at BedRock Systems

The BlueRock HyperVisor is a commercial, highly concurrent, verified virtualization platform that employs formal methods to enable proofs of complex, lock-free concurrent code; support automating proofs of large programs; and integrate with “informal” parts of the software lifecycle.