Agreed! I started verifying stuff with different tools as part of my PhD and it is really not that hard to grasp the basic concepts. It becomes more complex the deeper you delve in the internals, but I think it would be great if more people verified part of their code in addition to testing it.

Personally, I started with CBMC [1]: it is quite a staple in the field and their documentation is very clear. Basically, it translates a C program (decorated with assumptions and properties to verify) into a SAT formula: if the formula is satisfiable, a property can be violated (and you even get a program trace that shows exactly how that happens).

[1]: https://www.cprover.org/cbmc/