Q Framework
The Q Formal Analysis Framework is a set of software tools used to formally prove that implementations of high-consequence digital systems meet mathematical specifications. The tools are designed to work together as a set. Specifications are derived directly from high-level requirements and expressed in the QSpec hierarchical state machine format. The toolkit includes QSpec, QRefact, and QReqs. Sandia National Laboratories is a multimission laboratory managed and operated by National Technology & Engineering Solutions of Sandia, LLC, a wholly owned subsidiary of Honeywell International Inc., for the U.S. Department of Energy’s National Nuclear Security Administration under contract DE-NA0003525. SAND2021-0504 O