This talk will describe a DSL for representing the SGX extensions to the Intel Architecture instruction set, the accompanying compiler and some early results of its use. It is hoped that our experience may be of interest to the community and instructive in embedded DSLs. In future we intend to explore repurposing our language for representing other instruction set extensions and reflecting output from the model checkers back into the DSL to better explain traces to the user. The talk will explain these future directions and we are receptive to further ideas from the community.