Ethereum

78 readers

1 users here now

Welcome to c/ethereum, the real front page of web3.

Rules:

No inappropriate behavior. This includes, but is not limited to: personal attacks, threats of violence, gossip, slurs of any kind, posting people's private information.
No duplicate threads.
No spamming or drive by posting.
No misleading titles.

founded 1 year ago

MODERATORS

[email protected]

Formal Verification for n00bs — Part 1: The K ecosystem (medium.com)

submitted 1 year ago* (last edited 1 year ago) by [email protected] to c/[email protected]

0 comments fedilink hide all child comments

Part 2

Part 3

Part 4

The motivation for Formal Verification Security of smart contracts is still a crucial challenge: we all remember the DAO, parity hacks, a bunch of smaller attacks and the most recent delayed hard fork. We would like to see the future in which we can be way more confident about our code.

Depending how you count, event over a half a billion dollars (by today’s Ethereum evaluation), was lost in a couple of biggest smart contract hacks.

What about if behind every responsible piece of code stands pure solid mathematics instead of personal conviction of developers? With formal verification tools for Ethereum finally maturing, it is now not only possible but also practical.

In this and following post we will be getting step by step into the world of K-framework, which allows to formally verify EVM smart contracts.

no comments (yet)

sorted by: hot top controversial new old

there doesn't seem to be anything here