The Ethereum Foundation has given $25,097 to The University of Iowa to support the research of Prof. Aaron Stump, Computer Science. A central goal of the Ethereum Foundation is the continued development of the technology underlying Ethereum, the second leading cryptocurrency after bitcoin. Ethereum supports so-called smart contracts, which are essentially programs that can participate in exchange of ether based on some programmed conditions. One serious issue is the possibility of bugs in smart contracts, which in fact led in 2016 to an attack on a decentralized investment fund called the DAO, resulting in the loss of ether equivalent at the time to $70 million. Ethereum Foundation is interested in using Prof. Stump's research on computer-checked proofs of programs, so that smart contracts could come with proofs that they do not exhibit malicious behavior, or satisfy some other desired conditions. Prof. Stump and his students, postdocs, and other collaborators are developing a minimalistic proof language called Cedille, that allows verification for a rich programming language, based on a very small trusted core theory and checker for that theory. The goal is to incorporate Cedille into Ethereum, for smart contract verification.

The gift has already had an impact in the department supporting sending Andrew Marmaduke, a first-year PhD student advised by Stump — and member of the Computational Logic Center — to Devcon 4 in Prague, Czech Republic. Below is an abridged account* of Andrew's feedback from the conference.

"Because I was representing The University of Iowa as a grantee, I also got to sit down in the Grantee Showcase and talk a little bit about Cedille with those who were interested.
To start off, I'll share my first impressions of Devcon4. [...] Prague is a very beautiful city and the conference (held at Prague Conference Centre) was outside of Prague 1 (or the tourist hotspot).

Every day during the conference there was a decompression room where a performer sitting in the center played several ethereal sounding instruments (like chimes, low frequency drums, etc) with a column of lights hanging above her and pillows and comfy carpets surrounding her.

However, the conference also had a distinctly business feel. I've been to my fair share of academic conferences and have attended a developer conference or two before Devcon4, but I've never had an investor ask me for an elevator pitch.
Needless to say, if you're a researcher keen to network inside the blockchain business world then I would wager it's worth your time to attend Devcon5.

Aside from first impressions I arrived at the conference with a particular skepticism about blockchain and the vision of Ethereum. I set a goal for myself to try and resolve that skepticism and to cut through the hype.
I feel like I succeeded.

As one might expect from cryptography, mathematical results that were cast as having essentially no practical applications turned out to have practical applications.

Another interesting project that also happens to be a grantee of the Ethereum Foundation is the Gitcoin project.
Gitcoin is a Dapp (decentralized application built from smart contracts on the Ethereum blockchain) that allows users to post bounties on Github issues for other users to work on and then claim.
In my opinion, Gitcoin is an admirable effort to energize the open source community by changing the story from volunteer passion work to actual work!

Finally, the Solidity team at Ethereum showcased the beginnings of their SMT integration [using, in part, CVC4]. It was encouraging to see a team greasing the gears of automated formal verification in a programming language.

Devcon4 was a lot of fun and there was a lot to discover.
I recommend giving the talks a glance and watching anything you find interesting, there was a lot going on that I missed!"

^{* Head to Prof. Stump's blog entitled "QA9: Exploring the Computational Logic Literature" for the unabridged account.}