A model checker still stops at a bound. The last step up is a proof: an argument a machine checks, covering every input, including more of them than anyone could visit.
Formal verification
Also called Formal methods, Proof, Vericoding
Proving that code or a design meets a written specification for all inputs, not only the ones you tried, with a machine checking the proof. It covers what the spec says, under what the proof assumes, and nothing else.
A proof checker rejects an invalid proof however plausible it sounds, so it is one check an agent can't talk its way past. The cost moves to the spec. When one agent writes the code, the spec and the proof, one misunderstanding can sit in all three, and that is self-evaluation bias with a stronger label on it. It can also weaken the spec until it passes, the way it can edit a test. So someone else has to read the spec, usually you, and reading specs is a skill too.
“Verify one property of settle() in Dafny: the shares always add up to the bill, for all inputs. Before you write any proof, show me the spec in plain English and stop, because I will approve it. Then show the proof failing on a copy with the rounding step removed, and list every assumption and everything outside the proof.”