Lemmas

Package hard reasoning into reusable proof steps. Lemmas let later contracts rely on facts you have already established.

Declaring Lemmas

Lemmas are proof helpers that establish facts for the verifier without affecting runtime behavior.

Calling lemmas establishes facts that help the verifier prove your code correct.

Step lemmas break complex loop invariant proofs into manageable inductive steps that the SMT solver can verify.