Finite automata and context-free grammars This repository contains a blueprint for the formalisation of some results in about finite automata and context-free grammars in Lean 4.