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