I don’t know anything about MIRI research strategy than is publicly available, but if you look at what they are working on, it is all in the direction of formal verification.
After speaking to experts in formal verification of chips and of other systems, and they have confirmed what you learned from fiddlemath. Formal verification is limited in its capabilities: Often, you can only verify some very low-level or very specific assertions. And you have to be able to specify the assertion that you are verifying.
So, it seems that they are taking on a very difficult challenge.
I don’t know anything about MIRI research strategy than is publicly available, but if you look at what they are working on, it is all in the direction of formal verification.
After speaking to experts in formal verification of chips and of other systems, and they have confirmed what you learned from fiddlemath. Formal verification is limited in its capabilities: Often, you can only verify some very low-level or very specific assertions. And you have to be able to specify the assertion that you are verifying.
So, it seems that they are taking on a very difficult challenge.