In order to adapt the actual application requirements, sensitive-level functions, perfect integrity labels of subjects and objects were added in the traditional Biba model. Also its safety operation rules were improved. The elements, the invariants and the transition rules of the improved model were described in completely formal methods. By doing this, the model was automatically formal verified by using theorem-prover Isabelle. The formal description and formal verification satisfied the formal methods requirement in the development of high-level secure operating systems.