Not the parent, but indeed like you said, writing unit tests doesn't show absence of bugs, but can only show their presence. To be able to state that a piece o

Not the parent, but indeed like you said, writing unit tests doesn't show absence of bugs, but can only show their presence. To be able to state that a piece of software is bug-free and formally correct, we first need a notion of correctness: that the algorithm follows a [formal] specification. The first step would be to formally specify what the software/algorithm should do. Then, the next step would be to use formal methods and mathematical tools (e.g. set theory and logic) to prove that your algorithm does exactly as the specification says. TLA+ is a formal method that can be used for writing specifications and model-checking them. While a big step forward from testing, model-checking still doesn't "prove" anything. For proving, you can use theorem provers like the Z3 [0] SMT solver (or a formal framework that uses theorem provers) to do proof checking. The Event-B [1] method is one such formal method that uses SMT solvers and allows you to model systems starting with a very abstract and high-level model, state invariants about your system, and prove that those invariants hold as you refine your models and make them more concrete. Feel free to shoot me an email if you like to talk more about formal methods :) [0]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]: http://www.event-b.org/ http://www.event-b.org/