Is it possible to create formal proofs of interesting mathematical theorems which are mechanically checked in every detail and yet are readable and even faithful to the best expositions of those results in the literature? This paper answers that question positively for theorems about decidable properties of finite automata. The exposition is from Hopcroft and Ullman's classic 1969 textbook Formal Languages and Their Relation to Automata. This paper describes a successful formalization which is faithful to that book.
The requirement of being faithful to the book has unexpected consequences, namely that the underlying formal theory must include primitive notions of computability. This requirement makes a constructive formalization especially suitable. It also opens the possibility of using the formal proofs to decide properties of automata. The paper shows how to do this.