it's especially confusing since model checking and verification research has been lively for the past twenty years and recently produced some pretty good results (like bedrock and ironclad), but this is all willfully ignored by the langsec community...