I present the results of constructing a fully untrusted verifier for memory safety of Typed Assembly Language programs, using the Open Verifier architecture. The verifier is untrusted in the sense that its soundness depends only on axioms about the semantics of a concrete machine architecture, not on any axioms specific to a type system. This experiment served to evaluate both the expressiveness of the Open Verifier architecture and the quality of its support for simplifying the construction of verifiers. I discuss issues of proof generation that are generally not the focus of previous efforts for foundational checking of TAL, and I contrast with these past approaches the sort of logical formalization that is natural in the context of the Open Verifier. My approach is novel in that it uses direct reasoning about concrete machine states where past approaches have formalized typed abstract machines and proved their correspondence with concrete machines. I also describe a new approach to modeling higher-order functions that uses only first-order logic.