The Laboratory for Applied Logic (LAL) is a research unit of the Department of Computer Science at Brigham Young University. The lab develops tools for finding proofs of incorrectness in formal models of complex devices. The research is motivated by the pervasive nature of digital devices in society. Lives are affected when missed mistakes emerge in products on the market, and the growing complexity of digital design makes finding all mistakes difficult. Manufacturers expend a large amount of their resources in conventional simulation to reduce the risk of escaped errors. They create different scenarios and simulate the behavior of their product in those scenarios to uncover errors. The approach is not comprehensive and misses critical mistakes because it is not possible to create and simulate all scenarios. In contrast, formal methods define correct behaviors in a product and then search for the existence of incorrect behaviors. The proof of incorrectness in the formal model considers the behavior of the product in all possible scenarios to uncover errors. The current research in LAL focuses on semiformal model checking and incremental refinement to find errors. We apply parallel and machine learning algorithms to improve the performance and capacity of algorithms for finding incorrectness proofs. We use incremental refinement to manage designs as they evolve through the design cycle. Our goal is to create methods which quickly find errors in complex formal models that exceed the capacity of all existing exhaustive methods.