Formal method provides a way to achieve an exact and consistent definition of security for a given scenario. This paper presents a formal state-based verifiable RBAC model described with Z language, in which the state-transition functions are specified formally. Based on the separation of duty policy, the constraint rules and security theorems are constructed. Using a case study, we show how to specify and verify the consistency of formal RBAC system with theorem proving. By specifying RBAC model formally, it provides a precise description for the system security requirements. The internal consistency of this model can be validated by verification of the model.