How is verifying whether an assignment satisfies a boolean formula possible in polynomial time?

How can I prove that I can verify whether a boolean assignment of variables $a$ satisfies some boolean formmula $\phi$ in polynomial time?

I know that we can just plug the boolean assignment into the formula, but this seems to be a very high-level description, and I am not sure that it is a reliable one since we must simplify the formula.

There is no need to simplify the formula, you just evaluate it recursively according to the definition of the boolean operators in use.

Let $\varphi$ a boolean formula and $a : X_\varphi \to \{0,1\}$ an assignment of all variables that occur in $\varphi$. Now we define the evaluation function $\operatorname{eval}_a$ on variable-free boolean expressions in the following way:

$\qquad \begin{align}
\operatorname{eval}_a(\text{true}) &= 1 \\
\operatorname{eval}_a(\text{false}) &= 0 \\
\operatorname{eval}_a(x) &= a(x) \\
\operatorname{eval}_a(\lnot \varphi) &= 1 - \operatorname{eval}_a(\varphi) \\
\operatorname{eval}_a(\varphi \land \psi) &= \operatorname{eval}_a(\varphi) \cdot \operatorname{eval}_a(\psi) \\
\operatorname{eval}_a(\varphi \lor \psi) &= \max(\operatorname{eval}_a(\varphi), \operatorname{eval}_a(\psi)) \\
& \vdots
\end{align}$

Clearly, $\operatorname{eval}_a(\varphi) = 1$ if and only if $a(\varphi) \mathop{|\!\!\!==\!\!\!|} \text{true}$ (here, $a$ is continued on $\varphi$ in a syntactical manner: it replaces all variable occurrences $x$ in $\varphi$ with $a(x)$). If in doubt, perform a structural induction along the inductive definition of boolean formulae. Furthermore, $\operatorname{eval}_a$ performs about one operation per operator and literal; thus it runs in time $O(|\langle \varphi \rangle|)$.

StackExchange Computer Science Q#7134, answer score: 11