Formal verification is a process that uses mathematical logic to prove or disprove whether a system satisfies a precise behavioural specification.
That system could be a piece of software, hardware, a protocol or even an argument, a chain of reasoning.
Formal verification tools require a vast amount of logic and understanding both in implementing the framework as much as modelling the problem itself. So specifically in software engineering they were either being actively avoided, not known or brushed away as too expensive. Only critical systems used them, i.e medical equipement. One example is TLA+ a language for modeling a system's design and checking for bugs before any code was written.
Today they play a bigger role, arguably in what the AI industry is referring to as RSI (recursive self improvement). The argument goes like this: The system cannot be better than its creator because it's bounded by the data of it's creator so in order to surpass the creator it needs to generate its own data and train itself with that data.
Two very often cited examples are AlphaGo and AlphaZero, two AI systems that play Go, shogi and chess, using a combination of neural networks and specialised treesearch. The reason why they managed to get better than most if not all humans was the ability to play against themselves and generate the data needed to get better.
Some scientists believe they could get the same results with LLMs. The difference between systems like AlphaGo and AlphaZero and LLMs is a reliable verifier. Go and chess have explicit rules, well defined state and unambiguous win/loss conditions. Which means the ground truth feedback is deterministic.
One of the reasons why systems like AlphaProof do so well in mathematics is because Lean acts as the formal verification process in this loop.
Abstract linguistic arguments though resist formal verification, because in order to verify an argument you need to convert the language into symbolic logic, but the issue is that language is full of ambiguity and polysemy and implicit premises. Basically humans assume, with varying degrees of success, what the other party knows or doesn't know as well as their background and omit unnecessary parts of the argument.
But in language you can also get a 100% valid reasoning chain that can be true for me, but not true for the person next to me. There have been attempts to train models as external verifiers which basically play the role of a judge in arguments and chain of thought and it works to a degree but there will always be bias built in them, which brings us back to historical imperialism again. But no one is that much bothered about it, to the point that there are still people out there that declare any non-Western civilisation as barbarian.
Cultures disagree in fundamental values; the same policy can be perfect for a corporation but a community's worst nightmare. So who would build that verifier, and whose values would it enforce?