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?

[Abstract to appear]

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.

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.