Projects
The projects directory of the Community Books contains a variety
of projects that have been carried out with ACL2.
Subtopics
- Apt
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- Acre
- ACL2 Centaur Regular Expressions
- Milawa
- Milawa is a "self-verifying" theorem prover for an ACL2-like logic.
- Smtlink
- Tutorial and documentation for the ACL2 book, Smtlink.
- Aleobft
- Formal specification and correctness proofs of AleoBFT.
- Abnf
- A library for ABNF (Augmented Backus-Naur Form).
- Vwsim
- A circuit simulator for rapid, single-flux, quantum
circuits.
- Isar
- An ACL2 library for Isar-style proofs.
- Wp-gen
- An algorithm for generating weakest preconditions as mutually
recursive functions.
- Dimacs-reader
- A reader and parser for satisfiability instances stored in the DIMACS
SAT format.
- Pfcs
- A library for PFCSes (Prime Field Constraint Systems).
- Legacy-defrstobj
- A predecessor of the defrstobj library that wasn't based on
abstract stobjs.
- Proof-checker-array
- Array-based RAT Proof Checker
- Soft
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- Farray
- farray -- A data structure for a field-addressable array.
- Rp-rewriter
- A verified clause-processor and customized rewriter for large terms
that uses existing ACL2 rewrite rules to prove theorems.
- Instant-runoff-voting
- An ACL2 Formalization of an Instant-Runoff Voting Scheme
- Imp-language
- An ACL2 library for the simple programming language Imp.
- Sidekick
- 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.
- Leftist-trees
- An implementation of Leftist Trees.
- C
- An ACL2 library for C.
- Java
- An ACL2 library for Java.
- Taspi
- 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.
- Bitcoin
- A library for Bitcoin.
- Des
- An implementation of the historically significant Data Encription
Standard, an algorithm for encrypting data.
- Ethereum
- A library for Ethereum.
- X86isa
- x86 ISA model and machine-code analysis framework developed
at UT Austin.
- Sha-2
- An implementation of the SHA-2 cryptographic hash
function.
- Yul
- An ACL2 library for Yul.
- Riscv
- A library for RISC-V.
- Zcash
- A library for Zcash.
- Proof-checker-itp13
- RAT Proof Checker for ITP 2013
- Regex
- Regular expression library for ACL2
- ACL2-programming-language
- A library about the ACL2 programming language.
- Json
- A library for JSON.
- Jfkr
- An executable ACL2 model of the JFKr key establishment protocol for
establishing a shared encryption key between two participants.
- Equational
- A modest resolution/paramodulation/factoring/merging prover written
in the Argonne style
with Set-Of-Support, pick-given-ratio, mild term weighting, etc.
- Cryptography
- A library for cryptography.
- Poseidon
- The Poseidon hash function.
- Where-do-i-place-my-book
- How to decide where in the books directory structure to place your book
- Bigmems
- 2^64-byte memory models that are logically a record.
- Builtins
- A library about the ACL2 built-ins.
- Axe
- The Axe toolkit
- Execloader
- Read in some sections of ELF and Mach-O format files into stobjs
- Solidity
- An ACL2 library for Solidity.
- Leo
- An ACL2 library for the Leo language.
- Paco
- Paco is a cut-down, simplified ACL2-like theorem prover for
pedagogical use.
- Concurrent-programs
- ACL2 proofs establishing the fairness of the Bakery Algorithm and the
coherence of the German Cache Protocol.
