How to Specify the Behavior of Automata for Verification

Question

I am wondering what it takes to "verify" or "prove" that an automaton is correct. What the components are that are required. It seems that an automaton would be an easier thing to formally verify as sound than say an arbitrary function. Not sure though what needs to be verified in an automaton, which is what brings up the question.

Thank you!