Symbolic-VM-based verification engine.
Uses a semantic MIR executor to build symbolic state, then checks safety properties with a unified property checker.