Yoichi Hirai

Yoichi Hirai

Yoichi Hirai

a convenience logician

·

Who can recover stuck funds on Ethereum?

I started reading a pull-request to ethereum/EIPs repository as an EIP editor. The PR soon became a storm, and out I am not an EIP editor…

Feb 15, 2018 · 2 min read

My attitude on protocol changes affecting particular Ethereum accounts

There is an attempt to institutionalize requests to recover lost funds in Ethereum. Before these requests arrive, I should prepare for them…

Feb 3, 2018 · 2 min read

If there is a stuck Ethereum contract

It has been reported that many instances of a multisig wallet got stuck and the contained funds are not accessible. I have not checked…

Nov 14, 2017 · 2 min read

@piraipra’s snapshot post (October 2017)

I write about what I’m doing currently for Ethereum, and why.

Oct 23, 2017 · 3 min read

Don’t get those tokens unless the tokens need you

Tokens are blockchains’ way of controlling people. Bitcoin and Eth make people mine. When Casper comes in, Eth will make people vote on…

Oct 20, 2017 · 2 min read

Implementing a vault in Bamboo

I saw vault.sol. It’s about protecting ETH against a stolen private key. A vault key and a recover key are involved. When the vault key is…

Oct 19, 2017 · 4 min read

What I think about what KEVM people think about EVM

I stumbled upon an interesting document by the KEVM project. The KEVM project is an attempt at defining the Ethereum Virtual Machine, whose…

Aug 2, 2017 · 2 min read

Empty this Ethereum contract on Ropsten written in Bamboo!

I have been developing Bamboo, a programming language for Ethereum contracts. It is super-immature. Every time I write a new contract, I…

Jul 26, 2017 · 2 min read

Bamboo compiler started producing EVM bytecode

It’s been nine months since I started working on the Bamboo compiler. There was a long dormant period, but this week the compiler started…

Jun 27, 2017 · 3 min read

Impressions on Metropolis

Sometimes I’m asked about the Metropolis release. The list of Metropolis EIPs looks stable already. I’m sharing how I read them, but I’m…

Jun 1, 2017 · 6 min read

What happens when Metropolis EIPs change

I’ve been attending recent Ethereum all-core-dev meetings. These were mainly about the next change in the Ethereum protocol called…

May 26, 2017 · 5 min read

What I do for Ethereum when I’m not writing blogs

On Medium, I posted some blogs about verifying Ethereum contracts or proving PoS slashing conditions correct. These efforts are easily…

May 9, 2017 · 2 min read

Ten Ethereum-Related Projects You could Take

During the half year in the Ethereum space, I accumulated some nice-to-do projects. I usually put them aside and instead work on existing…

Apr 27, 2017 · 4 min read

FC 2017 Report & Is there a Mechanism Designer Aboard?

I attended a conference “Financial Cryptography and Data Security 2017”. It had a mixture of cryptographers and blockchain people (with a…

Apr 10, 2017 · 3 min read

Formal methods on another Casper

In a previous post, I talked about proving properties of Vitalik’s Casper. This post is about Vlad’s Casper. They are very different. The…

Mar 9, 2017 · 13 min read

Ethereum Virtual Machine for Coq (v0.0.2)

Here is the version 0.0.2 of eth-isabelle project. Now it can produce a Coq definition of the Ethereum Virtual Machine. The project…

Mar 5, 2017 · 2 min read

1,000 Ether bounty on a proven-correct wallet (with 17 instructions, just a beginning)

In the EDCON conference in Paris, I will talk about proving smart contracts correct. There I will release a bounty program. For everybody…

Feb 17, 2017 · 2 min read

Hoare Logics for Ethereum Virtual Machine

This time I’m not announcing a release, or publishing a verification result of Ethereum smart contracts. This post is just a progress…

Jan 16, 2017 · 4 min read

Measuring the VM Test’s Coverage with the Lem Model

I wanted to prove and deploy smart contracts that never break. So I implemented the Ethereum Virtual Machine (EVM) for interactive theorem…

Jan 6, 2017 · 2 min read

Ethereum Virtual Machine for interactive theorem provers (version 0.0.1)

I announce the version 0.0.1 of eth-isabelle project: a formalization of Ethereum Virtual Machine (EVM) for interactive theorem provers.

Jan 5, 2017 · 1 min read