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

KEwasm and KWasm





18 DAI
4 contributors

Your contribution goes a long way!

1 DAI contribution

+ 1 DAI match

10 DAI contribution

+ 2 DAI match

100 DAI contribution

+ 5 DAI match

1,000 DAI contribution

+ 8 DAI match

Next update : 1 month, 2 weeks ago | Last updated : 1 month, 2 weeks ago


Eth2.0 Community Education Security


{"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