@GrapheneOS Does it still apply to MTProto 2.0?
https://en.wikipedia.org/wiki/Telegram_(software)#Privacy
I do not consider Telegram to be a good solution for private communication. it seems that they can still have copies of encrypted and unencrypted messages on the server and the server decides on the encryption parameters.
@ruza Yes, it does. Also, proving code correct simply shows it matches a specification. It doesn't mean it's secure. Code that's proven correct can still have bugs both since the specification can have bugs and proving it correct can have bugs.