This manual provides an introduction to Dracula, the programming environment for the ACL2 theorem prover in DrScheme. See section 1 for instructions on installing, upgrading, and uninstalling Dracula. See section 2 for a tutorial on running and verifying programs using Dracula and ACL2. Section 3 introduces DoubleCheck, the teachpack for using automated testing to check your conjectures. Section 4 introduces Modular ACL2, an extension of ACL2 that supports systematic, piece-by-piece development and verification of ACL2 proofs.