I'd love to hear more about the process for proposing amendments to the chain. My understanding is that users can propose code changes to the protocol, and receive bounties for these changes.

My specific questions are:

* How are changes actually proposed technically? Do users submit a transaction with their proposed changes, and then other users vote on them? Can anyone submit proposals?

* Is the voting / upgrade process part of the codebase yet, or is that work still coming?

Considering the close ties of OCaml and Coq, has anyone done some sort of formal verification for Tezos ?

The main focus has been on the formal verifiability of smart contracts written in Michelson -- https://www.michelson-lang.com/ I'm checking on Tezos itself.