Abstract: Search tree algorithms are widely used in areas such as database indexing, compiler design, and file systems, where the functional correctness of these algorithms is a critical factor in ensuring software reliability. However, traditional development process face two major challenges: first, algorithm design often lacks rigorous mathematical modeling, causing correctness verification to remain at an empirical level; second, existing verification approaches heavily rely on manual or interactive theorem proving, making the verification complexity grow exponentially with increasing algorithm scale. To address the above issues, an Isabelle-driven method for modeling and automated verification of search tree algorithms is proposed, This method builds on a formally verified functional modeling library to construct a modular modeling strategy that supports various search tree structures, and introduces a formal specification–driven framework for automatically synthesizing algorithmic code. Developers are required to supply only minimal functional expressions to complete the implementation. In addition, a reusable lemma library has been developed to support an automated block-wise verification strategy, significantly reducing verification costs. Furthermore, a method for generating functional executable programs is proposed. Experimental evaluation using a representative case study demonstrates that the proposed method substantially reduces verification costs. Compared to interactive verification approaches, the average reductions in code size and manual effort are 88.60% and 61.51%, respectively; compared with generative AI plus interactive verification methods, the average reductions in code size and manual effort are 88.09% and 41.76%, respectively. Overall, the proposed framework provides a systematic and highly automated solution for the formal verification of complex data structure algorithms in specific domains, while also offering a feasible pathway and methodological support for generating correct functional executable programs.