It's all about model checking:

https://en.wikipedia.org/wiki/Model_checking

Three of the pioneers of model checking won the Turing Award back in the noughties:

https://amturing.acm.org/award_winners/clarke_1167964.cfm

https://amturing.acm.org/award_winners/emerson_1671460.cfm

https://amturing.acm.org/award_winners/sifakis_1701095.cfm

Z3 is an amazing theorem prover, bordering on magic.

https://en.wikipedia.org/wiki/Z3_Theorem_Prover

Theorem proving is often used in model checking.

This guy's code produces Z3 theorems for a subset of the x86 instructions. By theorems, I mean "mathematical statements about how they work".

They can be combined so that a small(ish?) piece of x86 code can be turned into a model, which Z3 can prove (or disprove) statements about.

This is very useful for proving a piece of code right or wrong.

Model checking used to require a phd -- now it just requires a bit of effort and "mathematical maturity". We have come a long way towards making it a generally available tool for all/most programmers but there is still a long way to go.

Could this be used to show that two programs (with only instructions from the covered subset) are equivalent?

You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].

1. https://github.com/AliveToolkit/alive2

2. https://sel4.systems/

This type of thing can help you formally verify code.

So, if your proof is correct, and your description of the (language/CPU) is correct, you can prove the code does what you think it does.

Formal proof systems are still growing up, though, and they are still pretty hard to use. See Coq for an introduction: https://coq.inria.fr/

This was for a super optimizer.