It is often not so easy to map the classes directly to the  user requirements when developing with the ObjectOriented methodology. FeatureOriented Programming methodology can solve this problem,so it has significant meaning. In this paper,we firstly introduce the ideas of FOP,its similarities and differences with AspectOriented Programming,and its influence on the corresponding formal verification methods; then we survey the existing FOP formal verification methods and our related work,compare their advantages and disadvantages.Finally,we prospect the future directions of formal verification on FOP.