A collection of ACL2 books contributed mainly by Kestrel Institute.
The Kestrel Books are a collection of ACL2 books
contributed mainly by Kestrel Institute. The Kestrel Books are freely available under a liberal license.
Specific copyright, author, and license information
is provided in the individual files and subdirectories.
As they become more stable,
parts of the Kestrel Books may be moved
to other locations in the Community Books. For example, STD and X86ISA include some Kestrel contributions.
Many of the Kestrel Books build upon,
and are meant to extend and be compatible with,
the ACL2 system code
and various existing libraries such as STD, FTY, Seq, and others.
- A hierarchical deterministic wallet for cryptocurrencies.
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- A library of utilities for error checking.
- A library for ABNF (Augmented Backus-Naur Form).
- Extensions of FTY in the Kestrel Books.
- An ACL2 library for Isar-style proofs.
- Utilities that are part of the
- A library for PFCSes (Prime Field Constraint Systems).
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- The BV library for reasoning about bit-vectors
- An ACL2 library for the simple programming language Imp.
- A library of concepts and utilities for event macros.
- A library for Bitcoin.
- A library for Ethereum.
- An ACL2 library for Yul.
- A library for Zcash.
- A library about the ACL2 programming language.
- A library about prime fields.
- An ACL2 library for Java.
- An ACL2 library for C.
- An ACL2 library for the Syntheto language.
- A lightweight library for file input and output.
- Some utilities related to number theory
- A library for cryptography.
- A lightweight library for lists.
- A library for JSON.
- The Axe toolkit
- A library about the ACL2 built-ins.
- An ACL2 library for Solidity.
- Extensions of Std library in the Kestrel Books.
- Tools for finding, improving, and repairing proofs and books.
- HTTP/HTTPS client library
- A lightweight library for lists of items of various types.
- An arithmetic library developed using a lightweight approach