Comment by jeff-davis

Note that there are quite a few ways that crypto implementations can be insecure even if it's proven to be "correct" (in terms of inputs and outputs). For instance, it may leak information through timing, or by failing to clear sensitive memory due to a compiler optimization.