1. A method for verifying a system model, the system model comprising a plurality of terms, particular ones of the plurality of terms defining at least one performance attribute of the system model, the method comprising the operations of: identifying a plurality of unannotated terms from the plurality of terms; annotating particular ones of the plurality of unannotated terms with a first annotation, and annotating particular other ones of the plurality of unannotated terms with a second annotation; proving the correctness of the particular ones of the unannotated terms which are annotated with the first annotation, the proving the correctness operation using a set of inference rules to prove the correctness of the particular ones of the unannotated terms which are annotated with the first annotation, at least one inference rule of the set of inference rules being a Nuprl inference rule, and the annotated terms having the second annotation requiring no proof of correctness; performing a verification of the system model using the annotated terms having the first annotation and the annotated terms having the second annotation, the verification providing an indication whether the system model operates in accordance with a set of system properties; and adjusting the system model as a function of the indication.