acl2

Logic and programming language for modeling and verifying computer systems

brewmacoslinux
Try with needOr install directly
Source

About

Logic and programming language in which you can model computer systems

Commands

acl2

Examples

Start the ACL2 interactive REPL for theorem proving$ acl2
Load and certify an ACL2 book/file for verification$ acl2 < myproof.lisp
Run ACL2 in batch mode to process a script$ echo '(defthm my-theorem (equal x x))' | acl2