Long version: Formal verification is a broad topic with a lot of different facets. But hopefully this sheds some light on some of the more useful ones:
Model-checkers like TLA+. You can specify an algorithm, say something simple like a bank account transfer where a sender's account is debited, and a receiver's account is credited. You can then set constraints, such that the sender's account must have enough to cover the transfer, etc. TLA+ will then run through all the scenarios in your algorithm to find corner-cases when the constraints aren't met. It's useful for modeling distributed systems, and you can try simulating an algorithm in parallel to see error conditions in multi-threaded code.
The downside to TLA+ is that you produce a specification, but still have to reproduce the specification in compilable/runnable code. I understand Amazon has had a lot of success using TLA+ to wring out potential bugs in systems before implementing them, and Leslie Lamport (author of TLA+ and creator of LaTeX, too) has some great (and entertaining) videos on his website explaining how they work: https://lamport.azurewebsites.net/tla/tla.html
There are formally-verifiable dialects of programming languages like the SPARK dialect of Ada, and Frama-C, which let you specify pre and post-conditions for functions, and then it will perform model-checking with flow analysis and SMT solvers to ensure those conditions are met in a way that's mathematically sound. Some conditions, like lack of buffer or integer overflows, are always checked. This way, code which has passed the proof stage can truly be said to be free of run-time errors, and whatever extra contracts you've added in your code will be met as well. Since all of this is checked at compile/proof-time, there's no run-time penalty for the extra assurance.
I came up with this simple example of SPARK code that proves if I have a function that doubles every element in an array, then the result satisfies a contract where every element in the output is even: https://pastebin.com/BtkaEDQ5
There are also proof assistants and theorem proving tools/languages like HOL, Isabelle, Coq, LEAN, and others which IMO fall under the umbrella of formal verification, but more on the computer science side than software engineering. In contrast, TLA+ and SPARK are very useful and practical for developing high-integrity software. Still, they're programming languages, and you can write executable code in them that can be said to be mathematically sound. A good resource is the Software Foundations course: https://softwarefoundations.cis.upenn.edu/
Some dependently-typed programming languages like Idris, F*, Dafny, and (I think) Liquid Haskell provide different mixes of these capabilities, but are geared towards producing usable software.