Incorporated more of Narges' feedback

Mostly in the formalization section. Defined the formal verification
better, using operational semantics. Stuff is a lot cleaner now.