While the prominent quantum computing architectures are based on superconducting technology, new quantum hardware technologies are emerging, such as Trapped Ions, Neutral Atoms (or FPQAs), Silicon Spin Qubits, etc. This diverse set of technologies presents fundamental trade-offs in terms of scalability, fidelity, manufacturing, and operating expenses. To manage these diverse quantum technologies, there is a growing need for a \textit{retargetable compiler} that can efficiently adapt existing code to these emerging hardware platforms. Such a retargetable compiler must be \textit{extensible} to support new and rapidly evolving technologies, \textit{performant} with fast compilation times and hardware-specific optimizations, and verifiable through rigorous equivalence checking to ensure the functional \textit{equivalence} of the retargeted code.

To this end, we present \textit{Weaver}, the first extensible, performant, and verifiable retargetable quantum compiler framework with a focus on FPQAs due to their unique, promising features. \textit{Weaver} introduces \textit{WQASM}, the first formal extension of the standard OpenQASM quantum assembly with FPQA-specific instructions to support their distinct capabilities. Next, \textit{Weaver} implements the \textit{WOptimizer}, an extensible set of FPQA-specific optimization passes to improve execution quality. Last, the \textit{WChecker} automatically checks for equivalence between the original and the retargeted code. Our evaluation shows that \textit{Weaver} improves compilation times by $10^3\times$, execution times by $4.4\times$, and execution quality by $10%$, on average, compared to superconducting and state-of-the-art (non-retargetable) FPQA compilers.