Academic Papers
2015
 Sol Swords and Jared Davis. Fix
your types.
In ACL2
2015. October,
2015. EPTCS
192. Pages 316.
 Abstract.
When using existing ACL2 datatype frameworks, many theorems require type hypotheses. These
hypotheses slow down the theorem prover, are tedious to write, and are easy to forget. We describe a
principled approach to types that provides strong type safety and execution efficiency while avoiding
type hypotheses, and we present a library that automates this approach. Using this approach, types
help you catch programming errors and then get out of the way of theorem proving.
 (See also the FTY Documentation)
 Jared Davis and Magnus O. Myreen.
The reflective Milawa theorem prover is sound (down to the machine code that runs it).
Journal
of Automated Reasoning. Springer. August, 2015. Volume 55(2), Pages
117183.
 Official version (Springer) / Author's preprint version
 Abstract. This paper presents, we believe, the most comprehensive
evidence of a theorem prover's soundness to date. Our subject is the Milawa
theorem prover. We present evidence of its soundness down to the machine
code.
 Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an
idealised version of ACL2's computational logic and provides the user with
highlevel tactics similar to ACL2's. In contrast to NQTHM and ACL2, Milawa has
a small kernel that is somewhat like an LCFstyle system.
 We explain how the Milawa theorem prover is constructed as a sequence of
reflective extensions from its kernel. The kernel establishes the soundness of
these extensions during Milawa's bootstrapping process.
 Going deeper, we explain how we have shown that the Milawa kernel is sound
using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved
the logic sound, and proved that the source code for the Milawa kernel (1,700
lines of Lisp) faithfully implements this logic.
 Going even further, we have combined these results with the x86
machinecode level verification of the Lisp runtime Jitawa. Our toplevel
theorem states that Milawa can never claim to prove anything that is false when
it is run on this Lisp runtime.
 (See
also Milawa
Documentation and
Jitawa's Website)
2014
 Jared Davis, Anna Slobodova, and Sol Swords. Microcode
Verification—Another Piece of the Microprocessor Verification
Puzzle. Invited
talk, ITP 2014.
Springer, LNCS 8558. July, 2014. Pages 116.
 Official version
(Springer) / Author's preprint
version
 Abstract. Despite significant progress in formal hardware
verification in the past decade, little has been published on the verification
of microcode. Microcode is the heart of every microprocessor and is one of the
most complex parts of the design: it is tightly connected to the huge machine
state, written in an assemblylike language that has no support for data or
control structures, and has little documentation and changing semantics. At the
same time it plays a crucial role in the way the processor works.
 We describe the method of formal microcode verification we have developed
for an x8664 microprocessor designed at Centaur Technology. While the previous
work on high and low level code verification is based on an unverified abstract
machine model, our approach is tightly connected with our effort to verify the
registertransfer level implementation of the hardware. The same microoperation
specifications developed to verify implementation of the execution units are
used to define operational semantics for the microcode verification.
 While the techniques used in the described verification effort are not
inherently new, to our knowledge, our effort is the first interconnection of
hardware and microcode verification in context of an industrial size
design. Both our hardware and microcode verifications are done within the same
verification framework.
 Jared Davis and Matt Kaufmann.
Industrial Strength
Documentation for ACL2.
In ACL2 2014. July,
2014.
EPTCS 152. Pages 925.
 Abstract. The ACL2 theorem prover is a complex system. Its
libraries are vast. Industrial verification efforts may extend this base with
hundreds of thousands of lines of additional modeling tools, specifications,
and proof scripts. High quality documentation is vital for teams that are
working together on projects of this scale. We have developed XDOC, a
flexible, scalable documentation tool for ACL2 that can incorporate the
documentation for ACL2 itself, the Community Books, and an organization's
internal formal verification projects, and which has many features that help to
keep the resulting manuals up to date. Using this tool, we have produced a
comprehensive, publicly available ACL2+Books Manual that brings better
documentation to all ACL2 users. We have also developed an extended manual for
use within Centaur Technology that extends the public manual to cover Centaur's
internal books. We expect that other organizations using ACL2 will wish to
develop similarly extended manuals.
 (See also the ACL2+Books Manual)
 Magnus O. Myreen and Jared Davis.
The reflective Milawa theorem
prover is sound (down to the machine code that runs it)
.
In ITP 2014.
July, 2014. Springer, LNCS 8558. Pages 421436.
 Note: You may prefer the more comprehensive 2015 journal paper of
the same name, see above.
 Abstract.
Milawa is a theorem prover styled after ACL2 but with a
small kernel and a powerful reflection mechanism. We have used the
HOL4 theorem prover to formalize the logic of Milawa, prove the logic
sound, and prove that the source code for the Milawa kernel (2,000 lines
of Lisp) is faithful to the logic. Going further, we have combined these
results with our previous verification of an x86 machinecode implementation
of a Lisp runtime. Our toplevel HOL4 theorem states that when
Milawa is run on top of our verified Lisp, it will only print theorem
statements that are semantically true. We believe that this toplevel
theorem is the most comprehensive formal evidence of a theorem prover's
soundness to date.
 (See also
the Milawa
Documentation and
Jitawa's Website)
 (See
also Slides
from my July 2012 talk at Northeastern University)
2013
 Jared Davis and Sol Swords.
Verified AIG Algorithms in ACL2.
In ACL2 2013. May, 2013.
EPTCS 114. Pages 95110.
 Abstract. AndInverter Graphs (AIGs) are a popular way to represent
Boolean functions (like circuits). AIG simplification algorithms can
dramatically reduce an AIG, and play an important role in modern hardware
verification tools like equivalence checkers. In practice, these tricky
algorithms are implemented with optimized C or C++ routines with no guarantee
of correctness. Meanwhile, many interactive theorem provers can now employ SAT
or SMT solvers to automatically solve finite goals, but no theorem prover makes
use of these advanced, AIGbased approaches.
 We have developed two ways to represent AIGs within the ACL2 theorem
prover. One representation, HonsAIGs, is especially convenient to use and
reason about. The other, Aignet, is the opposite; it is styled after modern
AIG packages and allows for efficient algorithms. We have implemented
functions for converting between these representations, random vector
simulation, conversion to CNF, etc., and developed reasoning strategies for
verifying these algorithms.
 Aside from these contributions towards verifying AIG algorithms, this work
has an immediate, practical benefit for ACL2 users who are using GL to
bitblast finite ACL2 theorems: they can now optionally trust an offtheshelf
SAT solver to carry out the proof, instead of using the builtin BDD package.
Looking to the future, it is a first step toward implementing verified AIG
simplification algorithms that might further improve GL performance.
 Jared Davis.
Embedding ACL2 Models in EndUser Applications.
In DoForm 2013,
AISB 2013, Exeter, UK.
April, 2013. Pages 4956.
 Abstract.
Formal verification, based on mechanical theorem proving, can provide unique
evidence that systems are correct. Unfortunately this promise of correctness
is, for most projects, not enough to justify its high cost. Since formal
models and proof scripts offer few other direct benefits to system developers
and managers, the idea of formal verification is abandoned.
 We have developed a way to embed functions from the ACL2 theorem prover
into software that is written in mainstream programming languages. This lets
us reuse formal ACL2 models to develop applications with features like
graphics, networking, databases, etc. For example, we have written a webbased
tool for hardware designers in Ruby on top of a 100,000+ line ACL2
codebase.
 This is neat: we can reuse the supporting work needed for formal
verification to create tools that are useful beyond the formal verification
team. The value added by these tools will help to justify the investment in
formal verification, and the project as a whole will benefit from the precision
of formal modeling and analysis.
2011
 Sol Swords and Jared Davis.
BitBlasting ACL2 Theorems.
ACL2 2011. November, 2011.
EPTCS 70. Pages 84102.
 Abstract. Interactive theorem proving requires a lot of human
guidance. Proving a property involves (1) figuring out why it holds, then (2)
coaxing the theorem prover into believing it. Both steps can take a long
time. We explain how to use GL, a framework for proving finite ACL2 theorems
with BDD or SATbased reasoning. This approach makes it unnecessary to deeply
understand why a property is true, and automates the process of admitting it as
a theorem. We use GL at Centaur Technology to verify execution units for x86
integer, MMX, SSE, and floatingpoint arithmetic.
 (See also ACL2 '11 Slides)
 Magnus O. Myreen and Jared Davis. A
Verified Runtime for a Verified Theorem Prover. In Interactive Theorem
Proving (ITP 2011).
August, 2011, Nijmegen, The Netherlands. Springer, LNCS 6898. Pages
265280.
 Abstract. Theorem provers, such as ACL2, HOL, Isabelle and
Coq, rely on the correctness of runtime systems for programming languages like
ML, OCaml or Common Lisp. These runtime systems are complex and critical to the
integrity of the theorem provers.
 In this paper, we present a new Lisp runtime which has been formally veried and
can run the Milawa theorem prover. Our runtime consists of 7,500 lines of
machine code and is able to complete a 4 gigabyte Milawa proof effort. When our
runtime is used to carry out Milawa proofs, less unveried code must be trusted
than with any other theorem prover.
 Our runtime includes a justintime compiler, a copying garbage collector,
a parser and a printer, all of which are HOL4veried down to the concrete x86
code. We make heavy use of our previously developed tools for machinecode
verication. This work demonstrates that our approach to machinecode verication
scales to nontrivial applications.
 (See
also Milawa
Documentation and
Jitawa's Website)
 (See also ACL2 '11 Rump Session Slides)
 Anna Slobadova, Jared Davis, Sol Swords, and Warren A Hunt., Jr. A Flexible Formal Verification Framework
for Industrial Scale Validation. Invited talk, Formal Methods and Models for Codesign (MemoCode
2011). July, 2011. Cambridge, UK. Pages 8997.
 Abstract. In recent years, leading microprocessor companies have
made huge investments to improve the reliability of their products. Besides
expanding their validation and CAD tools teams, they have incorporated formal
verification methods into their design flows. Formal verification (FV)
engineers require extensive training, and FV tools from CAD vendors are
expensive. At first glance, it may seem that FV teams are not affordable by
smaller companies. We have not found this to be true. This paper describes the
formal verification framework we have built on top of publiclyavailable
tools. This framework gives us the flexibility to work on myriad different
problems that occur in microprocessor design.
2010

Warren A. Hunt Jr., Sol Swords, Jared Davis, and Anna Slobadova.
Use of Formal Verification at Centaur Technology. In David S. Hardin, editor,
Design
and Verification of Microprocessor Systems for High Assurance Applications.
2010. Springer. Pages 6588.
 Abstract. We have developed a formalmethodsbased hardware
verification toolflow to help ensure the correctness of our X86compatible
microprocessors. Our toolflow uses the ACL2 theoremproving system as a design
database and a verification engine. We verify Verilog designs by first
translating them into a formally defined hardware description language, and
then using a variety of automated verification algorithms controlled by
theoremproving scripts.
 In this chapter, we describe our approach to verifying components of VIA
Centaur's 64bit Nano, X86compatible microprocessor. We have successfully
verified a number of mediaunit operations, such as the packed
addition/subtraction instructions. We have verified the integer multiplication
unit, and we are in the process of verifying microcode sequences that perform
arithmetic operations.
2009

Jared Davis.
A SelfVerifying Theorem Prover.
Ph.D. Dissertation.
The University of Texas at Austin.
December, 2009
 Abstract.Programs have precise semantics, so we can use mathematical
proof to establish their properties. These proofs are often too large to
validate with the usual "social process" of mathematics, so instead we create
and check them with theorem proving software. This software must be advanced
enough to make the proof process tractable, but this very sophistication casts
doubt upon the whole enterprise: who verifies the verifier?
 We begin with a simple proof checker, Level 1, that only accepts proofs
composed of the most primitive steps, like Instantiation and Cut. This program
is so straightforward the ordinary, social process can establish its soundness
and the consistency of the logical theory it implements (so we know theorems
are "always true").
 Next, we develop a series of increasingly capable proof checkers, Level 2,
Level 3, etc. Each new proof checker accepts new kinds of proof steps which
were not accepted in the previous levels. By taking advantage of these new
proof steps, higherlevel proofs can be written more concisely than lowerlevel
proofs, and can take less time to construct and check. Our highestlevel proof
checker, Level 11, can be thought of as a simplified version of the ACL2 or
NQTHM theorem provers. One contribution of this work is to show how such
systems can be verified.
 To establish that the Level 11 proof checker can be trusted, we first use
it, without trusting it, to prove the fidelity of every Level n to Level
1: whenever Level n accepts a proof of some Phi, there exists a Level 1
proof of Phi. We then mechanically translate the Level 11 proof for each Level
n into a Level n  1 proof. That is, we create a Level 1 proof of Level
2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering
shows that each level can be trusted, and allows us to manage the sizes of
these proofs.
 In this way, our system proves its own fidelity, and trusting Level 11 only
requires us to trust Level 1.
 (See
also Milawa
Documentation)
2006

Jared Davis.
Memories: Arraylike Records for ACL2.
In ACL2 2006.
August, 2006, Seattle, WA, USA.
 Abstract. We have written a new records library for
modelling fixedsize arrays and linear memories. Our implementation provides
fixnumoptimized O(log_{2} n) reads and writes from addresses 0,
1, ... , n1. Space is not allocated until locations are used, so large
address spaces can be represented. We do not use singlethreaded objects or
ACL2 arrays, which frees the user from syntactic restrictions and slowarray
warnings. Finally, we can prove the same hypothesisfree rewrite rules found
in misc/records for efficient rewriting during theorem proving.
 (See also Memory Library Documentation)

Jared Davis.
Reasoning about File Input in ACL2.
In ACL2 2006.
August, 2006, Seattle, WA, USA.
 Abstract. We introduce the logical story behind file input
in ACL2 and discuss the types of theorems that can be proven about filereading
operations. We develop a low level library for reasoning about the primitive
input routines. We then develop a representation for Unicode text, and
implement efficient functions to translate our representation to and from the
UTF8 encoding scheme. We introduce an efficient function to read UTF8encoded
files, and prove that when files are well formed, the function produces valid
Unicode text which corresponds to the contents of the file.
 We find exhaustive testing to be a useful technique for proving many theorems
in this work. We show how ACL2 can be directed to prove a theorem by exhaustive
testing.
 (This is now mostly in the ACL2 Std/IO library)
2004

Jared Davis.
Finite Set Theory based on Fully Ordered Lists.
In ACL2 2004.
November, 2004, Austin, TX, USA.
 Abstract. We present a new finite set theory implementation for
ACL2 wherein sets are implemented as fully ordered lists. This order unifies
the notions of set equality and element equality by creating a unique
representation for each set, which in turn enables nested sets to be trivially
supported and eliminates the need for congruence rules.
 We demonstrate that ordered sets can be reasoned about in the traditional
style of membership arguments. Using this technique, we prove the classic
properties of set operations in a natural and effotless manner. We then use the
exciting new MBE feature of ACL2 to provide lineartime implementations of all
basic set operations. These optimizations are made "behind the scenes" and do
not adversely impact reasoning ability.
 We finally develop a framework for reasoning about quantification over set
elements. We also begin to provide common higherorder patterns from functional
programming. The net result is an efficient library that is easy to use and
reason about.
 (This became the ACL2 Std/Osets library)

Gregory L. Wickstrom, Jared Davis, Steve Morrison, Steve Roach, Victor L. Winter.
The SSP: An Example of HighAssurance Systems Engineering.
In HighAssurance Systems Engineering
(HASE 2004).
March, 2004, Tampa, FL, USA. IEEE Computer Society 2004, ISBN 0769520944.
 Abstract. The SSP is a high assurance systems engineering effort
spanning both hardware and software. Extensive design review, first principle
design, nversion programming, program transformation, verification, and
consistency checking are the techniques used to provide assurance in the
correctness of the resulting system.