My assumption would be that the main difference is the formal proof, and whatever changes were necessary in order to permit formal verification (i.e. they may h

My assumption would be that the main difference is the formal proof, and whatever changes were necessary in order to permit formal verification (i.e. they may have changed behaviour in order to make the implementation actually meet the abstract specification). But I agree it would be very interesting to find out what the differences are, and whether substantial changes were required in order to do this kind of formal verification.