Evaluating the accuracy of a model is an unsolved problem with both formal and informal approaches.
Formally: we could ask multiple separate model/proof assistants to generate separate models from the same underlying specification, and then attempt to find discrepancies between their predicted results. This really just punts the responsibility: now we're relying on the accuracy of the abstract specification, rather than the model(s) automatically or manually produced from it. It's also not sound; it just allows us to feel more confident.
Informally: we can have a lot of different people look at the model very closely, and produce test vectors for the model based on human predictions of behavior.
Formally: we could ask multiple separate model/proof assistants to generate separate models from the same underlying specification, and then attempt to find discrepancies between their predicted results. This really just punts the responsibility: now we're relying on the accuracy of the abstract specification, rather than the model(s) automatically or manually produced from it. It's also not sound; it just allows us to feel more confident.
Informally: we can have a lot of different people look at the model very closely, and produce test vectors for the model based on human predictions of behavior.