Formal verification of software can provide a more rigorous guarantee of correctness compared to conventional software testing methods. However, doing this by hand requires substantial effort and is often impractical. To combat this, various verification tools have been developed in recent decades to at least partially automate this process. In this paper we explore Why3, a tool for deductive program verification, by implementing and verifying the A* algorithm. We find that Why3's expressive language allows for easy implementation and verification of A*. However, we also find that it has a significant learning curve and requires some knowledge on formal verification to use. In spite of this, we find it is a useful tool for automated verification.