Malware detection and classification is critical for the security of IT infrastructure. Legacy detection of malware has been highly reliant on static signatures, so malware authors have evolved code polymorphic techniques to counteract these tools, thus rendering static malware detectors ineffective. While malware writers may easily use code rewriting techniques to scramble binary images; malware processes at runtime still must conduct a sequence of operational steps to achieve its design goal, indicating an approach based on behavioral analysis where the captured invariants form a new type of forensic fingerprint. Moreover these operational steps are constrained to occur within the computers' or mobile devices' abstract system interface- A finite basis of activities that submit to effective monitoring with a variety of tools. In this work, we propose a formalism for expressing these behaviors, learning them and analyzing them to form automated malware analysis tools. Thus motivated by a need to detect and classify malware, we root its foundation in formal verification, as well as methodology from statistical and machine learning. Specifically using trace data from malware we leverage formal verification methods (such as probabilistic model checking) to construct classifiers and evaluate their efficacy in supervised learning and cross-fold validation experiments. The results inform how a fully automated reasoning mechanism may be applied to unknown software by posing its system trace as a query to various classifiers as hypothesis testing, the outputs informing belief of membership. Finally, we demonstrate the method and results on real malware data.