We take a break from Flutter and Dart by discussing what it means for software to be correct. Do you trust unit tests to give you the guarantees you are looking for? What does it mean for software to be actually correct? Can we give some formal guarantees about the behavior of your program? During this talk these questions and more will be answered. The goal of the presentation is to show examples of formal guarantees in an approachable manner. We will touch upon how to use the type system to your advantage to eliminate the mere possibility of bugs. Finally, we conclude by showing examples in the Lean theorem prover where we can prove guarantees of more complex properties. Expect some unpopular opinions and hopefully a change of perspective regarding what we call correct.