1. A computer system for formal verification of models, the system comprising: a processor; one or more model reducers to reduce a model; one or more model checkers to check the model, wherein at least one of the model reducers is to run concurrently on the computer system with at least one of the model checkers; and a model synchronizer running concurrently with the at least one of the model reducers and the at least one of the model checkers on the computer system to synchronize information between the at least one of the model reducers and the at least one of the model checkers, wherein the model synchronizer is to: receive model reduction information from the at least one of the model reducers wherein the model reduction information comprises one or more invariants determined by the at least one of the model reducers, and to transfer the model reduction information to the at least one of the model checkers, and wherein the model synchronizer is to add the one or more invariants to an invariant queue, and, if a size of the invariant queue is greater than a threshold value, to transfer content of the invariant queue to the at least one of the model checkers.