Auxviom is a variant of LLVM specialized to execute smart contracts on the blockchain. Its design, definition and implementation have been done at the highest mathematical standards, following a semantics-first approach with verification of smart contracts as a major 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 Ethereum Virtual Machine, which is a stack-based machine, Auxviom is proposed to be designed as register-based machine, like LLVM. It has an unbounded number of registers and 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