diff --git a/BlankProjectTemplate/docs/Design/MIS/MIS-Checklist.tex b/BlankProjectTemplate/docs/Design/MIS/MIS-Checklist.tex
index 690d25ecd45517b31ef93d2866a184a6d7c7f091..6e6bf3e0c6c44260c3813131eab2be02db8afa15 100644
--- a/BlankProjectTemplate/docs/Design/MIS/MIS-Checklist.tex
+++ b/BlankProjectTemplate/docs/Design/MIS/MIS-Checklist.tex
@@ -85,7 +85,11 @@
     state variables for another module, or an environment variable.
   \item Outputs use $out := ...$
   \item Exceptions use $exc := ...$
-        
+  \item If the state invariant is satisfied before an access program call, it
+    will remain satisfied after the call
+  \item State invariant is initially satisfied
+  \item Local functions make the specification easier to read (there is no
+    requirement that the local functions will actually be implemented in code)
   \end{todolist}
 
   \item Mathematical syntax
diff --git a/Lectures/L14_MIS/MIS.tex b/Lectures/L14_MIS/MIS.tex
index b683b59a34b3267ebd9826e81509448605d66c92..b697f842f119d5a9e61fa9ff8f75504ca622ae07 100755
--- a/Lectures/L14_MIS/MIS.tex
+++ b/Lectures/L14_MIS/MIS.tex
@@ -771,7 +771,7 @@ seq\_init():
 \item Using built-in language constructs
 \end{itemize}
 \item Caused by errors made by programmers, not by users
-\item Write code so that it avoid exceptions
+\item Write code so that it avoids exceptions
 \item Exceptions will be particularly useful during testing
 \end{itemize}