Below is a compact map of what kinds of guarantees engineers usually want (safety, boundedness, convergence, timing, etc.), and how formal verification (FV) actually secures each one—what you write, how you prove it, and what evidence (“certificate”) you can ship.

1) Safety (nothing bad ever happens)

• What you state: “Always avoid a bad set.” In temporal logic: G ¬bad (globally not bad).

• Typical math form: an inductive invariant I(x)I(x) such that

  (i) I(x0)I(x_0) holds initially, (ii) I(x)∧step(x,x′)⇒I(x′)I(x)\wedge \text{step}(x,x') \Rightarrow I(x'), and (iii) I(x)⇒¬bad(x)I(x)\Rightarrow \neg bad(x).

• How you prove: k‑induction / IC3(PDR) / model checking; abstract interpretation for code; barrier certificates (CBFs) or set‑invariance for dynamics.

• Certificate you can ship: the invariant (or barrier function) itself, plus a machine‑checkable proof/UNSAT certificate.

• Runtime backstop: a monitor/shield that enforces the safety predicate and switches to a fallback controller if it’s about to be violated (Simplex pattern).

2) Boundedness (state stays within limits)

• What you state: “All variables stay bounded.” Equivalent to safety with a forward‑invariant set XsafeX_{\text{safe}}.
• How you prove (software): numeric invariants via abstract interpretation, interval/polyhedral domains, refinement with SMT.
• How you prove (control/CPS): find a Lyapunov or storage function showing trajectories cannot escape a compact set; or a CBF ensuring h(x)≤0h(x)\le 0 remains true.
• Certificate: invariant set description (polytope/ellipsoid) or barrier function with derivative condition.