Programming and automating mathematics in the Tarski–Kleene hierarchy

•A reference formalisation of Kleene and relation algebras in Isabelle/HOL is given.•This includes the most important models of these algebras.•Libraries contain laws for important relation-algebraic concepts.•These include vectors, functions, reflexive transitive closure.•Direct relational products are presented as an advanced formalisation example.

We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example.