Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper, we argue the position that modalities, in the sense of modal logic, should be a go-to approach when specifying and verifying low-level systems code. We explain how the concept of a resource context helps guide the design of new modalities for verification of systems code, and we justify our perspective by discussing prior systems that have used modalities for systems verification successfully, arguing that they fit into the verification design pattern we articulate, and explaining how this approach might apply to other systems verification challenges.

翻译：尽管低级系统在功能上存在差异，但它们展现出特定的计算资源设计与使用模式。本文主张，在规范和验证低级系统代码时，模态逻辑意义上的模态应成为首选方法。我们阐释了资源上下文的概念如何指导设计用于系统代码验证的新模态，并通过讨论先前已成功运用模态进行系统验证的案例来论证我们的观点——这些案例均符合我们所阐述的验证设计模式，同时说明该方法如何适用于其他系统验证挑战。