1. Overview

This library provides a complete x86-32 macro assembler implemented in Lean 4, leveraging dependent types for type-safe instruction encoding and assembly.

1. 1.1. Why a Verified Assembler?
2. 1.2. Key Features
3. 1.3. Design Philosophy