We present an intuitionistic counterpart of the modal \(\mu \) -calculus formulated with the binary Lewis arrow, a generalisation of the \(\Box \) -operator. Using Ruitenburg’s theorem, we prove that every formula is equivalent to a guarded one. We then provide a sound and complete non-wellfounded proof system for the logic that is cut-free, and obtain as a corollary that the logic is decidable and admits a cyclic proof system. A game semantics for the logic is developed which acts as a mediator between the formal proof system and the relational semantics.