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