Are there algorithms for proving two finite state machines are equivalent?
Given two deterministic finite automata $A_1,A_2$, you can construct the product automaton $A_1 \times A_2$ using the product construction. Let a mixed state be one which is accepting in $A_1$ and rejecting in $A_2$, or vice versa. The two automata are equivalent iff no mixed stated is reachable from the initial state.