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!
It feels to me like this has already been explained before (1, 2). To prove that an automaton is correct, you first must define what correctness means to you. Usually that is done by writing a specification of what it means to be correct. Then, you prove that an automaton meets the specification.
If you're interested in knowing how to do that, that's a broad subject that people have written entire books about. I suggest reading a textbook on model checking (particularly of finite-state systems).
How do you know what the specification should be? Well, you have to figure out what correctness means, or the requirements are. That's not really a question about computer science but rather a question about your application or your business domain and what problem you are trying to solve or what you're trying to do with the automaton.
If you're asking "what to verify", we can't answer that, because that's something you have to decide: you have to decide what properties you want to prove. It's like asking 'how do I prove the natural numbers?' You can't. You have to decide what theorem you want to prove, before you can ask how to prove it. If you ask a mathematician how to know what theorems to prove, the answer will probably be something like "well, you have to figure out what you want to know or what is interesting to know".
