An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem. - David M. Russinoff (J. Autom. Reason., 1985)

Proteus: A Frame-Based Nonmonotonic Inference System. - David M. Russinoff (Object-Oriented Concepts, Databases, and Applications, 1989)

A Verification System for Current Programs Based on the Boyer-Moore Prover. - David M. Russinoff (Formal Aspects Comput., 1992)

A Mechanical Proof of Quadratic Reciprocity. - David M. Russinoff (J. Autom. Reason., 1992)

A Verified Prolog Compiler for the Warren Abstract Machine. - David M. Russinoff (J. Log. Program., 1992)

Specification and verification of gate-level VHDL models of synchronous and asynchronous circuits. - David M. Russinoff (Specification and validation methods, 1993)

A Mechanically Verified Incremental Garbage Collector. - David M. Russinoff (Formal Aspects Comput., 1994)

A Formalization of a Subset of VHDL in the Boyer-Moore Logic. - David M. Russinoff (Formal Methods Syst. Des., 1995)

A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor. - David M. Russinoff (LMS J. Comput. Math., 1998)

A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. - David M. Russinoff (Formal Methods Syst. Des., 1999)

A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD AthlonTM Processor. - David M. Russinoff (FMCAD, 2000)

A Mathematical Approach to RTL Verification. - David M. Russinoff (CAV, 2007)

A Mechanically Verified Commercial SRT Divider. - David M. Russinoff (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables. - David M. Russinoff (IEEE Trans. Computers, 2013)

Modeling Algorithms in SystemC and ACL2. - John W. O'Leary; David M. Russinoff (ACL2, 2014)

A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. - David M. Russinoff (ACL2, 2017)

Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. - David M. Russinoff (ACL2, 2020)

Formal Verification of Floating-Point Hardware Design - A Mathematical Approach, Second Edition - David M. Russinoff (Formal Verification of Floating-Point Hardware Design, 2nd Edition, 2022)

Formal Verification of a Chained Multiply-Add Design: Combining Theorem Proving and Equivalence Checking. - David M. Russinoff; Javier D. Bruguera; Cuong Chau; Mayank Manjrekar; Nicholas Pfister; Harsha Valsaraju (ARITH, 2022)

Properties of the Hebrew Calendar. - David M. Russinoff (ACL2, 2022)

A Formalization of Finite Group Theory. - David M. Russinoff (ACL2, 2022)

A Formalization of Finite Group Theory: Part III. - David M. Russinoff (ACL2, 2023)

A Formalization of Finite Group Theory: Part II. - David M. Russinoff (ACL2, 2023)

A Formalization of Elementary Linear Algebra: Part I. - David M. Russinoff (CoRR, 2025)