What do you think about Tezos Smart Contracts then?

I've done no research, I don't really know much about the whole... ledgersphere?

Seems like it just puts in a mechanism for changing the protocol without forking the chain, but I'm not sure why people couldn't continue running the old protocol, effectively forking it anyway (other than a "look, we all agreed to no forks, you're explicitly a dick if you fork it, not just someone with a disagreement" angle.)

Oh well I was pointing out to the part where their whole codebase is formally prove, plus their Smart Contract language Michelson is functional and can be used very easily to be formally proven (there by leading to writing more secure smart contracts), since you're earlier concern was security.

I don't see that anywhere, although I only googled very briefly. The closest I saw was this:

> Updates to the protocol can be required to carry formal proofs indicating that they respect agreed core principles agreed upon by the stakeholders.

Which doesn't really make sense; how do you write a formal proof that something align with someone's core principles?