Abstract: This paper describes some tools to support formal methods, and conversely some formal methods for developing such tools. We focus on distributed cooperative proving over the web. Our tools include a proof editor/assistant, servers for remote proof execution, a distributed truth protocol, an editor generator, and a new method for interface design called algebraic semiotics, which combines semiotics with algebraic specification. Some examples are given. 							
						
							
					 															
					Joseph A. Goguen, Kai Lin, A. Mori, Grigore Rosu,