diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index b9e097db1a38304cd77bf47975cbe8c53cb9aa58..9707b813e39d2dfd1c0817025af504980c8a0e05 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -247,26 +247,6 @@ let convertToMu formula =
   in
   convert_post helper formula
 
-let verifyMuAltFree formula =
-  true
-
-let verifyMuMonotone forumla =
-  true
-
-let verifyMuGuarded formula =
-  let helper f =
-	match f with
-	| MU (s, f1)
-	| NU (s, f1) ->
-	   (match f1 with
-		| VAR s ->
-		   raise (CoAlgException ("formula not guarded"))
-		| _ -> ())
-	| _ -> ()
-  in
-  iter helper formula;
-  true
-
 (** Appends a string representation of a formula to a string buffer.
     Parentheses are ommited where possible
     where the preference rules are defined as usual.
@@ -626,6 +606,122 @@ let lexer = A.make_lexer
 
 let mk_exn s = CoAlgException s
 
+(** Process from inside out. cons all variables seen, remove them when
+    binding fixpoint is found. Fixpoint type may only change if last
+    (inner) fixpoint didn't include any free variables.
+ *)
+let rec verifyMuAltFree formula =
+  let proc = verifyMuAltFree in
+  match formula with
+  | TRUE | FALSE | AP _ -> ("none", [])
+  | CONST _
+  | CONSTN _ -> ("none", [])
+  | AT (_,a) | NOT a
+  | EX (_,a) | AX (_,a) -> proc a
+  | OR (a,b) | AND (a,b)
+  | EQU (a,b) | IMP (a,b) ->
+	 let (atype, afree) = proc a
+	 and (btype, bfree) = proc b in
+	 if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+		  (compare atype "ν" == 0 && compare btype "μ" == 0) then
+	   raise (CoAlgException ("formula not alternation-free"));
+	 if compare atype "none" == 0 then
+	   (btype, List.flatten [afree; bfree])
+	 else
+	   (atype, List.flatten [afree; bfree])
+  | ENFORCES (_,a) | ALLOWS   (_,a)
+  | MIN (_,_,a)    | MAX (_,_,a)
+  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
+  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
+  | ID(a) -> proc a
+  | NORM(a, b) | NORMN(a, b)
+  | CHC (a,b)  ->
+	 let (atype, afree) = proc a
+	 and (btype, bfree) = proc b in
+	 if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+		  (compare atype "ν" == 0 && compare btype "μ" == 0) then
+	   raise (CoAlgException ("formula not alternation-free"));
+	 if compare atype "none" == 0 then
+	   (btype, List.flatten [afree; bfree])
+	 else
+	   (atype, List.flatten [afree; bfree])
+  | FUS (_,a) -> proc a
+  | MU (s, f) ->
+	 let (fptype, free) = proc f in
+	 (if (compare fptype "ν" == 0) then
+		raise (CoAlgException ("formula not alternation-free")));
+	 let predicate x = compare x s != 0 in
+     let newfree = List.filter predicate free in
+	 if newfree = [] then
+	   ("none", [])
+	 else
+	   ("μ", newfree)
+  | NU (s, f) ->
+	 let (fptype, free) = proc f in
+	 (if (compare fptype "μ" == 0) then
+		raise (CoAlgException ("formula not alternation-free")));
+	 let predicate x = compare x s != 0 in
+     let newfree = List.filter predicate free in
+	 if newfree = [] then
+	   ("none", [])
+	 else
+	   ("ν", newfree)
+  | VAR s -> ("none", [s])
+
+(** Process from outside in. For every variable bound keep the tuple
+    (name, negations). For every negation crossed map a +1 over snd on
+    that list. For every variable met check that the matching
+    negations is even.
+ *)
+let rec verifyMuMonotone negations formula =
+  let proc = verifyMuMonotone negations in
+  match formula with
+  | TRUE | FALSE | AP _ -> ()
+  | CONST _
+  | CONSTN _ -> ()
+  | AT (_,a)
+  | EX (_,a) | AX (_,a) -> proc a
+  | OR (a,b) | AND (a,b)
+  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
+  | ENFORCES (_,a) | ALLOWS   (_,a)
+  | MIN (_,_,a)    | MAX (_,_,a)
+  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
+  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
+  | ID(a) -> proc a
+  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
+  | CHC (a,b)  -> (proc a ; proc b)
+  | FUS (_,a) -> proc a
+  | MU (s, f)
+  | NU (s, f) ->
+	 let newNeg = (s, 0) :: negations in
+	 verifyMuMonotone newNeg f
+  | VAR s ->
+	 let finder (x, _) = compare x s == 0 in
+	 let (_, neg) = List.find finder negations in
+	 if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
+  | NOT a ->
+	 let increment (s, n) = (s, n+1) in
+	 let newNeg = List.map increment negations in
+	 verifyMuMonotone newNeg a
+
+let verifyMuGuarded formula =
+  let helper f =
+	match f with
+	| MU (s, f1)
+	| NU (s, f1) ->
+	   (match f1 with
+		| VAR s ->
+		   raise (CoAlgException ("formula not guarded"))
+		| _ -> ())
+	| _ -> ()
+  in
+  iter helper formula
+
+let verifyFormula formula =
+  verifyMuAltFree formula;
+  verifyMuMonotone [] formula;
+  verifyMuGuarded formula
+
 (** These functions parse a token stream to obtain a formula.
     It is a standard recursive descent procedure.
     @param ts A token stream.