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.
- A library of utilities for error checking.
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- An ACL2 library for Isar-style proofs.
- Utilities that are part of the
- Extensions of FTY in the Kestrel Books.
- A library for ABNF (Augmented Backus-Naur Form).
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- A library for PFCS (Prime Field Constraint Systems).
- 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 Ethereum.
- A library for Bitcoin.
- 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.
- A library for cryptography.
- An ACL2 library for C.
- A lightweight library for lists.
- Some utilities related to number theory
- A lightweight library for file input and output.
- A library for JSON.
- An ACL2 library for Solidity.
- The Axe toolkit
- Extensions of Std library in the Kestrel Books.
- A lightweight library for lists of items of various types.
- An arithmetic library developed using a lightweight approach