ACL2 Guide to Logic and Programming Language: Proof-automation.

Software verification projects, tools, etc.

Also see the (probably incomplete) page of ACL2-related publications.

Subtopics

Axe

The Axe toolkit

Execloader

Read in some sections of ELF and Mach-O format files into stobjs

Kestrel-books

A collection of ACL2 books contributed mainly by Kestrel Institute.

X86isa

x86 ISA model and machine-code analysis framework developed at UT Austin.