In this Master’s Thesis, I outline a class of tree-based active learning grammatical inference algorithms referred to as *-VADA. I define necessary concepts, and then define three variants of the algorithm class, as well as giving proofs of soundness and completeness results for all three. The first algorithm covered in this thesis, ARVADA, originates from the 2021 paper ”Learning Highly Recursive Input Grammars” by Neil Kulkarni, Caroline Lemieux, and Koushik Sen. Their 2021 paper outlines the algorithm as wellas gives evaluation of heuristic performance. Using their definition of ARVADA as a launching point, I seek to formalize and strengthen soundness and completeness results by formalizing the ARVADA algorithm itself, as well as building off variants of the algorithm with formally proven correctness results.