Liveness rules from fairness based on TLA

Formal methods use mathematic and logic method to describe and validate the system, TLA (The temporal logic of actions) is for specifying systems, it is brought forward by Leslie Lamport, and it can specify a system´s modeling and property together. Its specifying language is TLA+ and the checking tool is TLC. Liveness property is important property of a system, it is close relation to fairness property. It is in formal a conjunct of the fairness properties of the system properties. Leslie Lamport has put forward several liveness rules. We use a new way to prove the liveness rule from weak fairness and the liveness rule from strong fairness.