A computer-implemented method for verifying a model in a product lifecycle management (PLM) system includes defining a model and an envelope of allowable model states and, based on one or more requirements, deriving at least one counterexample objective. The method also includes optimizing a set of parameters related to the allowable model states and the allowable model context, redefining at least one of the model and the allowable model states when the at least one counterexample objective is outside of a specified tolerance, and, after a predefined number of iterations, defining the model as verified.