Soundness of the simply typed lambda calculus in ACL2. - Sol Swords; William R. Cook (ACL2, 2006)

Centaur Technology Media Unit Verification. - Warren A. Hunt Jr.; Sol Swords (CAV, 2009)

Use of Formal Verification at Centaur Technology. - Warren A. Hunt Jr.; Sol Swords; Jared Davis; Anna Slobodová (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

A Mechanically Verified AIG-to-BDD Conversion Algorithm. - Sol Swords; Warren A. Hunt Jr. (ITP, 2010)

A flexible formal verification framework for industrial scale validation. - Anna Slobodová; Jared Davis; Sol Swords; Warren A. Hunt Jr. (MEMOCODE, 2011)

Bit-Blasting ACL2 Theorems - Sol Swords; Jared Davis (ACL2, 2011)

Verified AIG Algorithms in ACL2 - Jared Davis; Sol Swords (ACL2, 2013)

Microcode Verification - Another Piece of the Microprocessor Verification Puzzle. - Jared Davis; Anna Slobodová; Sol Swords (ITP, 2014)

Fix Your Types. - Sol Swords; Jared Davis (ACL2, 2015)

Meta-extract: Using Existing Facts in Meta-reasoning. - Matt Kaufmann; Sol Swords (ACL2, 2017)

Term-Level Reasoning in Support of Bit-blasting. - Sol Swords (ACL2, 2017)

Incremental SAT Library Integration Using Abstract Stobjs. - Sol Swords (ACL2, 2018)

Hint Orchestration Using ACL2's Simplifier. - Sol Swords (ACL2, 2018)

Verifying x86 instruction implementations. - Shilpi Goel; Anna Slobodová; Rob Sumners; Sol Swords (CPP, 2020)

New Rewriter Features in FGL. - Sol Swords (ACL2, 2020)

Generating Mutually Inductive Theorems from Concise Descriptions. - Sol Swords (ACL2, 2020)

Balancing Automation and Control for Formal Verification of Microprocessors. - Shilpi Goel; Anna Slobodová; Rob Sumners; Sol Swords (CAV (1), 2021)

Robust, End-to-end Correctness Proofs of Industrial Divide and Square Root RTL Designs. - Sol Swords; Cuong Chau (ARITH, 2025)