diff --git a/research/formal-methods.md b/research/formal-methods.md
index e95b8f2fc6f94ce9c6502a147b875fabeb52a4c9..0eb169e755fdfcdee568f7e64ed08f207abb1baa 100644
--- a/research/formal-methods.md
+++ b/research/formal-methods.md
@@ -8,15 +8,15 @@ This term usually identifies a set of technologies that presuppose representing
 
 Therefore formal methods are highly successful in applications where a high degree of confidence is desired, e.g. in program verification, as the foundation of mathematics, or even in legal frameworks. To accommodate for these applications a large zoo of logics has been developed and mechanized reasoning systems have been developed.
 
-### Entailment Systems
+#### Entailment Systems
 
 The foundation of formal methods is the entailment relation ⊧, a relation between a set Φ of formulae (the assumptions) and a formula T : Φ ⊧ T signifies that T must be true in all situations, where the assumptions in Φ are. So, if Φ is empty, T must be true in all situations, and we call it a theorem. The relation ⊧ is usually defined by reference to some externally given semantics, but can be approximated by a calculus. This gives the notion of a proof: we know Φ ⊧ T , if there is a proof of T from Φ that conforms to the rules of the calculus. So Φ ⊧ T can be verified by purely syntactical means, giving us a way to establish theorem-hood by a machine.
 
-### Logical Systems
+#### Logical Systems
 
 Entailment systems usually induced by logics, i.e. formal languages for representing knowledge with a model and/or proof theory. The KWARC group develops meta-logical approaches for modeling logics and the relations between them. For instance, we have developed the [LATIN Logic Atlas](/projects/latin/); a graph of more than 1000 logic fragments and logic-translations. 
 
-### Interoperability in Formal Methods
+#### Interoperability in Formal Methods
 
-There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge.
+There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge. The KWARC group is developing a general, knowledge-based interoperability architecture: the Math-in-the-Middle (MitM) Approach to interoperability. We use modularly represented mathematical knowledge as a pivot point for connecting systems. In the [OpenDreamKit](/projects/odk) we instantiate this for computer algebra systems, and in the [OAF](/projects/oaf) for theorem prover (libraries).