To improve the quality of software, formal methods are expected to be proper solutions. They enable rigorous analysis of systems specifications. In this report, we introduce formal methods into the specification of digital ATC track database. This specification defines the invariants to be kept at all times and a small set of operations. Proof obligations, which are items to be proved in order to verify the integrity of the specification, are then generated automatically. All of the proof obligations are mechanically proved to the fullest, although some proof obligations are proved interactively.