AuxViom - Auxledger Virtual Machine

Auxviom is a variant of LLVM[3] 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.


[3] C. Lattner and V. Adve, “LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation” 2004.
Link: Link:

Was this article helpful?

Related Articles