I am not seeing the connection to LANGSEC. The Spectre and Meltdown attacks turn the processor into a confused deputy, that is all. If anything, this is predicted by LANGSEC. The beef is not even with hardware verification, as some have suggested, because the specification never calls for such security guarantees. The specification is architectural because we want different processors to implement the same architecture, such that they are compatible. The only reason transient instruction sequences have security violating side effects is microarchitectural leaks.