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