This paper discusses the use of intuitionistic linear-time μ-calculus (IμTL) whose underlying model is based on Heyting algebra of prefixed closed sets as the basis for the specification of assumption and guarantee paradigm, and then propose an assumption-guarantee rule in IμTL. The rule formulated is more general then previously proposed rules that used linear-time temporal logic (LTL) in the specification of assumption and guarantee paradigm and extends the discussion for safety properties of the form “always φ”, and therefore represents more uniform reasoning of assumption and guarantee specifications for also supporting circular compositional reasoning.