It's all about model checking: https://en.wikipedia.org/wiki/Model_checking https://en.wikipedia.org/wiki/Model_checking Three of the pioneers of model checki

It's all about model checking: https://en.wikipedia.org/wiki/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/clarke_1167964.cfm https://amturing.acm.org/award_winners/emerson_1671460.cfm https://amturing.acm.org/award_winners/emerson_1671460.cfm https://amturing.acm.org/award_winners/sifakis_1701095.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 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.