QZqznc·Nov 9, 2017
Formal verification is critical. Projects like this are necessary: https://github.com/pirapira/eth-isabelle
Paper: https://yoichihirai.com/malta-paper.pdf
In The Bitcoin bubble – Greater fool theorypirapira
eth-isabelle
Isabelle2017–2017
pirapira / eth-isabelle
eth-isabelle
A Lem formalization of EVM and some Isabelle/HOL proofs
3Distinct people
3Mentions
0Explicit recommenders
245GitHub stars
What to know before exploring
What it is
A Lem formalization of EVM and some Isabelle/HOL proofs
GitHub
Where it is used
No documented product use has been verified yet.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
- pirapira/ethereum-formal-verification-overview · linked in 2 of the same discussions
Mentioned in the same Hacker News threads. That is not proof they are substitutes.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 5:04:57 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by week3 dated mentions
Observed mentions: 2017-07-24 16:39:25 UTC to 2017-11-09 15:03:57 UTC. Weeks start Monday, UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| Jul 24 | 2017-07-24 00:00:00 UTC | 2017-07-31 00:00:00 UTC | 2 | 0 | 2 |
| Jul 31 | 2017-07-31 00:00:00 UTC | 2017-08-07 00:00:00 UTC | 0 | 0 | 0 |
| Aug 7 | 2017-08-07 00:00:00 UTC | 2017-08-14 00:00:00 UTC | 0 | 0 | 0 |
| Aug 14 | 2017-08-14 00:00:00 UTC | 2017-08-21 00:00:00 UTC | 0 | 0 | 0 |
| Aug 21 | 2017-08-21 00:00:00 UTC | 2017-08-28 00:00:00 UTC | 0 | 0 | 0 |
| Aug 28 | 2017-08-28 00:00:00 UTC | 2017-09-04 00:00:00 UTC | 0 | 0 | 0 |
| Sep 4 | 2017-09-04 00:00:00 UTC | 2017-09-11 00:00:00 UTC | 0 | 0 | 0 |
| Sep 11 | 2017-09-11 00:00:00 UTC | 2017-09-18 00:00:00 UTC | 0 | 0 | 0 |
| Sep 18 | 2017-09-18 00:00:00 UTC | 2017-09-25 00:00:00 UTC | 0 | 0 | 0 |
| Sep 25 | 2017-09-25 00:00:00 UTC | 2017-10-02 00:00:00 UTC | 0 | 0 | 0 |
| Oct 2 | 2017-10-02 00:00:00 UTC | 2017-10-09 00:00:00 UTC | 0 | 0 | 0 |
| Oct 9 | 2017-10-09 00:00:00 UTC | 2017-10-16 00:00:00 UTC | 0 | 0 | 0 |
| Oct 16 | 2017-10-16 00:00:00 UTC | 2017-10-23 00:00:00 UTC | 0 | 0 | 0 |
| Oct 23 | 2017-10-23 00:00:00 UTC | 2017-10-30 00:00:00 UTC | 0 | 0 | 0 |
| Oct 30 | 2017-10-30 00:00:00 UTC | 2017-11-06 00:00:00 UTC | 0 | 0 | 0 |
| Nov 6 | 2017-11-06 00:00:00 UTC | 2017-11-13 00:00:00 UTC | 1 | 0 | 1 |
What Hacker News says
3 sourcesThe specification of EVM in HOL exists already [1] and can be used to prove correctness of EVM code already. EVM is pretty low-level, though; the same can't be done for Solidity code. Yoichi has a page that outlines his thinking about what Ethereum's formal verification needs are [2].
What I would like to see is a verified high-level smart contract language layered on top of the Ethereum stack, 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]: http://lambda-the-ultimate.org/node/5003#comment-94645
In A hacker stole $31M of Ether – how it happened, and what it means for EthereumSome pointers you might appreciate:
Jack Petterson and Robert Edström did a master's thesis about retargeting the Idris compiler to emit EVM code, with a custom effect type to express smart contract effects. They ended up modestly skeptical of functional programming as a paradigm for EVM, instead looking toward process calculi. https://publications.lib.chalmers.se/records/fulltext/234939...
Yoichi Hirai's summary of his research into Ethereum formal verification as a full-time formal methods researcher at the Foundation: https://github.com/pirapira/ethereum-formal-verification-ove...
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 proof verifying an utt
Read the rest
erly simple wallet contract makes me a bit skeptical of this approach to smart contract correctness: https://github.com/pirapira/eth-isabelle/blob/master/example...