Formal verification is actually a very interesting concept and topic. There is a famous statement called the Curry–Howard correspondence: every type signature is a theorem, and the implementation is its proof.

So if I have a language where I can encode in the type system that a number is a prime and is even, then for example the following would be a theorem with a proof:

  Lemma even-prime: a -> Prime(a) ∧ Even(a) { // read as 'it returns a number `a` that is both prime and even 
    return 2
  }

If we restrict the language enough, we can both encode very complex statements and can make sure that one can only ever write an implementation that compiles if it's actually true. E.g. an ordinary language like python where you could return None instead of 2 would fail these requirements.

So they often have dependent type systems -- in these you can freely mix functions and values in your type signatures, not just types. E.g. you could have a Matrix type with two parameters, and then you can have functions like `transpose: Matrix a b -> Matrix b a`.

---

But this is just one side of the whole thing, the other is how to actually prove anything, like what even is `Even` in the above? A type like `someNum: Int` is also a theorem, but it only translates to "there exists an integer" - hardly interesting.

The real "mind blow" (at least to me) was that we just simply create a type for Equality. It takes the same parameter twice [1] (like in the Matrix example it would be Matrix a a) -- and thus we get a construct that can only be instantiated if the two sides are equal as per the language's compilers rules, that is automatically enforced by the compiler itself!

So now you can have `Eq 2 (1+1)`, but not `Eq 2 (1+3)`. And one last step that makes it general enough for all kinds of proofs, the compiler of these languages are not Turing complete. You can write many things, but for reasoning about loops you usually introduce a fuel that is always decreasing (and thus the compiler will accept it, as it knows it will run out once and that's enough for it). So it can evaluate everything, even in types and creating a normalized expression -- and then accepts everything as equal that normalizes to the same thing.

So for a more complex proof, you can just break down the problem to small steps that are by themselves understandably equal by the compiler.

[1] It's not quite true in this form