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
|
| 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 |
| Sep 11, 2024 8:01am |
|
21 |
VERSION_BUMP |
3fd08f7e |
| May 1, 2024 10:19am |
|
17 |
VERSION_BUMP |
df983dec |
| Jan 28, 2024 8:56pm |
|
15 |
VERSION_BUMP |
a0b0d6aa |
| Jan 28, 2024 12:21pm |
|
15 |
VERSION_BUMP |
639bb432 |
| Dec 29, 2023 3:09am |
|
14 |
VERSION_BUMP |
9d3b65ed |
| Dec 24, 2023 6:52pm |
|
13 |
VERSION_BUMP |
5d0c8756 |
| Oct 22, 2023 11:44am |
|
11 |
VERSION_BUMP |
f4dfc5ce |
| May 1, 2023 12:37pm |
|
9 |
VERSION_BUMP |
22efd5df |
| Mar 29, 2023 1:37am |
|
8 |
VERSION_BUMP |
91f545d3 |
| Feb 27, 2023 12:32am |
|
7 |
VERSION_BUMP |
e97171a2 |
| Jan 29, 2023 5:12am |
|
6 |
VERSION_BUMP |
96ceb58d |
| Jan 29, 2023 5:12am |
|
6 |
VERSION_BUMP |
593c3c37 |
| Dec 29, 2022 11:54pm |
|
5 |
VERSION_BUMP |
9cded52e |
| Dec 29, 2022 11:54pm |
|
5 |
VERSION_BUMP |
e9804bb1 |
|