It can, but it is highly non-trivial. Here are a couple of 2015 papers on OpenSSL verification from the same group at Princeton: SHA verification (ACM TOPLAS):

It can, but it is highly non-trivial. Here are a couple of 2015 papers on OpenSSL verification from the same group at Princeton: SHA verification (ACM TOPLAS): https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf HMAC verification (Usenix Security): http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf