Box-and-arrow diagrams seem inevitable for presentation of software architecture; however, the term "boxology" often mocks their over-use, especially when informal. We introduce in this paper a formal boxology to serve as a semantic domain for graph-based software architecture representation languages: the Nested Boxes and Arrows (NBA) model. NBA graphs use commonly-adopted features of structure diagrams for software: boxes for objects, arrows for relations, attributes for values, and a containment hierarchy. NBA graphs are visualized using a number of conventions, and are transmitted in exchange languages such as GXL and TA. The NBA model is formalized as typed graphs with attributes and an identified spanning tree (containment). Meta-modeling is defined and formalized by schemas, which are also NBA graphs. The universal schema is defined. A number of tools have been developed to query, manipulate and visualize NBA graphs.