Thanks Kent and Gerwin! To Kent's question about how I found the issue with x86_read_fs_base_impl: it wasn't the result of any static analysis, just something that I stumbled on while browsing to figure out how segment registers are handled ... and Kent's description answered that nicely. Thanks specifically for pointing out RESET_SELECTORS; I missed that previously because it uses an unadorned "es" whereas I had searched for "%es" to reduce false positives; lesson learned ... On the verification side, I've long been interested in the question of how we protect against covert channels resulting from hardware state components that are undocumented, or that don't work as intended, or that are not captured in a formal model. [There was a news item in the last few weeks about a (seemingly harmless) flaw of this kind in the Apple M1 processor, which is probably why this was on my mind again.] Best wishes, and thanks again, Mark