Formalization only helps you if you prove that the formalization is correctly implemented, that the model didn’t subtly mess up or cheat.

Someone still has to read the formalization.