A book about transducers. It covers string-to-string functions, such as Mealy machines or two-way transducers. All results in the book have been formalized in Lean, and the formalization is linked to the web interface.