Candidate implementations are checked against a suite of temporal-logic properties; verdicts aggregate into a reward; every violation returns a counterexample trace. The two placements of that signal — training time and inference time — share one currency: the counterexample.
require(). The checker answers with the
two-step behavior that exploits it, replayed on the state graph.Language models write code now, and the standard recipe for making them better at it is reinforcement learning from verifiable rewards (RLVR): the model generates a candidate, a mechanical checker scores it, and the score trains the model. For code, the usual checker is a test suite. Tests have three structural limits: they certify behavior only on the cases someone thought to write; when they fail, they say “failed” and little else; and a model under training pressure learns to game them — pass the cases, miss the point.
The claim of this page, made runnable: for stateful systems in adversarial settings — here, a smart contract — a model checker over temporal-logic properties is a stronger reward oracle. It decides each property over every reachable state of a model of the system, and when a property fails it returns the failing behavior itself, a counterexample: structured training material that a bare pass/fail cannot supply.
The signal plugs in at two places. At training time, verdicts aggregate into a scalar reward that updates the model, and versioning the property suite makes capability drift measurable across model generations — re-checking is a re-run. At inference time, the counterexample steers the repair of one artifact (or ranks a best-of-n batch under a frozen model). The trade between the two is the classic one: inference-time placement works with any frozen model and guarantees each artifact, but the checking bill recurs per sample and the model itself learns nothing.
The recipe has three moves. One — model the system: describe it as a finite set
of states and the moves between them. The contract on this page boils down to five
variables, which gives 128 possible states; every require() in the source becomes a
rule about which moves are allowed, and a forbidden call simply changes nothing.
Two — state the requirement as a property: a formula about how states may unfold
over time, such as “an upgrade only ever executes after the delay has elapsed”.
Three — check: an algorithm visits every reachable state, exhaustively, and returns
either holds everywhere or a concrete run that breaks the property.
Two things are worth holding onto. The check is a decision procedure — a yes/no algorithm that always terminates, with no human in the loop and no “maybe”. And the negative answer is a behavior: a step-by-step run you can watch, replay and learn from. On this page the whole world fits in 128 states, so the exhaustive visit costs under a millisecond — the badge above ran the full battery when the page loaded.
| Auto-active program verifiers & theorem proving (Dafny-style contracts, proof assistants) | Model checking (this page) | |
|---|---|---|
| Object checked | the code itself, over unbounded state | a finite model of the system |
| Native guarantee | compositional proofs about the program — the strongest form of assurance software has | each property decided over every reachable state of the model |
| Automation | proof search, guided by annotations the author writes (pre/postconditions, invariants) | push-button decision procedure |
| Failure artifact | an unproven obligation — where it fails, rarely why | a counterexample: a concrete, executable trace to the violation |
| Under change | proofs break and need maintenance | re-checking is a re-run; regression tracking comes for free |
| Standing cost | writing specifications and invariants | writing the model — fidelity to the code is the gap to manage (see the colophon) |
One logic is never enough: EF (“a continuation exists”) has no equivalent in linear-time logic, which speaks about single runs; the fairness patterns G F / F G have no equivalent in branching-time logic. CTL and LTL are incomparable, the suite on this page deliberately uses both, and the same split lifts one level up to the probabilistic logics (PCTL, CSL) at the ladder’s top rung.
The running example is a timelock: a contract whose owner may propose an upgrade, must then let a delay elapse in public view, and only afterwards may execute it (or cancel). The delay is the whole point — it is the community’s window to react before a malicious upgrade goes live. The model’s world is adversarial by construction: at every step, anyone (owner or attacker) may attempt any call, and the checker explores all of it. Alongside the correct implementation stand four flawed candidates, each one line apart — a dropped delay check, dropped authorization, a dropped guard, and a copy-paste slip that quietly freezes the contract forever. Four bugs of the kind review misses, because every individual call still “works”.
Built for two speeds: the primer above assumes no background; if you verify software for a living, the three cards under the self-test badge jump straight to the exhibits.
The artifact under verification is a timelock upgrade contract: the owner proposes an upgrade, a delay must elapse, then the owner may execute it (or cancel). The repository carries one correct implementation and four flawed candidates — each a one-line deviation of the kind code review misses precisely because every individual call still “works”.
Each candidate is modeled as a finite transition system in SMV. The translation is
mechanical and the environment is adversarial by construction: caller and action
are left unconstrained, so the checker explores every interleaving of calls by every
party. Each Solidity require() becomes a transition guard; a call whose guard
fails changes nothing — a stuttering step, mirroring revert semantics.
propose / execute / cancel) from some sender, or the
passage of one time unit (wait). Time is discrete and the counter saturates: with
DELAY = 2, the cap at 3 preserves the only fact the properties need — whether the
delay has elapsed. Five state variables, 128 states, 8 successors per state. The state
space is deliberately tiny; the argument it carries is the loop, and the modeling gap it
accepts is stated honestly in the colophon.
Pick a call and a sender. Accepted calls move the configuration; reverting calls flash and stay put. The five suite properties are monitored live on your run — including “execution still reachable from here”, which is the progress property P5 seen from the driver’s seat.
The suite is a versioned data object (properties.json), separate from models and
code: it is the reward’s specification. Each property carries a severity weight; the
weights sum to 1, so the reward of a candidate is the weighted fraction of proven
properties. The suite deliberately spans property classes and both logic families
(the primer’s glossary says why one is never enough) — that choice is what
the frozen exhibit and the ladder are about.
Five candidates × five properties. Every verdict in this table is computed in your browser by the portal’s checker, then compared against the repository’s committed expected matrix — the same 35 instances its CI re-checks on every push.
src/loop.py.The scalar is the policy-gradient signal. Alongside
it travels a per-property signature and, per violation, a labeled negative: the
counterexample trace packaged with the property it violates, its class, and its weight —
material for counterexample-conditioned repair, preference pairs against a proven
sibling, hard-negative curricula. Below, the committed reward record for one candidate,
exactly as src/loop.py emits it.
A copy-paste slip in executeUpgrade(): the guard demands
upgrade_executed where it meant upgrade_proposed. Since executed starts false
and only this function could ever set it, execution is unreachable — the contract
accepts proposals and then holds them forever.
Under the full suite the frozen candidate scores 0.85 and ranks
second — tied with no_proposal_guard, which fails a different property for a
structurally different reason. The tie is informative rather than embarrassing: the
scalar alone cannot tell a bricked contract from a provenance leak, and that is the
argument for the per-property signature travelling with the scalar.
A contract that does nothing violates no safety property: under a safety-only suite the frozen candidate is the degenerate optimum a policy trained on an under-specified verified reward would discover. It is caught here by a property from a class that assertional reasoning does not natively speak — P5, AG (proposed → EF executed), an existential over continuations. Vacuous satisfaction has a two-decade literature as a specification-quality problem (Beer, Ben-David, Eisner and Rodeh, Formal Methods in System Design, 2001); placed inside a reward loop it stops being a lint and becomes a safety property of the training signal itself.
The baseline and the concession are in the primer: auto-active program verifiers prove the code itself, over unbounded state, compositionally — stronger on that ground than anything in this repository. The ladder’s criterion is what each class of tool yields natively, with a decision procedure attached, at push-button cost. Each rung up asks a kind of question the assertional frame does not natively speak, and each has a runnable file here.
Naive liveness — G (proposal_accepted → F (executes_now ∨ cancel_accepted)) — is false on the correct model, and the counterexample is a design discovery: the owner can re-propose forever, each proposal resetting the delay clock, an upgrade kept permanently pending without violating a single safety property (proposal churn). The formulation that survives carries three explicit fairness premises. Toggle them: the portal’s checker re-decides liveness live, and every lasso it returns names the assumption you dropped.
“48 hours” is what deployment means, and dense time is a different algorithmic family: continuous clocks are first-class state, transitions interleave with time-elapse steps of arbitrary real duration, and the checker decides the property over that infinite-state system symbolically (SMT-based algorithms in nuXmv’s timed mode). The trace below is replayed, and structurally validated, by the portal — it is decided by nuXmv: an in-page explicit-state checker cannot enumerate a continuum, which is precisely what this rung adds.
# 1. one candidate, all five properties, the counterexample in full python3 src/verify.py models/timelock_bypass.smv # 2. the loop: five candidates in, rewards and ranking out python3 src/loop.py # 3. the whole expected-verdict matrix, as CI runs it python3 tests/check.py
Repository: daditalicus/verified-rewards-loop (public release pending at the time this page was generated). One binary — NuSMV — and stock Python 3.9+; no Python dependencies.