ACL2 (R1CS and PFCS books): Mature prime-field constraint verification with light tactics
================================================================================

ACL2 has a mature library for R1CS and prime-field constraint systems and an acl2-jolt project. zkSecurity's 2025 comparison found it the lightest on tactic effort among circuit frameworks, at the cost of a smaller ecosystem.

Maintainer: ACL2 community (Kestrel Institute)
Website: https://www.cs.utexas.edu/~moore/acl2/
Category: Proof assistants and general verifiers
Targets: R1CS, Prime-field constraint systems, acl2-jolt
Approach: First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits
Access: Open source (BSD)
Status: Mature, niche
Strengths: Least proof effort per gadget in published comparisons. | Long history in hardware verification.
Limits: Small ZK community. | First-order logic limits expressiveness. | Less interoperability with Lean projects.
Firms using it: none listed
Sources: https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

Source page: https://sorryfree.com/frameworks/acl2/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13