acl2 ☆
« Back to VersTracker
Description:
Logic and programming language in which you can model computer systems
Type: Formula  |  Latest Version: 8.6@13  |  Tracked Since: Dec 17, 2025
Links: Homepage  |  formulae.brew.sh
Category: Developer tools
Tags: theorem-prover formal-verification logic lisp programming-language
Install: brew install acl2
About:
ACL2 is a theorem prover and a programming language designed for automated reasoning about software and hardware systems. It combines a functional programming language with a logical framework, enabling users to define models and rigorously prove their correctness. This tool is particularly valuable for verifying the reliability of critical systems.
Key Features:
  • Interactive theorem proving environment
  • Applicative subset of Common Lisp
  • Automated proof strategies and rewriting
  • Supports both logic and programming
Use Cases:
  • Verifying correctness of microprocessor designs
  • Proving theorems about software algorithms
  • Automated reasoning for security protocols
Alternatives:
  • Coq – Coq is based on dependent type theory, while ACL2 uses a first-order logic and a subset of Lisp.
  • Isabelle/HOL – Isabelle/HOL is another interactive theorem prover, but with a higher-order logic foundation.
License: BSD-3-Clause
Dependencies: sbcl
Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, sonoma, x86_64_linux
Version History
Detected Version Rev Change Commit
Oct 27, 2025 9:49pm 13 VERSION_BUMP d4901f67
Sep 13, 2025 9:48am 11 VERSION_BUMP 7e78c832
Dec 29, 2024 9:23pm 3 VERSION_BUMP 2b1e8cd6
Dec 29, 2024 3:40pm 3 VERSION_BUMP 02ecfa9c
Oct 31, 2024 5:14am 1 VERSION_BUMP 294fff00
Oct 3, 2024 4:31am 22 VERSION_BUMP 7926f755
« Back to VersTracker  |  Browse Packages  |  About