Traditionally, the verification of software code has been a labor-intensive process involving manual code reviews or running the code to identify anomalies. While valuable, these methods are susceptible to human error and impractical for complex systems. Enter Baldur, a meticulously engineered solution that harnesses the power of Large Language Models (LLMs) to generate mathematical proofs