Formal verification is within the reach of an engineering undergraduate (I know this because I am one and have done some basic hands-on formal verification).

I learnt formal verification using free and open-source tools from Symbiotic EDA here: https://youtube.com/playlist?list=PLX1FD-Xa88fbMhT-tTe67O2gz_UwEjz9-

Download and install the free Yosys software and the free solvers on Ubuntu, and then follow the YouTube videos from Symbiotic EDA and try it out hands-on. Visit this link for installation instructions: https://symbiyosys.readthedocs.io/en/latest/install.html

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry.

Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

**Property checking** is a technique where you specify properties, and the solver proves these properties are held true, either for all time i.e. induction, or for a certain number of cycles i.e. bounded model checking. 2 kinds of properties are specified: assumptions and assertions. Assumptions are properties which the solver assumes and assertions are the properties the solver needs to prove. So the problem of proving properties is represented as a SAT (Satisfiability, i.e. Boolean Satisfiability) problem, which is then solved by SAT solvers. 

SAT, as we know, is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs. But there are clever techniques used to speeden this up: blackboxes, cut-points and abstractions.
Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of the tool converging to a solution. 

For a large design, it is a common practice to break the problem of verifying the design into smaller, provable properties that verify the entire design.
For example, [RISC-V Formal](https://github.com/SymbioticEDA/riscv-formal) uses a set of simple properties to prove ISA compliance of RISC-V processors.

Formal verification is a really interesting and challenging field, and the effort is usually worth it. Some bugs like the Pentium Floating point division bug will most likely escape random testing, since the **probability of the occurences leading to the detection of some bugs in random testing is extremely small**. **You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for**. Formal verification proves the entire design is bug-free, provided one writes the right properties. Formal verification using the Induction technique proves the correctness of designs for *infinite cycles*. It's not magic, it's the **power of mathematics and formal logic**.

The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand technique to specify properties that can even span infinite cycles.