I'm currently reading some literature about verification of smart contracts. One of the papers I read is Defining the Ethereum Virtual Machine for Interactive Theorem Provers by Hirai (pirapira). In the considerations around solidity (Section 2.1) he states that:

Solidity has a reach syntax but no specification. The only definition of Solidity is the Solidity compiler implementation.

I am wondering if it is still so or something has changed in the meantime.

P.S. I see that the team of kframework has begun to define the semantics of solidity with K Framework

1 Answer 1


The semantics of Solidity change with every update, and the only canonical definition is the compiler itself. Note that there is a distinction between the intended behavior of the compiler and the actual behavior, which sometimes leads to compiler bugs. Maybe then it is more accurate to say that the (informal) definition of the solidity semantics is in the docs.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.