Generation of electricity has traditionally taken place at a small number of power stations but with advances in generating technology, small-scale generation of energy from wind and sun is now possible at individual buildings. Additionally, the integration of information technology into the generation and consumption process provides the notion of smart grid. Formal modelling of these systems allows for an understanding of their dynamic behaviour without building or interacting with actual systems. This paper reports on using a quantitative process algebra HYPE to model a residential smart grid (microgrid) for a spatially-extensive suburb of houses where energy is generated by wind power at each house and where excess energy can be shared with neighbours and between neighbourhoods. Both demand and wind availability are modelled stochastically, and the goal of the modelling is to understand the behaviour of the system under different redistribution policies that use local knowledge with spatial heterogeneity in wind availability.