Formal methods increasingly play an important role in the development of reliable computer systems, but computer support for formal methods in general lags well behind the state of the art, and in particular, usually fails to take account of the situation today, in which most significant software and hardware systems are developed by large teams, usually distributed over space and time, using a combination of formal and informal methods and a variety of tools to attack different facets of the problem, while struggling with inadequate user interfaces, poor documentation, and difficult mathematics.

The Tatami project is designing, building and testing web-based tools to ameloriate these problems, by supporting distributed cooperative work using multiple logical systems and their integration, by paying careful attention to user interface design, and by having the tools generate web-based output that fully documents what was done, is easy to browse, and has links to tutorials on the underlying mathematics, as well as to informal explanations. The system is available over the internet, and is well documented and efficient.

Some particular innovations of this project include the following:

• Support for first order behavioral logic, via the Kumo proof assistant and proof website generator, and its underlying BOBJ proof engine. This is a powerful new logic that can treat states in a natural way, as well as streams and other infinite data structures, and object oriented features, in addition to the traditional data structures and functions.
• A novel notion of proof that includes not merely formal proof steps, but also proof explanation and large-grain proof structure, and that allows informal reasoning to be integrated with fully formal reasoning. This is supported by an innovative use of a fuzzy logic of confidence levels for proof parts.
• A new protocol that supports distributed cooperative proving over the internet, keeping track of the relations among multiple versions of tasks, specifications, proof parts, and explanations.
• A novel framework that allows the integration of multiple logical systems and tools that use them, based on a new theory of "institution morphisms".
• A new theory for user interface design, called "algebraic semiotics," which holds promise of providing a systematic, scientific approach to this difficult but crucial aspect of system design.

The Tatami project website is

www.cs.ucsd.edu/groups/tatami/

It has had more than 8,000 hits in the last 3 years (not counting hits originating at UCSD). Many examples and papers produced by this project are linked from its homepage, including websites that have been produced by the Kumo system. The BOBJ proof engine also has a homepage,

www.cs.ucsd.edu/groups/tatami/bobj/

which again has links to many examples, some of which may be rather surprising.