diff --git a/Notes on Papers/A Review of Formal Methods applied to Machine Learning.md b/Notes on Papers/A Review of Formal Methods applied to Machine Learning.md
index 7d7157dc7..309e88e3d 100644
--- a/Notes on Papers/A Review of Formal Methods applied to Machine Learning.md	
+++ b/Notes on Papers/A Review of Formal Methods applied to Machine Learning.md	
@@ -26,7 +26,8 @@ network?
 **What is the main thrust?**
 This review gives an overview of formal methods applied to machine learning.
 Formal methods has been used for ML to test for robustness for various 
-perturbations on inputs. They start by talking about several types of formal methods, including deductive verification, design by refinement, proof 
+perturbations on inputs. They start by talking about several types of formal 
+methods, including deductive verification, design by refinement, proof 
 assistants, model checking, and semantic static analysis, and then finally, 
 abstract interpretation of semantic static analysis. The last one has been 
 used the most in FM of ML.
@@ -39,7 +40,14 @@ These methods generally do not apply well to large networks (beyond
 hundreds gets rough), but give the highest level of assurance. Here, there
 are two more subcategories: SMT based solvers and MILP-based solvers.
 
-SMT solvers are Satisfiability Modulo Theory solvers. These solvers 
+SMT solvers are Satisfiability Modulo Theory solvers. These solvers a set
+of constraints and check to see whether or not all of the constraints can be 
+satisfied. Safety conditions are encoded as the *negation* of the safety constraint.
+That way, if a safety condition is violated, the SMT solver will pick it up as a 
+counter example. 
+
+MILP based solvers are Mixed Integer Linear Programming solvers. MILPs use
+linear programming where certain constraints are integers to 
 
 **What is the supporting evidence?**