This formal verification walkthrough goes through the hows and whys of a recent project with Amazon that may have some answers for you. Obviously a different project but the fundamentals are similar https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ (I work at Galois)