Trace Abstraction (TA) is a powerful technique for automated program verification, but translating TA proofs into Hoare Logic (HL) proofs remains challenging. This work explores a systematic approach to bridge this gap, enabling the automation of HL proof generation from TA-based verification.