As an extremely experienced dev with a ton of Intel assembly experience, I'll confess I have no earthly idea what this is, what it does, who needs it, or what inspired it. Any good pointers to tutorials or introductory material?
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?