A means of verifying the correctness of hardware or software system design using formal methods. These formal methods compare the functionality of the design with a set of user-specified characteristics or model, described in a notation with a formal mathematical semantics, to ensure that the system specification has been implemented satisfactorily. See design automation.