# Proof Rules

Caesar supports a number of proof rule encodings out of the box. The proof rules are used via annotations on while loops. All while loops used in HeyVL must have a proof rule annotation so that they can be verified with loop-free verification pre-expectation reasoning.

If you have read our OOPSLA '23 publication: these proof rules were implemented in our `pgcl2heyvl`

tool to reason about pGCL programs, but are now implemented directly in Caesar.
This allows verifiers for languages other than pGCL to re-use the proof rule encodings.

Proof rules are only sound in specific contexts. Using proof rules in a wrong way may lead to unsoundness. To be certain that a proof rule may be applied, correctness of the proof rule needs to be proven with respect to the language semantics that are to be encoded. See our OOPSLA '23 publication for details on the theory.

## 📄️ Induction and k-Induction

Induction and k-Induction are proof rules for while loops.

## 📄️ Loop Unrolling

Loop unrolling, also known as bounded model checking.

## 📄️ ω-Invariants

TODO.

## 📄️ Almost-Sure Termination

TODO.

## 📄️ Positive Almost-Sure Termination

TODO.