×
Grow Open Source Bounties Hackathons Grants Quests Kudos
Back to Grants

CATEGORIES

Eth2.0 Community Education Security

MATCH ROUND 6

0 DAI

MATCH ESTIMATE

ROUND

5 DAI
1 contributors

Description

{"ops":[{"insert":"We are building KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0, written in the K framework.\n\nK tools blur the line between specification and implementation. The code is human-readable and a great reference for understanding Wasm and Ewasm, but it also generates a correct-by-construction interpreter.\n\nWe want Ewasm to have a specification that you can run your smart-contract with.\n\nWe have a prototype implementation of Ewasm that we have began using to verify an Ewasm contract with, "},{"attributes":{"link":"https://medium.com/@rv_inc/verifying-ethereum-flavored-wasm-ewasm-code-de91ab3179be"},"insert":"which we are blogging about"},{"insert":".\n\nIt is still early days, and right now we want to ramp up and make the prover more powerful, and the tools more accessible for early adopters.\n\nIn the next three months we want to get KWasm battle-ready. That includes:\nVerifying a prototype smart contract."},{"attributes":{"list":"bullet"},"insert":"\n"},{"insert":"Doing some major refactoring for readability and speed."},{"attributes":{"list":"bullet"},"insert":"\n"},{"insert":"Making educational material in the form of blog posts and webcasts on how to formally verify contracts."},{"attributes":{"list":"bullet"},"insert":"\n"},{"insert":"\nWho are we?"},{"attributes":{"header":1},"insert":"\n"},{"insert":"We are RV, Inc. We are the formal verification specialists behind KEVM which we use to verify Uniswap, DAI, the Ethereum 2.0 deposit contract, to name a few.\n\nKWasm, KEwasm, KEVM and the K framework itself are all "},{"attributes":{"link":"https://github.com/kframework/"},"insert":"completely open source"},{"insert":".\n"}]}

Activity Feed