Formally Verifying Automata for Trusted Decision Procedures

Automata-theoretic decision procedures date back to Büchi’s work, leveraging finite automata to decide sentences in weak theories of arithmetic. An extension of the original procedure by adding automatic sequences is now implemented in the Walnut software to check and discover theorems in combinatorics and number theory. However, automata based decision procedures do not generate efficiently checkable correctness guarantees as they run, raising concerns regarding the reliability and trustworthiness of the results they produce. Towards addressing this issue, we are building an automata library in Lean, which is both a proof assistant and a programming language. By formalizing executable automata and proving their properties, we provide a foundation for trusted automata theoretic decision procedures. We begin with Chapter 1, which introduces the context and motivation for this project. The basic mathematical theory of words and automata is provided in Chapter 2, with their formalization explained. Chapter 3 presents a decision procedure for automatic sequences, and reports the verification of crucial automata in volved. To our knowledge, this is the first exposition of a direct decision procedure for automatic sequences in full mathematical detail, together with the first formally veri f ied automata library designed to support a decision procedure for automatic sequences. We conclude in Chapter 4 by summarizing our contributions and propose directions for future work.