Formal verification of emergent properties