In Formal Languages and Automata Theory courses, students are introduced to various state machines that require careful reasoning to design. For some students, understanding nondeterministic behavior is challenging. This means that they are unsure why a word is accepted or rejected. Consequently, they are unable to validate and verify their machines. To aid students’ understanding, we propose the use of a dynamic visualizations tool in conjunction with a design-based approach using a domain-specific language to implement machines. The proposed tool is designed using the Norman principles of effective design. The tool traces all possible computations without repeated machine configurations and uses color to distinguish between accepting and rejecting computations. In addition, they aid in the verification process by affording users the ability to validate machines by visualizing the value of state invariants. Our research project, therefore, is twofold: develop the proposed visualization tool and evaluate their effectiveness to help students design, implement, validate, and verify machines.