The projects directory of the Community Books contains a variety
of projects that have been carried out with ACL2.
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- ACL2 Centaur Regular Expressions
- Milawa is a "self-verifying" theorem prover for an ACL2-like logic.
- Tutorial and documentation for the ACL2 book, Smtlink.
- A library for ABNF (Augmented Backus-Naur Form).
- A circuit simulator for rapid, single-flux, quantum
- An ACL2 library for Isar-style proofs.
- An algorithm for generating weakest preconditions as mutually
- A reader and parser for satisfiability instances stored in the DIMACS
- A library for PFCSes (Prime Field Constraint Systems).
- A predecessor of the defrstobj library that wasn't based on
- Array-based RAT Proof Checker
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- farray -- A data structure for a field-addressable array.
- A verified clause-processor and customized rewriter for large terms
that uses existing ACL2 rewrite rules to prove theorems.
- An ACL2 Formalization of an Instant-Runoff Voting Scheme
- An ACL2 library for the simple programming language Imp.
- The ACL2 Sidekick is a graphical add-on for ACL2. It extends your
ACL2 session with a web server so that you can interact with ACL2 through your
browser. You use the Sidekick along with—not instead of—Emacs or
your favorite ACL2 development environment.
- An implementation of Leftist Trees.
- Texas Analysis of Symbolic Phylogenetic Information (TASPI) is
specialized code for modeling collections of phylogenetic trees and performing
a few manipulations such as consensus analysis.
- A library for Bitcoin.
- An implementation of the historically significant Data Encription
Standard, an algorithm for encrypting data.
- A library for Ethereum.
- An implementation of the SHA-2 cryptographic hash
- An ACL2 library for Yul.
- A library for Zcash.
- RAT Proof Checker for ITP 2013
- A 2^64-byte memory model that is logically a record but
provides array-like performance during execution
- Regular expression library for ACL2
- A library about the ACL2 programming language.
- An ACL2 library for Java.
- An ACL2 library for C.
- An executable ACL2 model of the JFKr key establishment protocol for
establishing a shared encryption key between two participants.
- x86 ISA model and machine-code analysis framework developed
at UT Austin
- A modest resolution/paramodulation/factoring/merging prover written
in the Argonne style
with Set-Of-Support, pick-given-ratio, mild term weighting, etc.
- A library for cryptography.
- How to decide where in the books directory structure to place your book
- A library for JSON.
- A library about the ACL2 built-ins.
- Read in some sections of ELF and Mach-O format files into stobjs
- An ACL2 library for Solidity.
- Paco is a cut-down, simplified ACL2-like theorem prover for
- ACL2 proofs establishing the fairness of the Bakery Algorithm and the
coherence of the German Cache Protocol.