We describe the development and the analysis of the label distribution protocol (LDP) for the multiprotocol label switching system. We review the implementation issues that are required to construct the LDP for a gigabit switched router, and propose a detailed design of the LDP. We present the detailed design using the deviation tree of the protocol state machine and a formal specification of the state machine using process algebra. These specifications are based on the IETF standard. By analyzing the protocol behavior of the deviation trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP, and we expect that the reliability would be improved using these analyses. With the proofs, we expect the implemented LDP will be interoperable with other commercialized products. As a result, we validate the protocol behavior of the implemented LDP.