pirapira

Using my definition of EVM, I think it's already possible to create a small verified compiler.

My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.

There is a similar site [1] without external incentives (actually Proof Market is based on this). This site has active audience posting problems and proofs. Possibly Proof Market ends up in another example of overjustification.

[1] http://as305.dyndns.org/aps/

This gives very broad perspective. I want to cite this comment when I talk about the site. I have never thought about disrupting Wall St, but I do share your pipe dream.

I added risks and complications. A feature called "bounty" is now available. Anyone can add bounty for a problem. The sum goes to the next solver.

I wonder which is easier to encode, natural deduction or Hilbert style.

"admit" does not pass the checker right now. coqchk -o is used to detect those assumptions.

I can mix both approaches. The buyer and other people can stash up bounty, which the first prover gets. I have not implemented this lest "bitcoin stolen from Coq proof exchange".