This curriculum intends to provide a collection of formal methods to supplement and replace the tradi­tional architect’s arsenal. These methods produce mathe­matical proofs of critical system properties. Note that such proof can not typically be produced as an after­thought to a system’s architecture. Instead, the architecture needs to be designed from the start to be amenable to such proof. While designing and building systems that are amenable to various flavors of automated testing – such as unit, integration, accep­tance, and property testing – is estab­lished practice and well-supported by common technology stacks, formal methods require a substan­tially higher effort to incor­porate in a design. For instance, estab­lishing a formal connection between speci­fi­cation and imple­men­tation requires a careful selection of speci­fi­cation and programming languages, respectively.

To apply formal methods, archi­tects need to formulate important properties of the software system mathe­mat­i­cally, construct an architecture capable of ensuring these properties, and then proceed to verify them formally. Creating an architecture fit for verifi­cation requires careful consid­er­ation, and a high degree of architectural competency.