The "harvest now, decrypt later" (HNDL) problem is closer than it seems. Take a quick dive into PQ-safe alternatives, find out why discovery and spending are separate problems to solve. And how to verify these claims using Lean 4 and VCVio!