ACL2 Workshop 2025
Abstracts

Formal methods for system engineering have traditionally faced two fundamental barriers to adoption: formal specifications are hard to write, and formal proofs are hard to automate at scale. In this talk, I will argue that recent progress in machine learning offers a historic opportunity to overcome these problems. Specifically, I will summarize recent progress in the emerging field of AI for formal mathematics, including developments in automatic formalization, proof synthesis, and the acceleration of formal reasoning with informal methods. I will show that these techniques have immediate applications in software and hardware verification and that conversely, formal system engineering tasks raise interesting foundational questions in AI for math. I will end the talk by highlighting some productive ways in which the formal methods and AI communities can work together in this research area.

Bio: Swarat Chaudhuri (http://www.cs.utexas.edu/~swarat) is a Professor of Computer Science at UT Austin and a Research Scientist at Google Deepmind. He is known for his work at the interface of machine learning and automated reasoning, including program synthesis, neurosymbolic reasoning, and certified learning. Prof. Chaudhuri has received the NSF CAREER award, the ACM SIGPLAN John Reynolds Dissertation award, Meta and Google Research awards, several ACM SIGPLAN and SIGSOFT distinguished paper awards, and an Op-Ed Project Fellowship. He has served on the program committees of most of the prominent venues in formal methods, machine learning, and programming languages and has been a Program Chair for the CAV and ICLR conferences.

We will summarize the use of ACL2. We wish to have a discussion about the present and future use of ACL2. This discussion will concern (at least) the following questions.

• Who will use ACL2 in education about reasoning and formal methods?
• What could we do to expand the usage of ACL2?
• What should be the ACL2 business model? That is, how should ACL2 be enhanced and maintained after the original authors retire?
• Do you see yourself using ACL2 in 5 or 10 years?
• Should we have another ACL2 Workshop?

[Slides]

We present a formalization in ACL2(r) of the Wallis Product Formula for pi. This beautiful formula is a key step in a larger (in progress) formalization of Stirling's approximation to n!.

[Slides]

For my senior research project I am writing a verified translator from a simple expression language with binding to SAT. In the talk I will discuss my approach to verification, and my experience using ACL2 as a novice.

[Slides]

There is a lot of interest (and hype) surrounding quantum computing. This talk will discuss some of the fundamental capabilities of quantum computing and highlight some parallels between those capabilities and symbolic logic.

[Slides]

This talk will present a work-in-progress library for fast finite sets and maps. The goal of the library is to provide similar interfaces as the osets and omaps libraries but with a more efficient, tree-based data structure. Two partial implementations, at different levels of completeness, will be presented -- the first, based on "treaps" with a hash-based heap order; and the second, based on little-endian patricia trees.

[Slides]

This talk will summarize work to date on enabling the use of ACL2 to prove theorems of ZFC set theory, with applications to reasoning about notions typically considered "higher-order". This work resides in the community books directory books/projects/set-theory/ and is documented in topics ZFC and ZFC-MODEL.

[Slides]

We report on preliminary work on translating HOL4 definitions into ACL2. This work takes advantage of a recent integration of set theory with ACL2. This work may provide a key step towards being able to reason about HOL4 and ACL2 formalizations in a common ACL2 environment.

[Slides]

How will today's large language models do in a freshman-level class? We evaluate Google, OpenAI, and Anthropic's most capable, publicly available models on two exams and a homework from Northeastern's 2024 logic and computation course, taught using the ACL2s theorem prover. The models score close to the mean student on exams, but do poorly on a homework about proving function termination. In this presentation, we'll discuss the model's successes and shortcomings, and directions for future work using LLMs for theorem proving in ACL2s.

[Slides]

With the race to build large-scale quantum computers and efforts to exploit quantum algorithms for efficient problem solving in science and engineering disciplines, the requirement to have efficient and scalable verification methods are of vital importance. A novel formal verification method that is targeted at Quantum Fourier Transform (QFT) circuits is proposed. Quantum Fourier Transform is a fundamental quantum algorithm that forms the basis of many quantum computing applications. The verification method employs abstractions of quantum gates used in QFT that leads to a reduction of the verification problem from Hilbert space to the quantifier free logic of bit-vectors. Very efficient decision procedures are available to reason about bit-vectors. Therefore, this method is able to scale up to the verification of QFT circuits with 10,000 qubits and 50 million quantum gates. A generalization of this abstraction to other quantum algorithms however causes reduction in scaling. Many quantum functions are very symmetric. We are therefore working on using ACL2 to develop verified generators for such functions.

[Slides (pdf)]

[Slides (pptx)]

We have partially specified the x86 ISA in ACL2, allowing for the formal verification of x86 programs in the ACL2 theorem prover at the machine code level. This specification is complete enough to boot Linux and run many user programs. Our model is executable, and we apply co-simulation to validate its correctness. Using the model and the large library of lemmas that have been proven about it, multiple programs have been verified, including a Unix style `wc` word count program and a supervisor program that modifies the page tables to move data in the virtual address space. We hope this is a step to towards greater use of formal methods in the verification of software.

[Slides]