Auxviom is a variant of LLVM specialized to execute smart contracts on the blockchain. Its design, definition and implementation has been executed at the highest mathematical standards, following a semantics-first approach with verification of smart contracts as the main objective. Specifically, we have defined the formal syntax and semantics of Auxviom using the K framework, which in return gives us an executable reference model in addition to a series of program analysis tools, including a program verifier.
Unlike the stack based Ethereum Virtual Machine, Auxviom is proposed to be designed as a register-based machine similar to LLVM. Auxviom not only has an unbounded number of registers but also supports unbounded integers.
 C. Lattner and V. Adve, “LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation” 2004.
Link: Link: http://llvm.org/pubs/2004-01-30-CGO-LLVM.pdf