A highly reliable flight control system (FCS) is a necessary prerequisite for the reliable operation of an aircraft. Under the traditional development approach, the domain knowledge is first modeled by the human in the form of natural language, and then code is written by humans according to the model, and finally, the software defects are eliminated by using testing technology. The approach fails to build reliable FCS, because of human error, natural language ambiguity, and incompleteness of test techniques. A novel development approach based on formal verification technology could improve the reliability of FCS from many aspects. This paper presents a formal design and verification method for multicopter propulsion subsystem based on Coq and generated a usable and highly reliable functional software library. The main work of this study includes:the domain knowledge is organized into a hierarchical document suitable for formal verification, the basic functions, and composite functions are separated, and the concept of the simplest form of function (SFF) is proposed; formalize the system in Coq according to this document, defining constants, variables, basic functions, composite functions, SFF, axioms, etc.; the correctness of the derivation of all kinds of composite functions is expressed as lemmas and be proved; the algorithm for solving practical problems such as the longest hover time of multicopter is given; and a functional software library is generated using OCaml language by COQ program extraction ability. In the future, more subsystems of FCS will be developed based on formal verification, and finally, a complete and highly reliable FCS with formal verification will be established.