Verify HMAC tag without knowing the key

Let's say there's Alice and Bob.

1. Let Alice and Bob agree on a message $M_1$, a tag $T_1$, and a function $HMAC$.
2. Alice proves to Bob that she knows a key $K$ such that $T_1 = HMAC(M_1, K)$ without revealing what $K$ is, using a zero knowledge proof.
3. Alice sends Bob some cryptographic object $MysteryBox$.
4. Alice dies.
5. When Bob puts $M_2$ and $T_2$, which Alice doesn't know, into $MysteryBox$ she left, he can decide if $T_2 \stackrel{?}{=} HMAC(M_2, K)$, without knowing what $K$ is.

Can we design such $MysteryBox$, without using truly homomorphic encryption?

There are obviously constructions other than HMAC that work. Public key signing works obviously with Alice sending Bob her public key.

HMAC has no algebraic structure to allow this to work. Zero knowledge proofs for knowing a (m,MAC,k_MAC) triple use arbitrary circuits and require a prover who knows k_MAC.

To do what you're asking, you'll need indistinguishably obfuscation. This is a technique to obfuscate an arbitrary program in a cryptographically secure way. Then just write the MAC verification function Verify(m,mac)-->{True,False} for a fixed key and run it through the obfuscation scheme.

To quote the wikipedia article:

Currently known indistinguishability obfuscation candidates are very far from being practical. As measured by a 2017 paper[needs update], even obfuscating the toy function which outputs the logical conjunction of its thirty-two Boolean data type inputs produces a program nearly a dozen gigabytes large.

AFAIK it's still not really practical.