Skip to content

Safety margins and certificates

Intuition

A safety margin is a number that is positive in allowed states and negative after a violation.

That single scalar is how you tell a safety learner what "safe" means. You do not write a reward that trades off progress against risk; you hand the learner the margin and it learns the largest set of states from which safety can be maintained. The learned value function is that answer, and — because it is grounded in the margin — its sign is a learned safety certificate: an empirical certificate whose soundness we validate against a ground-truth reachability solve (see oracle validation), rather than a formally verified guarantee.

The two margins

There are two margins, one per safety problem. Both follow the same sign convention: ≥ 0 means "in the good set".

symbol name ≥ 0 means used by
g(s) safety margin the state is outside the failure set (safe) every safety learner
l(s) target margin the state is inside the target set ReachAvoid* only

A natural choice for g is a signed distance to the failure boundary (positive outside, negative inside), and for l a signed distance to the target (positive inside). The magnitudes matter too — they set the value function's scale and, in reach-avoid, the risk trade-off between committing to a maneuver and stopping (see best practices).

The certificate: V ≥ 0

In theory. At the Bellman fixed point — under the stated assumptions (the right min/max backup over margins, γ → 1, exact function representation) — the value function V satisfies:

V(s) ≥ 0 ⟺ the policy can stay safe from s — forever (avoid) or until it reaches the target without ever failing (reach-avoid).

{V ≥ 0} is then the certified set: the safe-controllable region, with {V = 0} its boundary.

In practice. What you actually train is a neural approximation V̂ of that fixed point from finite data, so {V̂ ≥ 0} is a learned certificate estimate, not a formally verified set. Whether it can be trusted is an empirical question — is V̂ sound? — that we answer by measurement: on bicycle5d, V̂ ≥ 0 predicts closed-loop reach-avoid success with ~98% precision against a Hamilton–Jacobi ground truth (see the oracle validation). Treat {V̂ ≥ 0} as a well-validated certificate, not a guarantee.

This is the property that makes safety_sb3's value functions usable as a runtime safety filter: run your nominal controller, and switch to the safety policy whenever the nominal's proposed next state has V̂ < 0.

For the estimate to approach the certified set, the value function must be learned with the right Bellman operator — a min/max recursion over margins, not a discounted sum of rewards. That is what Backups are about, and getting it exactly right (no entropy bonus in the critic target) is what makes the learned certificate sound rather than overconfident — as the oracle validation study measures.

How the library represents it

  • g(s) rides on the reward channel — the reward is the margin.
  • l(s) rides on info["l_x"] (NumPy path) or is returned directly by step_tensor (tensor path).
  • The episode terminates when g < 0.

The exact interface — spaces, dones/truncation, normalization rules, NumPy vs tensor — is the environment contract.

Never normalize the reward

VecNormalize(norm_reward=True), or any reward scaler, silently corrupts the backup: the value function's zero level set is the safety boundary, and rescaling moves it. Observation normalization is fine and recommended.

Consequences for users

  • You get a certificate for free with the policy — no separate learning step.
  • The certificate is only as good as the margin. A g that is wrong at the boundary moves the boundary; a margin violated by your own reset states condemns that region by construction.
  • Avoid and reach-avoid are different problems with different operators. Choosing the problem is choosing the Mode, not bending the margins — see Choose a learner.