Verified Flight Control System (VFCS) is an academic project for study the FCS software by theorem prover Coq.
We adopt the idea of construct-correct to analysis, modeling and design the FCS.
Coq proof assistant is a higher-order logic theorem prover based on Calculus of Inductive Constructions.
We mainly study the Multicopter at the first stage.
Below are main links of this project: