pirapira/eth-isabelle
View on GitHub ↗ ★ 245 Isabelle
A Lem formalization of EVM and some Isabelle/HOL proofs
3 mentions on Hacker News by 3 people: 0 stories, 3 comments · first 2017-07-24 · latest 2017-11-09
20082026
-
Formal verification is critical. Projects like this are necessary: https://github.com/pirapira/eth-isabelle Paper: https://yoichihirai.com/malta-paper.pdf
comment by qznc · 2017-11-09 · in The Bitcoin bubble – Greater fool theory -
…allowing non-logicians to put together contracts that mean what they think they mean. See [3]. [1]: https://github.com/pirapira/eth-isabelle [2]: https://github.com/pirapira/ethereum-formal-verification-ove... [3]:…
comment by chalst · 2017-07-25 · in A hacker stole $31M of Ether – how it happened, and what it means for Ethereum -
…See especially his formalization of the EVM as Hoare triples in Lem, which is usable from Isabelle: https://github.com/pirapira/eth-isabelle -- very cool stuff, although I have to say that the ostensible complexity and difficulty of his…
comment by mbrock · 2017-07-24 · in Learn Ethereum smart contract programming