AuxViom – Auxledger Virtual Machine

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

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

Was this article helpful?

Related Articles