But ACL2 is a logic. We can prove theorems about the model.
Theorem. MC 'mult is a multiplier (implies (and (natp x) (natp y)) (equal (lookup 'z (mc (s 'mult x y) (mclk x))) (* x y))).
This theorem says that a certain program running on the mc machine will correctly multiply any two natural numbers.
It is a statement about an infinite number of test cases!
We know it is true about the model because we proved it.