Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.

The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.

So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.

A proof is just a manipulation of each "side" until they are trivially equal to each other).

One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)