A system and method for managing and composing verification engines and simultaneously applying such compositions to verify properties with design constraints allocates computing resources to verification engines based upon properties to be checked and optionally a user-specified budget. The verification engines are run in order to verify a received register transfer level (RTL) design description of a circuit according to user-specified assertions and constraints received by the system. The particular verification engines to be run are selected from a database of such engines and a run order is designated in sequential, parallel and distributed flows.