In the research papers "Quantum Probabilistic Dyadic Second-Order Logic" (2013) and "PLQP & Company: Decidable Logics for Quantum Algorithms (2014), which were written together with my VIDI-team members, we used our earlier quantum dynamic logical systems as a starting-point and extended their expressivity to include probabilistic features. Using the more expressive systems allowed us to enrich the class of quantum protocols (studied in Quantum Information Theory) that can be verified via our logical setting. In the mentioned work we express the formal correctness of several protocols, including Quantum Leader Election, the Deutsch-Josza algorithm and the important Quantum Search algorithm. Later, part of the vidi team members went on to show the application of a probabilistic logical system for the verification of the correctness of the main BB84 Quantum Key Distribution protocol in quantum information theory.