A cyclic proof is a, possibly infinite but, regular derivation tree in which every infinite path satisfies a certain soundness criterion, the form of which depends on the logic under study. Circular and, more generally, non-wellfounded derivations are not traditionally regarded as formal proofs but merely as an intermediate machinery in proof-theoretic investigations.

They are, however, an important alternative to finitary proofs and in the last decade have helped break some important barriers in the proof theory of logics formalising inductive and co-inductive concepts. In this talk we focus on cyclic proofs for modal logics, ranging from Gödel-Löb logic to more expressive languages such as the modal mu-calculus, and reflect on how they can contribute to the development of the theory of fixed point modal logic.