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 are 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 of a trusted decision procedure for automatic sequence. They can also be used for decision procedures for Presburger arithmetic and Büchi's WS1S.