A man-machine interaction risk scene recognition method based on formal verification comprises the following steps that firstly, carrying out modeling on a complex man-machine interaction deduction process, and forming a universal man-machine interaction formal deduction model; 2, establishing a task formal model automatic deduction template considering human errors, and a system, a human-computerinterface and an environment formal model automatic deduction template considering abnormal states; 3, determining a man-machine system security attribute expression to obtain a man-machine system security specification; 4, completing the troubleshooting of a risk scene path by means of a model checking tool; 5, evaluating the possibility of the evolution path by adopting a qualitative comparisonmethod, and identifying a risk scene path with relatively high occurrence possibility; Through the above steps, a man-machine interaction formalization method is adopted, the problem of completenesschecking of abnormal-state interaction risk scenes of a man-machine system is solved, the effect of automatically completing complete enumeration of risk scene paths is achieved, and recognition of key risk scenes is achieved through a qualitative comparison method.