 Social procedures that have algorithmic aspects can often be improved by redesign. This holds for voting and other peaceful decision making procedures, for match-making, for auctioning, for fair division of estates, and for many procedures of distributive justice. The algorithmic aspects can be analyzed with formal methods. The term “social software” was coined by Rohit Parikh (2002) for the emerging interdisciplinary enterprise that is concerned with the design and analysis of algorithms that regulate social processes. Such analysis and (re-)design uses methods from logic, game theory and theoretical computer  science.[1]  The goals of research in formal approaches to social procedures are modeling social situations, developing theories of correctness, and (re-)designing social procedures, ideally leading to new social behavior.