I don't think formally verifying my showing that the model is correct is good enough anymore. You must prove that your implementation refines the model.