With the formalized semantics of the EVM in the K framework (the Jello paper), a new arsenal of analysis tools has become available for Ethereum smart contract development. This workshop will demonstrate how this tooling can be used to verify the complete behavior of smart contracts, sharing the techniques and tools used to verify the core contracts of multicollateral dai.
We will demonstrate the power of formal verification by presenting the Ethereum community with two challenges:
In the first one, we invite the workshop participants to a round of formally verified EVM golf. The most gas efficient implementation of an ERC20 contract which provably matches the specification wins!
In the second challenge, the task is to challenge the specification itself, by writing a passing adversarial smart contract. In this ""reverse bug bounty"", participants are invited to poke holes in a specification by writing smart contracts which satisfy the postulated requirements but are otherwise faulty in some way.
Creating an account on our site will allow you to customize your news stream and unlock additional functionalities!
The primary benefit of registring an account is that will give you the ability to customize your news feed and
select the sources from which your news are displayed.
In addition to this, registered users can
'Like' specific news items, thus showing their support and appreciation for the item
Comment on news items and rate comments
Propose new 'tags' on news items to improve searchability
The ability to engage in all of these actions is driven by a site-specific internal virtual currency
which we call Kreds. In order to encourage our users to use their moderation and
participation abilities responsibly, each action you perform will cost you a certain amount of Kreds.
You are automatically awarded a certain amount of Kreds every day and can earn Kreds by leaving comments
or propose tags which the community then approves through the on-site voting capabilities.
You have to be logged in to vote up news.
You don't have enough Kreds to execute this action.