The Coq mailing list

[Arthur Breitman <arthurb AT tezos.com>]

I posted a similar message on the OCaml mailing list (which probably intersects with this list quite a bit), but I wanted to reach out specifically to the Coq community. Apologies if you've read this already.

I'm working on Tezos, a project for a blockchain (in the same vein as Bitcoin or Ethereum) written entirely in OCaml, from scratch.

Tezos is a self-amending ledger. While other protocols achieve consensus about the state of their transactions, Tezos reaches a meta-consensus about its own protocol. This allows us to gradually build governance rules into the ledger by letting the participants choose under which condition the protocol may be amended.

We start with a simple voting procedure to accept or reject a proposed patch to a set of OCaml modules representing the protocol. Over time, complex rules can evolve. Of particular interest would be to introduce a form of constitutionalism by having the protocol require and enforce that any proposed modification be formally verified and guaranteed to preserve specific properties. This could be achieved by including a proof checker withing the protocol.

As a less ambitious first step, we'd like to build a formalization of our smart-contract language in Coq. We're aware of ongoing efforts to do this with the Ethereum virtual machine, but unlike the EVM, our smart contract language has a clear specification,  is generally pure, and is statically & strongly typed. This should make the process more pleasant.

We'd also be interested in proving certain parts of the code base correct, either by extracting them from a Coq implementation or directly with CFML.  

If you find this intriguing and enjoy working with Coq, please reach out, we'd like to sponsor research on the topic (within our modest means).

Best,

Arthur