To prove that the result of a program is correct, one has to prove that all transitions from each state (line) to the next is valid. We will be looking into the The basic idea behind Jolt and Lasso; to verify an execution trace by using table lookups.