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.
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.)