Verification

The folder Verification/ holds a Lean 4 development. It models parts of ACRES, proves properties of the models and tests the models against the real code. This page gives the theorems, their assumptions, the findings and the method to run the checks.

Status

A check against the Lean source on 2 October 2026 confirmed each theorem name on this page. The check script passed on that date with an audit of all 3,269 library constants. The Lean models of the Framework exist. The production code of the residual law, the shield, the automaton module, the residual reward and the plan checker does not exist. The Lean models are the specification of that code.

What Lean Proves

A proof is about a model. Four links connect a model to the code.

Link	Function
Differential test	The model and the code get the same inputs. The outputs must agree bit for bit
Golden vectors	The Lean executable writes inputs and outputs to files. Code that does not exist must pass these files later
Constants check	The check script compares the constants of the proofs with configs/scouting_v1.json
Axiom audit	Lean checks every project constant. Only the three standard axioms are permitted

No link is a proof. A link gives evidence that the code does what the model does.

Subjects

Subject	Real Code	Lean Model	Lean Proofs	Link to the Code
Command queue and clock	Acres/Source/Acres/AcresCommandTiming.h	CommandTiming.lean	Proofs/Queue.lean, Proofs/Clock.lean	Differential test
Command path and watchdog	AcresPolaris.cpp (StepPolarisControls), AcresUtvModel.cpp (StepDbw)	Watchdog.lean	Proofs/CommandPath.lean, Proofs/FloatFacts.lean	Differential test
Gear logic	spec.GearManager	GearManager.lean	Proofs/GearManager.lean	Differential test
Action limits	spec.action_to_command, spec.command_rows	ActionMap.lean	Proofs/ActionMap.lean	Differential test
Step reward	rewards.step_terms, rewards.step_reward	Rewards.lean	Proofs/Rewards.lean	Differential test
Bounded reward	rewards.bound, rewards.bounded_reward	Reward/Residual.lean (boundedStep)	Proofs/FailureBound.lean	Differential test
Residual law	Not built	Shield/Residual.lean	Shield/Proofs/Residual.lean	Golden vectors
Shield	Not built	Shield/Shield.lean	Shield/Proofs/	Golden vectors
Mission automaton	mission.EpisodeTracker has the transitions. The module is not built	Mission/Automaton.lean	Mission/Proofs.lean	Golden vectors
Shaping term	Not built	Shaping/Model.lean	Shaping/	Golden vectors; numpy.interp by differential test
Residual reward	Not built. The constants are in the configuration	Reward/Residual.lean (residualStep)	Reward/	Golden vectors; constants check
Planner	solvers.exact_dp, OptionGraph.cost	Planner/Model.lean (solve)	Planner/Optimality.lean, CodeCost.lean, Regret.lean, RegretTight.lean	Differential test; golden vectors
Plan checker	Not built	Planner/Model.lean (checkProposal)	Planner/Checker.lean	Golden vectors

The Lean files are in Verification/AcresVerification/. The Python files are in Learning/acres_learn/tasks/scouting/ and Learning/acres_learn/planners/.

Method

1. One model for each component. Each model follows the C++ or Python code statement by statement. The model uses a scalar type α. Helper functions reproduce the library functions of the code with their NaN rules. These functions are std::clamp, std::max, the max of Python, numpy.minimum, np.clip and numpy.interp. They also include the compensated sum of CPython, the order of numpy.sum and the fused ddot of OpenBLAS.
2. A model before the code. For the framework, the Lean model is the specification. The code comes after the model and must pass the golden vectors.
3. Proofs over exact numbers. The proofs use the models with α = ℚ or α = ℝ and Mathlib.

4. Tests over doubles. Three executables run the models with α = Float (IEEE 754 binary64).

   Executable	Source	Models
   acres_model	Main.lean	Command path, gear logic, action map, step reward
   acres_shield	ShieldMain.lean	Residual law, shield, mission automaton
   acres_golden	Golden.lean	Shaping term, bounded and residual reward, planner, plan checker

5. Axiom audit. audit_project.py finds every library source file, including files absent from the main import. Lean checks every constant by its source module. This includes private names, helper definitions and lemmas. Only propext, Classical.choice and Quot.sound are permitted. A new axiom fails even if no theorem uses it. Proof gaps fail even when a source file disables the warning for sorry. The build fails on warnings. The three executable roots have separate audits because each defines main. The audit helper also has a constant audit. An unknown source outside the library fails registration. Historical files in Reviews/ are outside this gate.

Floats. A proof over exact numbers leaves a gap to the doubles. These measures reduce the gap.

• The proofs of the timeout arithmetic of the watchdog use the real doubles. Lean defines Float by a model of binary64. The tactic decide +kernel evaluates this model in the kernel (Proofs/FloatFacts.lean).
• The proofs of the bounds and the order of the action map cover each double, with NaN and infinities. The proof uses two properties of IEEE rounding: it is monotone, and it does not change a double.
• The gear logic only compares, negates and takes absolute values. Doubles do these operations exactly. Thus its proofs over ℚ are true for each finite double.
• The clamps of the shield only compare and select. The clamp lemmas are true for each linear order, thus for finite doubles (Shield/Proofs/Clamp.lean).
• Some shield theorems are for each scalar type, Float included: the stop on unusable inputs, the intervention flag and the output curvature.
• The kernel evaluates named doubles for the shield, the residual law and the bounded map (Shield/Proofs/FloatFacts.lean, Reward/FloatFacts.lean).

Theorem Counts

The release gate audits 3,269 library constants. Of these, 1,765 are kernel theorem constants, including generated helpers. These counts are not counts of independent safety properties. The executable roots also have audits.

The older lists retain 554 named theorem entries for reference:

Audit File	Theorems	Scope
Verification/Audit.lean	56	The headline theorems of the command path, the gear logic, the action limits and the rewards v1 and bounded
Verification/AuditShield.lean	241	Each theorem of Shield/Proofs/ and Mission/Proofs.lean
Verification/AuditFramework.lean	257	Each theorem of Shaping/, Reward/ and Planner/

These lists help readers find named results. They do not determine audit coverage. AuditAll.lean checks the imported environment; audit_project.py supplies the complete module list.

Group	Files	Theorems
Residual law	Shield/Proofs/Residual.lean	30
Shield	Shield/Proofs/Caps.lean, Clamp.lean, Meta.lean, Rules.lean, FloatFacts.lean, Framework.lean	139
Kinematics	Shield/Proofs/Kinematics.lean	27
Stop command path	Shield/Proofs/CommandPath.lean	8
Mission automaton	Mission/Proofs.lean	37
Shaping	Shaping/Telescoping.lean, Mdp.lean, Potential.lean, Augmented.lean	117
Residual reward	Reward/ResidualProofs.lean, Spec.lean, FailureEvent.lean, FloatFacts.lean	78
Planner	Planner/Optimality.lean, CodeCost.lean	26
Regret	Planner/Regret.lean, RegretTight.lean	23
Plan checker	Planner/Checker.lean	13

Review Findings and Current Status

The independent review of 2 October 2026 found no non-standard axiom in the current project constants. The report is in Verification/Reviews/lean-review-2026-10-02.md. The review found these gaps in the release checks.

• Audit coverage: closed. The gate checks all project constants and fails on warnings. Tests inject proof gaps and new axioms into a private copy.
• Production code. Six components still use test mirrors: the residual law, shield, automaton, shaping term, residual reward and plan checker.
• Trainer reward contract: closed. Residual PPO must use raw rewards: normalize_rewards=false, reward_clip=null and gamma=0.995. The trainer rejects other settings for that variant. The production variant remains disabled. Historical baselines retain their reward transforms; the proofs do not cover those transforms.
• Step limits: guarded. The gate checks both PPO configurations, projection window, path spacing, map parameters and milestone values. A geometric check finds at most four checkpoints in any coverage disc on the current map. Runtime guards for the residual variant reject excessive progress, checkpoint counts, multiple milestones and invalid energy or area inputs. These checks do not prove the vehicle dynamics.
• Failure comparisons. The same-step theorem assumes a lower bound on the continuation value. A later collision can violate that bound.
• Shaping scope. Policy invariance is proved for finite processes. No theorem connects that process to the continuous scouting task.
• Shield scope. The main rule proofs use real numbers. Tests cover doubles; motion proofs use explicit assumptions about speed, braking and latency.
• Mission connection. The automaton tests do not compare the model with EpisodeTracker.

A green check is evidence for the listed checks. It does not establish that the residual framework is ready for training.

Run the Checks

1. Install elan, the Lean toolchain manager. Root access is not necessary.

   curl -sSfL -o elan-init.sh https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
   sh elan-init.sh -y --default-toolchain none
   

2. Get the Mathlib build cache and build one time. The cache is 7.7 GB in Verification/.lake/.

   cd Verification && ~/.elan/bin/lake exe cache get && ~/.elan/bin/lake build
   

3. Run all checks from the repository root.

   PATH=$HOME/.elan/bin:$PATH PYTHON=~/miniconda3/envs/torchenv/bin/python Verification/check.sh
   

The toolchain is Lean 4.34.1 (Verification/lean-toolchain). Mathlib is v4.34.1 (lakefile.toml).

check.sh does these steps:

1. It discovers the proof sources and builds all models with warning failures.
2. It audits every project constant.
3. It checks reward assumptions against configuration, code constants and map geometry.
4. It runs the shield and mission tests against the reference mirrors and golden vectors.
5. It compiles the drive-by-wire harness from the game sources and runs the differential tests.
6. It writes the golden vectors again and compares them with the committed files.
7. It runs the shaping, reward and planner differential tests.

Run the deliberate-failure tests separately. They use a temporary copy and keep the working sources unchanged.

~/miniconda3/envs/torchenv/bin/python Verification/mutation_tests.py --output /tmp/acres-mutation-results

The tests reject proof gaps, unused axioms, proof warnings and unregistered sources. They also reject changed discounts, reward weights, failure penalties, milestones, geometry settings and golden vectors. Both the original and restored copies must pass the gate.

Variable	Default	Function
SEQUENCES	1000	Generated sequences for each component
SEED	20260930	Seed of the sequences
BUILD_DIR	$TMPDIR/acres-verification	Folder for dbw_harness and the new golden files
PYTHON	python3	An interpreter with numpy
LAKE	lake, else ~/.elan/bin/lake	The build tool of Lean

The earlier run of 2 October 2026 printed these differential results. The current gate adds the full constant audit and the reward-assumption checks described above.

axiom audit: 56 theorems, standard axioms only
axiom audit (residual, shield, mission automaton): 241 theorems, standard axioms only
shield: the oracle mirror is identical on 4943 golden shield cases (2988 interventions, 557 stops for inputs that are not usable), 1527 golden residual cases, 10000 fresh shield cases, 2000 fresh residual cases; the golden files are as the Lean model prints them
mission: the oracle mirror is identical on 4624 golden sequences (30496 events), 1000 fresh sequences; the golden files are as the Lean model prints them
constants: as the proofs assume (36 constants)
timing: identical on 1000 sequences, 1533411 events, 452709 steps, 160742 steady_steps, 27 startup_timeouts, 249 stops_checked, 434 pauses_checked
gear: identical on 4000 sequences, 434096 calls, 5801 shifts
action: identical on 14060 actions, True nan_to_zero
reward: identical on 10000 steps, 3 steps where libm pow(x, 2) is one ulp off x * x, 4 fields within their ulp
axiom audit (shaping, reward, planner): 257 theorems, standard axioms only
golden vectors: 7 files, as the models write them
shaping constants: gamma 0.995, shaping_cost_per_step 0.55, shield_per_step 0.5 constants
shaping interp: 9552 numpy.interp queries
shaping potential: 220 golden shaping steps, 8 tables, not written yet (reference implementation only) production shaping code
shaping returns: 12 golden episodes, 3.0727130355551687e-16 largest relative gap of the telescoping identity
shaping reference time: 20 paths against deploy.mission.path_time_s, 8.434857979685428e-16 largest relative difference
reward constants: as the reward proofs assume constants
reward bounded: 5000 steps of variant=bounded, 2313 of them below the knee, 1268 values of rewards.bound, 1 steps where libm pow(x, 2) is one ulp off x * x, 1 fields within their ulps
reward bounded golden: 14 golden values of rewards.bound
reward residual: 49 golden residual steps, 0 with libm's pow one ulp off, not written yet (reference implementation only) production residual reward
reward floats: bounded_reward is above the floor and non-decreasing on a grid of 0.005 over [-1000, knee]; among adjacent doubles in [-60, knee] 8.2 % are reversed (by rounding); it first reaches the floor near -3.16e+08 (a position 25 km off the corridor), and bounded_reward(-1e17) = 0.0 doubles
planner code: raises ValueError (the model: the empty plan, cost 0) exact_dp on a mission without fields
planner instances: 53 golden instances, 52 feasible, 12 with many ties
planner random: 500 random tables, 13 without a feasible plan
planner regret: 8 regret cases, 0.141 largest regret over its bound
planner checker: 16 checker cases, 3 accepted, 52 optimal plans accepted, not written yet (reference implementation only) production checker
verification: all checks passed

Three lines contain "not written yet". They name code that does not exist. For that code, the script tests a reference implementation in the test file against the golden vectors. The lines shield and mission test an oracle mirror. An oracle mirror is a test oracle, not the production code.

Theorems

This table lists the theorems of the first development: the command path, the gear logic, the action limits and the rewards v1 and bounded. The sections from Residual Law give the theorems of the framework.

Component	Property	State	Theorems
Command queue	The steps apply the snapshots in arrival order	Proved for all times	applied_sublist, applied_increasing
Command queue	The length has a bound: one entry for each different due time; +2 over a pause; +1 in lockstep	Proved	length_le_of_dues, pause_bound, lockstep_bound
Command queue	The length has a bound by the number of different due steps	False (not a hazard)	due_step_counterexample
Command clock	Arrival order stays; gaps do not become longer	Proved	due_mono, due_gap
Command clock	The messages of the first read all apply at the next step	Proved (finding 3)	first_read_next
Watchdog	Commands at intervals of 20 ms or less never time out	Proved with assumptions A1 to A4	never_times_out
Watchdog	A silent subsystem disengages within \(T + dt\) and not before \(T\)	Proved; the game trips one step before ACRES Core	disengages_after, core_trips, game_trips
Gear logic	No gear command while \(\lvert v \rvert \ge 0.1\) m/s	Proved	no_gear_cmd_moving
Gear logic	The ULC speed is never against the gear; it is 0 for 1.2 s after a shift	Proved for finite inputs	ulc_along_gear, ulc_zero_after_shift
Gear logic	At most one gear change in 1.2 s; none inside the ±0.2 m/s band	Proved	shifts_spaced, no_shift_in_band
Gear logic	A constant command gets its gear, then its speed	Proved, if the vehicle stops	reverse_liveness, forward_liveness
Action limits	Curvature in ±0.2 m⁻¹, speed in [−1.5, 6] m/s	Proved for each double; the NaN case was false and is fixed	command_mem, command_mem_of_not_nan, command_nan
Action limits	The command is monotone in the action	Proved for inputs that are not NaN	command_mono
Crop never pays	A crop step earns less than the lane step of the same progress	Proved if the lane step costs no more energy	crop_never_pays, crop_never_pays_same_energy
Crop never pays	The same with only the energy bounds of the task	Proved above 0.024 k m of crop for each step; false below	full_width_never_pays, crawl_counterexample
Crop never pays	The same with the presence term \(P > w_E k\)	Proved	presence_term_fix, crop_never_pays_bounded
Failures never pay	Each bounded step is above the floor; the order of steps stays	Proved	boundedReward_gt_floor, boundedReward_strictMono
Failures never pay	The failure penalty alone is not worth more than \(T\) more steps and an end worth at least the penalty	Proved for the configured constants. Finding 37 gives the limit of this statement	failure_never_pays, failure_never_pays_strict, failure_never_pays_v2

Command Path

Model

CommandTiming.lean models FCommandClock (BeginRead, ApplyAt) and TTimedCommands (Push, Take). The value ApplyAtNextStep is −∞ in C++. In Lean it is the constructor Due.next, which is below each time.

Watchdog.lean models one physics step of the Polaris.

1. The step takes the snapshots that are due from the queue.
2. It applies a system enable or disable when the sequence number changed.
3. It marks a subsystem as fresh when its sequence number changed.
4. It gives the subsystem to the bridge while the last message is younger than ExternalHoldS (0.25 s).
5. The timeout part of StepDbw follows: the ages, the enabled flags and the actuator holdover of the ULC.

The age of a subsystem is Fresh ? 0 : Age + Dt. The initial age is 1e9 s. A subsystem is enabled when the system is enabled, the subsystem has a mode, and the age is at most CommandTimeoutS (0.1 s).

Arrival Order

Theorem applied_sublist: for each sequence of pushes and takes, the applied snapshots are a sublist of the pushed snapshots. Each applied snapshot is newer than the snapshot before it. The proof does not use the times. Thus it is true for each behaviour of the clock.

Theorem due_mono: a later arrival never gets an earlier time. Together, the steps see the commands in their arrival order. A step keeps only the newest snapshot of those that are due. This is the intended behaviour.

Bound

Theorem length_le_of_dues: the times of the queue stay strictly increasing. The queue holds at most its initial entries plus one entry for each different due time.

• During a pause, each frame advances the solver by 0. A pause adds at most two entries (pause_bound).
• In lockstep, the queue gains at most one entry (lockstep_bound).
• The bound is for each due time, not for each due step. Three messages at 3, 4 and 5 ms are all due at the step at 1/120 s. They use three entries (due_step_counterexample).

No Timeout

Theorem never_times_out. Let the messages of a subsystem come due at most \(G\) apart. Let the physics steps start at most \(2\delta\) off a grid of \(dt\). Let \(G + 2\delta \le T\). Then the age that the watchdog compares with \(T\) stays below \(G + 2\delta\). This is true from the step of the first message to the step of the last message.

The proof has four parts.

1. due_gap: arrivals \(\Delta\) apart apply at most \(\rho \Delta\) apart. \(\rho\) is the largest ratio of the solver time of a frame to the wall-clock time after the read before. With the frame time as the read interval, \(\rho = 1\).
2. delivered: the step at which a message is due takes that message or a newer snapshot.
3. fresh_at_due: that step sees a new sequence number. The subsystem is fresh.
4. age_le_of_fresh: the age is at most the time after the last fresh step.

For the Ranger, \(T = 0.1\) s, \(dt = 1/120\) s and \(\delta \le 0.5\) ms. With a controller that sends each 20 ms, the age stays below 21 ms.

Disengage

Theorem disengages_after. After the step \(k_L\) that applied the last message, no later step is fresh (no_fresh_after). The age at step \(k_L + j\) is exactly \(j \cdot dt\).

Arithmetic	Step \(dt\)	Engaged While	Disengages At	Theorems
Rationals	1/120 s	\(j \le 12\)	\(j = 13\): 0.1083 s	ranger_timeout_steps, ranger_disengage_time
Doubles, ACRES Core	1/120 as a double	\(j \le 12\)	\(j = 13\)	core_engaged, core_trips
Doubles, game	1/120 as a float: 0.0083333338 s	\(j \le 11\)	\(j = 12\): 0.1000000052 s	game_engaged, game_trips

The two results are within \(T + dt\) and not before \(T\). They differ by one step (finding 2). The ages then stay above the timeout for the next 10 s of steps (core_stays_tripped, game_stays_tripped). The throttle and the brake keep the last output of the ULC for 10 more steps (holdover_core, holdover_game).

Assumptions

Name	Assumption	Basis
A1	The physics thread runs the steps in order. Step \(k\) starts at \(s_k\) with \(s_b - s_a \ge (b - a) \, dt - 2\delta\)	The start is a float that rounds by up to 0.5 ms after 2 hours
A2	A message pushed between the takes of steps \(k - 1\) and \(k\) is not due before step \(k\)	The dispatch order of Chaos. This is an argument, not a proof
A3	The reads are at increasing wall-clock times. \(S_{n+1} = S_n + F_n\). \(F_n \le \rho (L_n - L_{n-1})\)	Reads.WellFormed
A4	The messages arrive after the first read of the clock, not in lockstep, with the system and the subsystem enabled	See finding 3

Gaps between Model and Code

• StepPolarisControls is Unreal code. dbw_harness.cpp and Watchdog.lean copy it statement by statement. The differential test compares the model with the copy, not with the compiled pawn.
• The test does not compile the arithmetic of FAcresRlBridge::BeginCommandRead. That arithmetic is assumption A3.
• The test compiles StepDbw as a whole. It compares only the watchdog outputs: ages, enabled flags, ULC holdover.
• The command-path proofs are over ℚ. The division and the clamp of the clock can move a due time by one ulp. The margin is 21 ms against 100 ms.

Gear Logic

GearManager.lean models spec.GearManager for one vehicle.

Property	Statement	Theorem
No gear command in motion	A GearCmd goes out only when \(\lvert v \rvert < 0.1\) m/s	no_gear_cmd_moving
Never against the gear	The ULC speed is ≤ 0 in R and ≥ 0 in L. It is 0 while a change is pending or on hold	ulc_along_gear
Stop during the shift	After a GearCmd, the ULC speed is 0 for that call and the 11 calls after it: 1.2 s at 10 Hz	ulc_zero_after_shift
No dither	Two gear commands are at least 12 calls apart	shifts_spaced
Hysteresis	A command inside the ±0.2 m/s band never asks for a change	no_shift_in_band
Liveness	From call \(n_0\), the command is a constant outside the band. Then from call \(n_0 + \max(M, 11) + 1\) the gear is the requested gear. 11 calls later the ULC gets the command	reverse_liveness, forward_liveness

The liveness theorems have one assumption. The vehicle is below 0.1 m/s after the ULC speed is 0 for \(M\) calls. The stop hold of the ULC gives this behaviour.

A NaN measured speed never shifts (nan_speed_no_shift). A NaN command reached the ULC as NaN (nan_gear_ulc). The fix of the action map removes the NaN at its source.

Action Limits

ActionMap.lean models spec.action_to_command and the clip of spec.command_rows. The proofs model a double as NaN, ±∞ or a finite rational. Each IEEE operation is the exact result, rounded by a monotone map that does not change a double.

• Bounds. After np.clip, each input that is not NaN is a finite value in [−1, 1]. Then the curvature is in [−0.2, 0.2] m⁻¹ and the ULC speed is in [−1.5, 6] m/s, with rounding (command_mem_of_not_nan).
• Order. The two outputs are monotone in their action coordinate (command_mono).
• NaN. np.clip keeps a NaN. Without a fix, a NaN action gave a NaN curvature and a NaN speed (command_nan). With the fix np.nan_to_num(action, nan=0.0), each input gives a finite command (command_mem, nan_action).

Crop Never Pays

Rewards.lean models ten terms of rewards.step_terms and the sum of rewards.step_reward. The model has no crop-presence term and no bound term. The proofs add them as separate quantities. Reward/Residual.lean models the two terms (boundedStep).

The proofs compare two steps. \(X\) is a step in crop outside the edge band. \(Y\) is a lane step with the same progress, the same time cost, no crop and no other penalty (CleanLaneStep). The weights are those of configs/scouting_v1.json. check.sh fails if they change.

Theorem	Statement
reward_gap	\(r(Y) - r(X)\) is the crop term of \(X\), plus \(w_E\) times the energy difference, plus the other penalties of \(X\), minus each bonus of \(X\)
crop_never_pays	If the lane step costs at most \(\kappa E_\text{ref}\) more energy and \(X\) earns no bonus, then \(r(X) < r(Y)\) when \(w_c \Delta A_\text{crop} / A_\text{ref} > w_E \kappa\)
crop_never_pays_same_energy	With \(\kappa = 0\), each crushed area makes the crop step worse
full_width_never_pays	With the full 1.59 m width over \(d\) metres and energies in \([0, k E_\text{ref}]\): crop never pays when \(12.5\,d > 0.3\,k\)
crawl_counterexample	Below that bound the claim is false: a creep of 1 cm with no energy earns 0.175 more than a lane step at \(E_\text{ref}\)
recrushed_is_free	A step over crushed crop has a crop term of 0
presence_term_fix	With a presence term \(-P\) and \(P > w_E k\), the crop step loses under the energy bounds alone

The task uses \(P = 1\) and \(w_E = 0.3\). Thus the claim is true for \(k < 3.33\). The measured \(k\) is approximately 1.2.

Failures Never Pay

Proofs/FailureBound.lean proves the properties of the bounded reward over exact numbers. The map is \(B(r) = r\) for \(r \ge a\), and \(B(r) = a - k x / (x + k)\) with \(x = a - r\) and \(k = a - b\) below the knee \(a\). \(b\) is the floor.

Theorem	Statement
boundedReward_gt_floor	\(B(r) > b\) for each \(r\)
boundedReward_strictMono	\(B\) is strictly increasing
crop_never_pays_bounded	The comparison of presence_term_fix is true for the bounded reward
failure_never_pays	Each step reward is at least \(-c\). The failure penalty is \(F \le -c / (1 - \gamma)\). Then \(F \le \sum_{k<T} \gamma^k r_k + \gamma^T V\) for each \(T\) and each \(V \ge F\)
failure_never_pays_strict	With each step strictly above \(-c\) and \(T \ge 1\), the inequality is strict
bounded_v2_failures	The configured constants: knee −2, floor −5, \(\gamma = 0.995\), thus \(-5 / (1 - 0.995) = -1000\)
failure_never_pays_v2	The strict theorem with the configured constants

\(V\) is the value of the end after \(T\) steps. The end can be the same failure, a different failure or a success. It can also be the bootstrapped value of a time limit. The proof shows that one more step before the failure never decreases the return.

These theorems compare the penalty \(F\) alone with the continuation. The dense reward of the step with the failure is not in the comparison. Across different steps, a failure on a step with a positive dense reward can be worth more than a continuation at the floor (failure_pays_on_a_good_step). Residual Reward gives the statements that count each dense reward.

check.sh fails if rewards_bounded or gamma change. The differential test compares rewards.bound and the bounded variant with the model boundedStep, bit for bit.

Residual Law

Subject: the residual law. Model: Shield/Residual.lean. Proofs: Shield/Proofs/Residual.lean, over exact numbers.

In plain words. The residual can move the command only by a bounded amount. With a gain of 0, the command is the base command. The residual cannot change the direction of travel and cannot move a vehicle that the base command stops.

Property	Statement	Theorems
Gain	The law uses the gain after the clamp to \([0, 1]\)	residualGain_mem
Identity at zero gain	A gain at or below 0 gives the base command	compose_zero_gain, compose_of_gain_nonpos
Identity on doubles	For each double, with NaN and -0.0: a gain of 0 or a NaN gain gives the bits of the base command	compose_zero_gain_float, compose_nan_gain_float
Bound	For each action and each gain, each channel is within \(g \, \delta\) of the base command	compose_deviation, compose_deviation_gain
Speed bound	\(\lvert v - v_\text{PP} \rvert \le g \min(1.0,\; 0.3 \lvert v_\text{PP} \rvert)\)	residualCommand_deviation
Sign	The speed has the sign of the base speed. It is 0 where the base speed is 0	residualCommand_sign
Standstill	While the measured speed is below 0.3 m/s, the speed is the base speed	residualCommand_standstill
Action limits	The command after the clip is inside the actuator limits. For a base command inside the limits, it stays within \(g \, \delta\)	limited_mem, limited_deviation
Monotone	The deviation does not decrease when the gain increases. The command increases with the action	deviation_mono_gain, compose_mono_gain, compose_mono_action
Configuration	The configured ranges pass the check. The law reaches the bounds: gain 1 and action (1, 1) on 0.1 m⁻¹ at 4 m/s give 0.15 m⁻¹ at 5 m/s	wellFormed_rat, rangerResidualF_wellFormed, rangerResidual_example

Assumptions. The ranges are not negative. The sign property needs a share of the base speed below 1. The configuration check permits at most 0.5. The exact numbers have no NaN and no infinity. For doubles, the action clip gives a finite value in \([-1, 1]\) for each input (clip_fixed_mem).

Shield

Subject: the shield. Model: Shield/Shield.lean. Proofs: Shield/Proofs/Caps.lean, Clamp.lean, Meta.lean, Rules.lean, FloatFacts.lean and Framework.lean.

In plain words. The shield gives a command that satisfies each rule. It changes a command only when the command breaks a rule. It never increases the speed and never reverses it. These theorems are about the command. They are not about the motion of the vehicle.

Shield as a Function

The theorems are over the real numbers, for well-formed parameters.

Property	Statement	Theorems
No contradiction	For each input, the stop on the base curvature satisfies each enabled rule	stop_satisfies
Rules hold	The output satisfies each enabled rule	shield_satisfies
Least restriction	A proposal that satisfies each enabled rule is the output	shield_least_restrictive
Idempotence	The shield applied to its own output gives that output, with no intervention and no rule code	shield_idempotent
Intervention flag	The flag is true if and only if the output is different from the proposal	shield_intervened_iff
Flag and codes	The flag is true if and only if the output has a rule code	shield_intervened_iff_violated, shield_violated_eq_zero_iff
Never faster, never reversed	The output speed is between 0 and the proposed speed	shield_speed_between, shield_abs_speed_le
To the base curvature	The output curvature is between the base curvature and the proposed curvature	shield_curvature_between
Order of the rules	The order of the rules of one channel does not change the output	shield_speed_order_free, shield_curvature_order_free
Base command	The base command passes each rule but the obstacle rule	shield_base, shield_base_fixed
Forward speed	For a forward proposal, the output speed is the minimum of the proposal and the upper limits	shield_forward
No state	Equal inputs give equal outputs	shield_deterministic

Three theorems are for each scalar type, with Float.

Property	Statement	Theorems
Stop on unusable inputs	An input that is not usable gives the stop: speed 0 and code 64	shield_of_not_valid, shield_stop_of_not_finite, shield_stop_of_nan_obstacle
Flag as a comparison	intervened is !(k_out == k_in && v_out == v_in)	shield_intervened_eq
Output curvature	The output curvature is the result of the first call. It does not read the obstacle distance	shield_curvature_eq, shieldCurvature_independent

Rules

Rule	Statement	Theorems
Actuator limits	For each input, the output is inside the limits. The clip of spec.command_rows does not change it	shield_actuator, limited_shield
Geofence, forward	Outside the left fence, \(\kappa \le \kappa_b\). Outside the right fence, \(\kappa \ge \kappa_b\)	shield_geofence_forward
Geofence, backward	The rule exchanges the two sides	shield_geofence_backward
Geofence, speed	Outside the fence, the output speed is between 0 and \(v_b\)	shield_geofence_speed, shield_geofence_abs_speed
Geofence, sides	The vehicle is never outside the two fences at the same time	not_out_both
Corner	\(\lvert v \rvert \le\) the corner cap at the output curvature	shield_corner, cornerCap_le, cornerCap_ge_base
Corner, lateral acceleration	\(\lvert v \rvert \le \lvert v_b \rvert\), or \(\lvert v \rvert \le c\) and \(v^2 \lvert \kappa \rvert \le a_\text{lat}\)	shield_corner_lateral, shield_corner_framework
Corner, each proposal	\(v^2 \lvert \kappa \rvert \le \max\bigl(a_\text{lat},\; v_b^2 (\lvert \kappa_b \rvert + \lvert \kappa - \kappa_b \rvert)\bigr)\)	shield_lateral_bound
Obstacle	\(\lvert v \rvert \le \text{stopCap}(d_\text{obs} - d_m)\)	shield_obstacle
Obstacle, stop distance	The output speed is 0, or \(d_m + \text{stop}(\lvert v \rvert) \le d_\text{obs}\)	shield_stop_distance
Obstacle, largest speed	The rule passes each speed that can stop in the distance	obstacle_cap_greatest

The caps have their own theorems.

Statement	Theorems
\(\text{stopCap}(x)\) is the largest speed with \(\text{stop}(v) \le x\). At \(\text{stopCap}(x)\) the stop distance is \(x\)	le_stopCap_iff, stopDistance_stopCap
More room permits more speed	stopCap_mono
A speed within \(\sqrt{a_\text{lat} / k}\) on a curvature \(k\) has a lateral acceleration of at most \(a_\text{lat}\)	sq_mul_le_of_abs_le_sqrt
The parameters of the task are well formed. The check in the code is the assumption of the proofs	rangerR_wf, rangerF_wellFormed, wellFormed_iff
A list of clamps into intervals with a common point keeps each interval, in each order	clampAll_mem, clampAll_between, clampAll_of_mem, clampAll_idem, clampAll_perm
Without a common point, a clamp can leave an interval	clampAll_conflict

The theorems nominal_example and geofence_example show that the hypotheses can be true.

Doubles

The kernel evaluates these cases with the real doubles.

Case	Result	Theorem
NaN base curvature	Stop: curvature 0, speed 0, code 64	shield_nan_base
NaN cross-track error	Stop on the base curvature inside the limits	shield_nan_error
NaN or \(-\infty\) obstacle distance	Stop on the output curvature	shield_nan_obstacle, shield_neg_inf_obstacle
NaN proposal	The base command, an intervention, code 1	shield_nan_proposal
Proposed speed \(+\infty\)	The base speed, then the other rules	shield_inf_proposal
Obstacle distance \(+\infty\)	No obstacle interval. Safe with a reach of 30 m: \(1.5 + \text{stop}(6) = 27\) m	shield_no_return, no_return_is_safe
Fence at \(h = 3\) m	(3 - 0.8) - 0.3 and 3 - (0.8 + 0.3) are different doubles	fence_order
Stop distance of the cap at 20 m	20.000000000000004 m in doubles	stopCap_rounding
No latency and a subnormal room	The cap is 0, not \(+\infty\)	stopCap_underflow
Room near the largest double	The cap is 0 at \(8 \times 10^{307}\) m and NaN at \(10^{308}\) m	stopCap_overflow

Shield Assumptions

• The parameters are well formed (ShieldParams.wellFormed).
• The proofs are over the real numbers. For doubles, the evidence is the golden vectors and the cases above.
• The geofence theorems use the sign convention of mission.EpisodeTracker. The model does not include the frames.
• limited_shield is about the clip alone. The gear logic and the launch hold are not part of the statement.

Kinematics

Proofs: Shield/Proofs/Kinematics.lean.

These results are at the level of a model. Each theorem has explicit assumptions on the motion. No theorem proves these assumptions for the Ranger or for the simulator.

Result	Assumptions	Statement	Theorems
Brake distance	A brake run in discrete time with the step \(h\). The speed does not increase. From step \(L\), the speed decreases by at least \(a h\) in each step. In one step, the vehicle moves at most \(h\) times its speed at the start of the step	The vehicle moves at most \(v (L + 1) h + v^2 / (2a)\). It stands after \(L + \lceil v / (a h) \rceil\) steps	brake_distance, brake_stops
Stop before the margin	A brake run at \(a_b\) with \((L + 1) h \le \tau\). The obstacle does not move. The measured distance is a lower bound. The speed at the start is within the stop cap	The front of the vehicle stays at least \(d_m\) from the obstacle at each step	stops_before_margin, shield_stops_before_margin
Cap in closed loop	At each control step the speed is at most the last cap, or the vehicle brakes at \(a_b\). \(\tau \ge 4h\). The start is inside the envelope	The vehicle never passes the margin	capRun_never_passes
Cap without latency	\(\tau = 0\)	The vehicle passes the obstacle by 2 m in the example	capRun_counterexample
Fence, one step	The vehicle is inside the fence. The localisation error is at most \(\varepsilon\). The body is parallel to the path. The corridor is at least as wide as the two margins. The half width is the same at the next projection. \(\varepsilon + \text{swing} \cdot \lvert v \rvert \Delta t\) is at most the geofence margin	After one control step, the side of the vehicle is not outside the corridor edge	lateral_step, fence_one_step
Fence, one step and a stop	As above, then a brake run. The budget holds the control step and the stop distance	The side of the vehicle never passes the corridor edge	fence_stop
Margin of 0.3 m	No localisation error. The vehicle goes straight to the edge	One step fits up to 3 m/s for the rear axle and up to 2.2 m/s for a body point. It does not fit at 4 m/s. One step and a stop fit at 0.35 m/s and not at 0.4 m/s	fence_margin_numbers
Body point	Kinematic bicycle, \(\lvert \kappa \rvert \le 0.2\) m⁻¹, the plan box of the Ranger	A body point moves at most 1.35 times as fast as the rear axle	body_point_speed, ranger_swing
Path cap	The path points are in the order of the arc length. No limit is negative	A vehicle within the cap that brakes at \(a_c\) arrives at each later point at or below its limit	envelope_le, envelope_reaches
Arc side	Kinematic bicycle	A positive curvature moves the vehicle to its left, forwards and backwards	arc_lateral_sign

The theorems canon_brakeRun, stops_before_margin_example, canon_capRun, capRun_example, fence_one_step_example, fence_stop_example and envelope_example show that the assumptions can be true.

These limits apply.

• shield_stops_before_margin assumes that the vehicle obeys the command. The shield does not read the measured speed.
• The brake run has one dimension: the distance along the arc. The model does not include the arcs of later control steps.
• capRun_never_passes permits no actuation latency of more than one control step. No theorem covers the closed loop with a longer latency.
• The lateral theorems use the cross-track error of the rear axle. A heading error of 5° moves the front corner 0.3 m more to the side.

Stop Command Path

Proofs: Shield/Proofs/CommandPath.lean. The theorems use the queue theorems of Command Path and their assumptions.

Statement	Theorems
A stop command applies at the physics step where it is due. It stays applied while each later message is a stop	stop_reaches_ulc
The due step exists. With steps at most gap apart, it starts less than gap after the time of the message	due_step
While the controller sends, the watchdog age stays within the timeout at each step that applies the stop	stop_applied_while_engaged
The latency \(\tau = 0.5\) s holds the control period (0.1 s) and the wait for the due step (1/120 s and 1 ms). It also holds the delay of the ULC (0.03 s) and 0.36 s more	ranger_latency_budget
At the physics rate, the stop model permits 59 steps of latency	ranger_latency_steps

The theorems hyp_example, stop_reaches_ulc_example and stop_applied_while_engaged_example show that the assumptions can be true.

The 0.36 s is a remainder. It is not a measured value. These theorems do not say that the vehicle decelerates. The deceleration is an assumption of the brake run. A watchdog timeout is not a stop: the subsystem disengages, and the throttle and the brake release after the holdover of the ULC.

Mission Automaton

Subject: the mission automaton. Model: Mission/Automaton.lean. Proofs: Mission/Proofs.lean.

In plain words. Only an event changes the phase. Each mission ends after a bounded number of events. DONE occurs only after each loop and the stop at H.

Property	Statement	Theorems
Deterministic and total	Each state and each event have one next state	trans_iff_step, trans_deterministic, trans_total
States stay in the mission	An event keeps the field index below \(n\)	step_wellFormed
No deadlock	Each state that is not final has an event that changes it	no_deadlock
Failure	A failure ends each driving state	failure_ends
Final states	A final state has no exit	final_absorbing, run_final
Progress	An event that changes the state decreases the rank: by 1, or to 0 for a failure	step_rank, step_rank_failure, step_rank_lt
Bound	At most \(2n + 2\) events change the state. At most \(2n + 1\) of them are milestones	changes_le, milestones_le
Completion	The expected events go from IDLE to DONE in \(2n + 2\) events	run_expected
Leg index	An event that changes the state increases the leg index by 1. START keeps it 0. A failure is the exception	step_legIndex, legIndex_lt, legIndex_le
Rank and leg index	Rank plus leg index is \(2n + 1\) in the driving states and in DONE	rank_add_legIndex
Order, one step	SCOUT(i) starts only from GOTO(i) with ENTRY_REACHED. DONE starts only from RETURN with HOME_STOPPED. RETURN starts only after the last loop	scout_only_after_entry, done_only_after_home, returning_only_after_last_loop
Order, whole runs	A run in SCOUT(i) had an ENTRY_REACHED in GOTO(i). A run in DONE had a LOOP_CLOSED in the Scout state of each field and a HOME_STOPPED in RETURN	run_scout, run_done
Phase input	The phase code is below 6. The one-hot input has one bit in a driving state and no bit in the other states	phaseCode_lt, phaseOneHot_spec
Example	A mission of two fields, with and without a failure	two_field_example

Assumptions. The proofs have no numeric assumption. The automaton does not know the coverage. The contract of the HOME_STOPPED test gives "each field is scouted". The proofs do not cover the milestone tests that raise the events.

Reward Shaping

Subject: the shaping term \(F = \gamma \Phi(s') - \Phi(s)\). Model: Shaping/Model.lean.

In plain words. The shaping term changes each return by a number that depends only on the first state. Thus it changes no comparison of two futures and no optimal policy. This is true only with the correct rule at the end of an episode.

One Trajectory

Proofs: Shaping/Telescoping.lean. The theorems have no assumption on \(\gamma\), on the potential or on the trajectory. They are true in each commutative ring.

Property	Statement	Theorems
Telescoping	The shaped return of \(T\) steps is the unshaped return plus \(\gamma^T \Phi(s_T) - \Phi(s_0)\)	shaped_return_telescope
Terminal case	With \(\Phi(\text{terminal}) = 0\), the shaped return is the unshaped return minus \(\Phi(s_0)\)	shaped_return_terminal, shaped_return_episode
Truncation	With the real \(\Phi(s_T)\) and the bootstrap value \(V - \Phi(s_T)\), the shaped return is the unshaped bootstrapped return minus \(\Phi(s_0)\)	shaped_boot_return
Critic error	A bootstrap value that is wrong by \(\varepsilon\) changes the shaped return by \(\gamma^T \varepsilon\)	shaped_boot_return_critic_error
Comparison	Two futures from one state keep the difference of their returns and their order	shaping_preserves_comparison, shaping_preserves_le, shaping_preserves_lt
PPO targets	With the critic \(V - \Phi\), the temporal-difference residuals and the advantage estimates are the unshaped ones	td_residual_shaped, gae_shaped
One discount	A shaping term with a different discount leaves a term that depends on the whole trajectory	shaped_return_gamma_mismatch
Wrong rule: \(\Phi(s_T) = 0\) at a truncation	The return has a bias \(-\gamma^T \Phi(s_T)\). The order of two trajectories can reverse	shaped_boot_terminal_convention, terminal_convention_at_truncation_reverses
Wrong rule: no bootstrap at a truncation	The order of two trajectories can reverse	no_bootstrap_reverses

Decision Process

Proofs: Shaping/Mdp.lean. The theory is for a finite Markov decision process with \(0 \le \gamma < 1\) and stationary policies. The values are the fixed points of the Bellman operators (evalOp_contracting, optOp_contracting, value_unique, optValue_unique).

Property	Statement	Theorems
Policy evaluation	For each policy: \(V' = V - \Phi\) and \(Q'(s, a) = Q(s, a) - \Phi(s)\). The advantages are equal	value_shape, qValue_shape, advantage_shape, q_shape
Policy invariance	\(Q'^*(s, a) = Q^*(s, a) - \Phi(s)\). The greedy actions are the same. A policy is optimal for the shaped process if and only if it is optimal for the unshaped process	optValue_shape, optQ_shape, isGreedy_shape, isOptimal_shape
Optimal has a meaning	No stationary policy is worth more than \(V^*\). An optimal policy exists	value_le_optValue, exists_isOptimal
Objective	The objective of each policy moves by a constant. The order of each two policies stays	objective_shape, objective_shape_le_iff
\(n\) steps with a bootstrap	\(n\) steps of the shaped process with the end value \(V - \Phi\) are \(n\) steps of the unshaped process with \(V\), minus \(\Phi\)	optOp_shape_iterate
\(n\) steps without a bootstrap	The shaped process with the end value 0 is the unshaped process with the end value \(\Phi\). The best action can change	optOp_shape_iterate_zero, finite_horizon_counterexample
Terminal state	A terminal state is worth 0. In the shaped process it is worth \(-\Phi\). Thus \(\Phi(\text{terminal})\) must be 0	optValue_absorbing, optValue_shape_absorbing
Bounds	\(\lvert r \rvert \le R_\text{max}\) gives \(\lvert V \rvert \le R_\text{max} / (1 - \gamma)\)	abs_value_le, abs_optValue_le
Limit	The values are the limits of the \(n\)-step values	tendsto_iterate_value
Example	A process with two states, with its optimal values with and without shaping	twoStateMDP_optValue, twoStateMDP_shaped

Potential of the Task

Proofs: Shaping/Potential.lean, over exact numbers.

Property	Statement	Theorems
Table	The table \(N_\text{ref}\) of the specification is well formed. Its total is the reference time of the episode in control steps	costToGoOfSteps_wellFormed, costToGoOfSteps_total
Cost-to-go	\(N_\text{ref}\) is never negative, is at most the total, does not increase with the arc length and is 0 at and after the last point	remaining_isCostToGo
Potential	\(-c_\Phi N_\text{total} \le \Phi \le 0\). \(\Phi = 0\) at the end of the path. \(\Phi\) does not decrease when \(s^*\) increases	potential_bounded, potential_goal, potential_mono
Term of one step	\(F = c_\Phi (N - N') + (1 - \gamma) c_\Phi N'\)	shaping_term_eq
Term at a termination	\(F = c_\Phi N\)	shaping_term_terminal
Term without progress	\(F = (1 - \gamma) c_\Phi N\). It is not 0	shaping_term_standing
Common term	A standing step and a driving step from one progress point have the term \((1 - \gamma) c_\Phi N\). The shaping adds \(\gamma c_\Phi (N - N')\) to their difference	shaping_term_common, shaped_step_difference
Bounds of the term	\(0 \le F \le c_\Phi N_\text{total}\)	shaping_term_nonneg, shaping_term_le, shapingStep_term_bounds
Progress point	\(s^*\) never decreases	advance_ge, progress_mono
Augmented state	The term that the code calculates is \(\gamma \Phi(a') - \Phi(a)\) for one potential of the augmented state	shapingStep_eq_aug
Not a function of the position	Two histories that end at the same arc length can have different potentials	potential_not_function_of_position, no_potential_of_position
Mission return	The shaped return of an episode that terminates is the return plus \(c_\Phi N_\text{ref}(s^*_0)\)	shaped_return_mission

Augmented State

Proofs: Shaping/Augmented.lean. The process has the state \((x, p)\): the simulator state and the progress. The potential is 0 in a terminal state.

Statement	Theorems
The shaped reward of this process is the term that the code calculates	augmented_shape_reward
The invariance theorems are true for this process	augmented_optQ_shape, augmented_isGreedy_shape, augmented_isOptimal_shape, augmented_advantage_shape, augmented_objective_shape
A terminal state is worth 0 in the shaped process	augmented_terminal_value

Assumptions. The process is finite. The progress is a finite type in the proof and a real number in the task. The policies are stationary. The critic of the shaped problem estimates \(V(x, p) - \Phi(p)\). Thus its input must determine \(\Phi(p)\).

Residual Reward

Subject: the reward of the residual variant. Model: Reward/Residual.lean. Proofs: Reward/ResidualProofs.lean, Reward/FailureEvent.lean, Reward/Spec.lean and Reward/FloatFacts.lean.

In plain words. A failure is never the better end. A step in crop is never the better step. A stop is better than a failure, and a drive in the lane is better than a stop. The shaping term changes none of these statements.

Property	Statement	Theorems
Formula	The sum of the model is \(B(d) - w_s 1_\text{intervention} + e + F\)	residualReward_eq
Floor	A step is above \(-5 - w_s = -5.5\) before its events and its shaping term	penaltyOutside_gt
Numbers	\((-5 - 0.5) / (1 - 0.995) = -1100\); \(-1200 \le -1100\); \(36.75 + 50 - 1200 = -1113.25 < -1100\); −1150 fails; \(-1500 \le -1200\)	spec_failure_inequalities, penalty_outside_needs
Failure penalty alone	The penalty now is worth less than \(T \ge 1\) more steps and an end worth at least \(F\)	failure_never_pays_residual, failure_never_pays_residual_v2, spec_failure_never_pays
Failure, like for like	The same-step comparison assumes non-negative continuation events and a final value of at least \(F - 5.5\)	failure_event_never_pays, failure_event_never_pays_residual, spec_failure_event_never_pays
Failure against each continuation	A step with a failure, with its dense reward and a milestone, is worth less than each continuation without a failure	failure_never_pays_against_safe, failure_never_pays_cross_step_residual, spec_failure_cross_step
Largest dense step	Within the limits of a step, the dense reward is at most 36.75	dense_le_of_limits
Condition is exact	Without a lower bound on the dense reward, a penalty \(p\) after the map needs \(F \le (-5 - p) / (1 - \gamma)\)	penalty_outside_exact, failure_needs_margin
Crop never pays	A step in crop earns less than the clean lane step of the same progress. This is true with and without an intervention in the crop step	crop_never_pays_residual, crop_never_pays_residual_v2, spec_crop_never_pays
Standing step	A step without progress earns at most −0.25 before the bound	standing_step_le
Lane step	A clean lane step with at least 0.4 m of progress and at most the reference energy earns at least +0.45	clean_step_reward, lane_step_ge
Order of the returns	failure < stop < lane, with the measured steps, with and without shaping	stall_drive_fail_order, attractor_order_measured, attractor_order_shaped, spec_attractor_order
Step by step	The shaped driving step is above the shaped standing step from the same progress point	spec_drive_step_gt_stand_step, spec_shaped_step_difference
Shaped stop	The shaped step of a stop is \(-0.31 + 0.00275 N_\text{ref}\). It is positive above 1240/11 reference steps	spec_standing_step_shaped
Shaped failure	The step of a failure carries \(-1200 + 0.55 N_\text{ref}\). It is positive above 24000/11 reference steps	spec_failure_step_shaped
Truncation	With the bootstrap value \(V + 0.55 N_\text{ref}(s^*_T) + \varepsilon\), the shaped return is the unshaped return plus \(0.55 N_\text{ref}(s^*_0) + \gamma^T \varepsilon\)	spec_truncation
End of a segment	The potential at the end of a segment is not 0	spec_segment_end_potential
Potential	\(-0.55 N_\text{total} \le \Phi \le 0\)	spec_potential_bounds
Bounds	\(\lvert r' \rvert \le \max(1505.5,\; D_\text{max} + e_\text{hi} + 0.55 N_\text{total})\). Bounded rewards give bounded returns	spec_reward_bound, residual_model_bounds, discounted_tsum_bound
Shaping keeps the order	Two futures from one state keep their order with the shaping term	shaping_keeps_order

Assumptions.

• The proofs are over exact numbers.
• The limits of one control step are hypotheses from the code: at most 14 m of progress and at most 4 new checkpoints (StepLimits). A step with a failure pays at most one milestone of at most 50.
• The measured steps are hypotheses: a stop earns −0.31 and the lane earns at least +0.45 (MeasuredSteps).
• The crop theorem needs \(k < 10/3\) for the energy of the lane step. The measured \(k\) is approximately 1.2. The crop step covers no new checkpoint. The two steps have the same shaping term.
• The crop theorems and the standing-step theorems compare two steps. They do not compare two routes.

Doubles. The kernel evaluates the bounded map on named doubles (Reward/FloatFacts.lean).

Case	Result	Theorem
Knee (−2), stop (−0.31), lane (0.45)	Unchanged, bit for bit	bounded_unchanged
−29 and −50	Above the floor and in the correct order	bounded_measured
Two adjacent doubles near −25.49	The smaller value has the larger result, by \(4 \times 10^{-15}\)	bounded_not_monotone
\(-10^6\) and \(-10^8\)	Above the floor	bounded_above_floor_to_1e8
\(-10^9\)	Exactly −5	bounded_reaches_floor
\(-10^{17}\)	0	bounded_cancels

Planner

Subject: solvers.exact_dp. Model: Planner/Model.lean (solve). The model follows the code cell by cell. It keeps the first minimum on a tie, as the code does.

Optimality

Proofs: Planner/Optimality.lean and Planner/CodeCost.lean, over exact numbers.

In plain words. The dynamic programme returns a plan that visits each requested field one time. No feasible plan costs less. It returns no plan only if no feasible plan exists.

Property	Statement	Theorems
Exact	The returned plan is a plan of the mission, is feasible and has the returned cost. No feasible plan costs less	solve_optimal, solve_isLeast, solve_feasible
No plan	The programme returns no plan if and only if no plan is feasible	solve_eq_none_iff
Reported cost	The cost that OptionGraph.cost reports is the cost of the plan. The order of numpy.sum gives the same sum	codeCost_eq_planCost, solve_codeCost, npSum_eq_sum

Assumptions. The theorems have no assumption on the tables. The costs can be negative, zero or equal.

Regret

Proofs: Planner/Regret.lean and Planner/RegretTight.lean.

In plain words. If each table entry is wrong by at most \(\varepsilon\), the plan from the wrong table costs at most \(2 L \varepsilon\) more than the optimum. \(L = 2n + 1\) is the number of entries that a plan reads.

Property	Statement	Theorems
Cost of one plan	The two costs of a feasible plan differ by at most \(L \varepsilon\)	abs_planCost_sub_le
Regret bound	The plan that is optimal for the estimate costs at most the optimum plus \(2 L \varepsilon\)	regret_bound, regret_bound_solve
Tight	An example reaches the bound for each number of fields	regret_bound_tight, regret_bound_tight_family
Relative error	With entries within the fraction \(\rho < 1\), the plan costs at most \((1 + \rho) / (1 - \rho)\) times the optimum	regret_bound_relative, relative_regret_bound
General fact	A decision that minimises an estimate within \(\delta\) is within \(2\delta\) of each decision	regret_of_uniform_error

Assumptions. The estimate and the true table have the same shape: the same fields, options and removed entries. The relative bound needs true entries that are not negative. The proofs do not model how a model error becomes a table error.

Checker

Proofs: Planner/Checker.lean.

In plain words. The checker accepts a proposal if and only if the proposal is a feasible plan of the mission. A plan from a source that is not trusted must pass the checker.

Property	Statement	Theorems
Sound and complete	The checker accepts a proposal if and only if the proposal is valid. This is true for each scalar type	checkProposal_iff, checkProposal_sound, checkProposal_complete
Valid means feasible	For a well-formed mission, the valid proposals are the feasible plans	validProposal_iff_isPlan
Mission test	Mission.checkWellFormed is true if and only if the mission is well formed	checkWellFormed_iff
Optimal plan	The plan of the dynamic programme passes the checker	solve_passes_check
Cost	An accepted plan costs at least the optimum	checked_cost_ge_optimum
Condition	Without a well-formed mission, the checker can accept a list that is not a plan	check_needs_wellFormed

Assumptions. The mission must pass Mission.checkWellFormed before the code uses the checker. No proof shows that the mission from an OptionGraph passes that test.

Findings

The proofs and the differential tests found these problems.

First Development

No.	Finding	State
1	A NaN action reached the drive-by-wire as a NaN curvature and a NaN speed	Fixed in spec.action_to_command and in the environment
2	The watchdog of the game trips one step before the watchdog of ACRES Core (12 against 13 steps)	Open. The two satisfy the specification
3	The messages of the first read all apply at one step. A long first frame then causes one timeout: 27 of 250 steady sessions in the test	Open
4	The queue bound is for each due time, not for each due step	Open. Not a hazard: the queue drains at each step
5	A NaN due time blocks the queue (nan_blocks_queue)	Open. No caller makes a NaN time
6	Crop can pay under the energy bounds alone	Fixed by the presence term \(P = 1\)
7	The last bit of the reward depends on the platform: pow(x, 2.0) of libm, the fused ddot of OpenBLAS, the compensated sum of CPython 3.12	Open. It affects only bit-exact replays between machines

The proposals for the open findings are:

• Finding 2. Give StepDbw the exact step, or count the ages in steps.
• Finding 3. Map the first read as if the read before it was one frame earlier.
• Finding 4. Merge a push into the last entry when the two are due at the same physics step.
• Finding 5. Read a NaN time as ApplyAtNextStep in Push.

One part of the crop claim stays open. The proofs compare single steps. They do not cover a corner cut over a whole route.

First Specification of the Shield

The first specification of the shield is the text of this documentation before the Lean model. The file Shield/Proofs/Framework.lean models that text (firstShield) and proves each error by a counterexample. The Framework has the corrected rules.

No.	Finding	Theorems	Correction
8	A NaN base curvature gave a NaN output curvature. The property "Limits" was false	first_nan_base	Rule 0: a stop
9	A NaN cross-track error switched the geofence off, with no flag	first_nan_error	Rule 0: a stop
10	On a backward stretch the geofence acted on the wrong side. It replaced the curvature that steers back and passed the curvature that steers out	first_backward_geofence, shield_backward_geofence	The input direction. A backward stretch exchanges the sides
11	Outside the fence, a proposal against the direction of the base command passed: −1 m/s with a base speed of 2 m/s	first_against_base	The speed is between 0 and \(v_b\)
12	The corner cap \(\max(c, \lvert v_\text{PP} \rvert)\) did not bound the lateral acceleration. 0.15 m⁻¹ at 4.8 m/s passed with 3.456 m/s² against the limit 1.5 m/s²	first_corner_lateral, shield_corner_example	The cap reads the output curvature
13	The ladder of speed factors is not monotone. At 10 m, 4.4 m/s gives 3.3 m/s and 4.5 m/s gives 2.25 m/s	ladder_not_monotone	The exact stop cap
14	The ladder does not give the largest safe speed. At 10 m, 4 m/s gives 3 m/s, but 3.3 m/s can stop	ladder_not_maximal, ladderPick_le_stopCap	The exact stop cap
15	The corner rule read the proposed curvature. A later curvature rule can then break the corner rule	corner_before_curvature_counterexample	The speed rules read the output curvature
16	The obstacle distance was for the proposed curvature, not for the curvature that the vehicle drives	shield_curvature_eq	Two calls: shield_curvature, then shield
17	The first specification assumed a base command inside the actuator limits. Outside the limits, the rules can contradict each other	baseCurvature_mem, baseSpeed_mem, stop_satisfies, clampAll_conflict	The shield uses \(\kappa_b\) and \(v_b\)
18	The rule for a bad proposal named only NaN. An infinite value is also unusable	shield_inf_proposal	Rule 1 is for each value that is not finite
19	The intervention had no exact definition	shield_intervened_eq	The IEEE comparison of the two commands

The ladder has two good properties: it is idempotent and it passes a safe speed (ladderPick_idempotent, ladderPick_fixed, ladderPick_stop). The two findings above are the reason for the change.

First Specification of the Residual Law

No.	Finding	Theorems	Correction
20	base + 0 * x is not the base command bit for bit. A base speed of -0.0 becomes +0.0	add_zero_loses_sign	A gain that is not above 0 returns the base command itself
21	The law had no rule for a gain outside \([0, 1]\) or a NaN gain	residualGain_mem, compose_nan_gain_float	The law clamps the gain. A NaN gain is 0
22	With a NaN measured speed, NaN < 0.3 is false. The range was then min(1.0, NaN)	Definition speedRange	The range is 0 if a speed is not finite
23	With a share of the base speed above 0.5, the doubles lose the sign at the smallest subnormal base speed	wellFormed_rat, residualCommand_sign	The configuration check permits at most 0.5
24	A clip before the shield hides a proposal outside the actuator limits from the shield	limited_mem, limited_shield	The law does not clip. The clip is at the end of the command path

Corrected Shield

No.	Finding	Theorems	Effect
25	(h - 0.8) - 0.3 and h - 1.1 are different doubles at \(h = 3\) m	fence_order	The code must use the order of the specification
26	In doubles, the stop distance of the cap at 20 m is 20.000000000000004 m	stopCap_rounding	A test must compare the speed with the cap, or use a tolerance of \(10^{-12}\) m
27	The first version of stopCap gave \(+\infty\) for no latency and a subnormal room. A fuzz test found it	stopCap_underflow	The cap is 0 when the denominator is 0
28	Above \(10^{307}\) m of room, the arithmetic of the cap overflows	stopCap_overflow	No effect: the scan reports at most 30 m or \(+\infty\)
29	The speed after the shield is not monotone in the gain	shielded_speed_not_monotone_in_gain	A larger gain is not always a faster command
30	With a cap without latency, the vehicle passes the margin in closed loop	capRun_counterexample	The closed-loop theorem needs \(\tau \ge 4h\)
31	The geofence margin of 0.3 m holds one control step only up to 3 m/s. One step and a stop fit only below 0.35 m/s	fence_margin_numbers	The geofence limits the command. It does not hold the vehicle in the corridor by braking

Automaton Events

No.	Finding	Theorems	Correction
32	The result depends on the order of two events in one control step. HOME_STOPPED then FAILURE gives DONE. The other order gives FAILED	final_absorbing, failure_ends	The code gives FAILURE first
33	The automaton cannot prove "done only after each field is scouted". LOOP_CLOSED means only that the vehicle is at the entry again	run_done, done_only_after_home	HOME_STOPPED must be the completion test
34	The rank uses the subtraction of natural numbers	Golden files mission_*.json	The code uses max(n - i, 0)

Reward and Shaping Rules

No.	Finding	Theorems	Correction
35	Inside the bounded map, the shield penalty of 0.5 is worth 0.005 at a dense reward of −29	intervention_cost_small, intervention_cost_above_knee	The reward subtracts the penalty after the map
36	With the penalty after the map, failures at −1000 can pay. One more step at −29 with an intervention, then the failure, is worth −1000.2	penalty_outside_counterexample, penalty_outside_v2, penalty_outside_exact	Failures −1200, collision −1500
37	The sentence "no failure is worth more than a continued drive" is false across different steps. A failure on a step at +0.45 is worth −999.55. A continuation at −4.999 is worth −999.8	failure_pays_on_a_good_step	The like-for-like statement and the second inequality with \(D_\text{max}\)
38	\(\Phi(s_T) = 0\) at a truncation reverses the order of two trajectories	terminal_convention_at_truncation_reverses	The real potential and the shaped bootstrap value
39	A truncation without a bootstrap reverses the order of two trajectories	no_bootstrap_reverses, finite_horizon_counterexample	PPO bootstraps at each truncation
40	The potential is not a function of the vehicle position	no_potential_of_position	The state of the proof is the augmented state. The critic gets \(N_\text{ref}\)
41	The first specification gave \(\Phi = 0\) at the end of the episode path. At the end of a segment the potential is not 0	spec_segment_end_potential	The truncation rule applies at the end of a segment
42	The shaping term of a stop is positive: \(0.00275 N_\text{ref}\) for each step	shaping_term_standing, spec_standing_step_shaped	No change. The order of the returns stays (spec_attractor_order)
43	The step of a failure can be positive: \(-1200 + 0.55 N_\text{ref}\), above 2182 reference steps	spec_failure_step_shaped	No change. The statements about returns stay
44	The shaping term must use the discount of the return	shaped_return_gamma_mismatch	rewards.gamma must be equal to ppo.gamma
45	In doubles the bounded map is not monotone, reaches the floor at \(-10^9\) and gives 0 at \(-10^{17}\)	bounded_not_monotone, bounded_reaches_floor, bounded_cancels	No change. The values are outside the range of the task, except the rounding of \(4 \times 10^{-15}\)

Planner Code

No.	Finding	Theorems	State
46	solvers.exact_dp raises ValueError for a mission without fields. The model gives the empty plan with cost 0	solve_optimal; differential test	Open in the code. The callers handle that mission before the call
47	The checker can accept a list that is not a plan if the mission is not well formed	check_needs_wellFormed	The code must run Mission.checkWellFormed first
48	An example reaches the regret bound \(2 L \varepsilon\) through a tie in the estimate	regret_bound_tight, regret_bound_tight_family	The bound cannot be smaller

Input Code of the Shield

These findings are about code that exists. This work did not change the code. Known Problems lists them for the code phase.

No.	Location	Finding
49	mission.EpisodeTracker._project	Near a change of direction, the projection can be on a different stretch than the base driver
50	mission.corridor	The tangent is wrong at the stop point of each change of direction. The half widths there are 8.0 m or 0.0 m
51	spec.LaunchHold	The launch hold runs after the gear logic. Its speed command can be larger than the output of the shield
52	Map products	On 30.7 % of the Scout path points, at least one side has a fence of 0. On 18.4 %, the two sides have a fence of 0

Differential Tests

Verification/Differential/run_differential.py generates the inputs of the first four rows.

Component	Inputs	Compared	Result on 2 October 2026
Command path	1000 sessions: frames of 4 ms to 2 s, pauses, lockstep, stops, other modes, disable and enable	1,533,411 events; 452,709 physics steps	Identical. The traces also satisfy the theorems (see below)
Gear logic	4000 vehicles: random walks through the band and the standstill limit, exact limits, NaN, ±∞	434,096 calls; 5801 shifts	Identical
Action map	Uniform, near ±1, subnormal, ±0, large, ±∞, NaN	14,060 actions	Identical
Step reward	Random steps, each term	10,000 steps	Identical, with one ulp on 3 steps (finding 7)
Bounded reward	Random steps of variant="bounded"; special values of rewards.bound	5000 steps; 1268 values; 14 golden values	Identical, with one ulp on 1 step
numpy.interp	Random knots, queries on and between the knots, NaN, infinities	9552 queries	Identical
Reference time	The table of the model against deploy.mission.path_time_s	20 paths	Largest relative difference \(8.4 \times 10^{-16}\)
Planner	Golden instances and random tables against solvers.exact_dp and OptionGraph.cost	53 instances; 500 random tables	The same plan, tie by tie, and the same cost bits
Planner regret	Golden cases against solvers.exact_dp	8 cases	Each regret is within the bound. The largest is 0.141 of its bound

The traces of the command path satisfy the theorems:

• No timeout occurs in 160,742 steps under a controller that sends each 20 ms or less.
• Each of 249 silent controllers disengages at step 12 (game step) or step 13 (Core step).
• Each of 434 pauses adds at most two entries.

The C++ side is dbw_harness. The check script compiles it from AcresCommandTiming.h and AcresUtvModel.cpp of the game. The Python side calls spec.py, rewards.py, planners/solvers.py and planners/options.py directly.

Golden-Vector Contract

The production code of the framework must pass these files. The Lean executables write them. The check script writes them again at each run and fails if a file is different.

File	Content	Executable
shield_boundary.json	93 curated cases with notes; 1200 cases near the limits of each input	acres_shield
shield_random.json	3650 random cases with ten parameter sets	acres_shield
shield_residual.json	27 curated and 1500 random cases of the residual law and of the action limits	acres_shield
mission_boundary.json	3124 cases: each sequence of 1 to 4 events for missions of 0 to 3 fields, and the expected sequences	acres_shield
mission_random.json	1500 random sequences for missions of 0 to 8 fields	acres_shield
shaping_potential.json	220 shaping steps on 8 tables	acres_golden
shaping_returns.json	12 episodes with their shaped and unshaped returns	acres_golden
reward_residual.json	49 steps of the residual reward with each term	acres_golden
reward_bounded.json	14 values of rewards.bound	acres_golden
planner_instances.json	53 instances with the optimal plan and its cost	acres_golden
planner_regret.json	8 cases of the regret bound	acres_golden
planner_checker.json	16 proposals with the answer of the checker	acres_golden

The files are in Verification/Differential/golden/.

These rules are the contract.

1. The residual law and the shield must give the bits of each golden case. The shield files hold each double as 16 hexadecimal digits.
2. Each shield case has the 10 inputs in this order: curvature_per_m, speed_mps, base_curvature_per_m, base_speed_mps, cross_track_m, half_left_m, half_right_m, direction, path_cap_mps, obstacle_m.
3. The outputs are curvature_per_m, speed_mps and shield_curvature_per_m, and the flags intervened and violated. shield_curvature_per_m is the result of the first call.
4. The code must write the comparisons as the oracles do: std::clamp, std::min and std::max. The golden cases with -0.0 fix the result for signed zeros.
5. The automaton must give the phase, the field, the leg index and the rank after each event of each sequence.
6. The residual reward must add the terms in the specified order with the sum of Python. Bind the function to PRODUCTION_RESIDUAL in reward_differential.py.
7. The shaping term must pass the 220 steps. Bind the function to PRODUCTION_STEP in shaping_differential.py.
8. The plan checker must pass the 16 proposals. Bind the function to PRODUCTION_CHECK in planner_differential.py. The mission must pass the test of Mission.checkWellFormed first.

shield_reference.py and mission_reference.py are test oracles. They are not the production code. The check script proves nothing about the production code until that code exists and is bound to the tests.

shield_check.py also tests the claims of the theorems on the doubles of each golden case:

• The output satisfies each rule.
• The shield is idempotent.
• A safe proposal passes.
• The flag agrees with the rule codes.
• The speed is between 0 and the proposal.

Not Proved

• The neural network. No theorem is about the policy. The bounds are about the law that scales its output.
• The motion of the vehicle. The shield theorems are about the command. The kinematic results have explicit assumptions that no theorem proves for the Ranger or the simulator.
• The deceleration of a stop. The value \(a_b = 0.8\) m/s² and the brake run are assumptions.
• Perception and localisation. The pose, the map, the half widths and the LiDAR scan are trusted inputs. The geometry of the swept corridor has no Lean model.
• The code of the framework. The residual law, the shield, the automaton module, the residual reward, the shaping term and the plan checker do not exist as production code.
• Model against code. The differential tests and the golden vectors give evidence. They are not a proof.
• Doubles. Most proofs are over exact numbers. For doubles, the proofs cover named cases and the properties in Method.
• The shaping theory for the real task. The proof is for a finite process and stationary policies. It does not cover continuous states, policies that depend on the history or an expectation over infinite trajectories. No proof covers the converse of the invariance theorem.
• The quality of the critic. The truncation result is exact only for an exact critic.
• The limits of one control step. The 14 m of progress, the 4 checkpoints and the one milestone are hypotheses from the code.
• The measured steps. The stop at −0.31 and the lane at +0.45 or more are measured values.
• The planner in doubles. The proofs are over exact numbers. The differential test compares the doubles.
• The tables of the planner. No proof covers the construction of the tables, OR-Tools or the geometry.
• The plan checker. It does not check the access and exit points, the time limit, the geofence or the geometry.
• The milestone tests. No proof covers the code that raises the events of the automaton.
• The first audit file. Audit.lean lists 56 of the 155 theorems of Proofs/.

Trusted Base

A proof is as good as the items that it must trust.

Item	Trust
The Lean kernel and the three standard axioms	Trusted
Mathlib	Checked by the kernel
The facts on doubles in the FloatFacts.lean files	Checked by the kernel. No trust in the compiler
The compiled acres_model, acres_shield and acres_golden	Trusts the Lean compiler and the C compiler for float operations
The agreement of model and code	Evidence from the differential tests and the golden vectors. Not a proof
The test oracles shield_reference.py and mission_reference.py	Checked against the Lean executable on the golden files and on fresh inputs
numpy, libm, OpenBLAS, CPython	Modelled by helper functions. Finding 7 gives the known differences
The specification	The theorems prove the stated properties. A person must judge if the properties are the correct ones
Assumptions A1 to A4	Stated, not proved
The hypotheses StepLimits, MeasuredSteps and the brake run	Stated, not proved
Sensors, map, localisation, vehicle dynamics	Outside the models
Neural networks	Outside the models

Files

Path	Content
Verification/AcresVerification/Scalar.lean	The scalar helpers
Verification/AcresVerification/*.lean	The models: CommandTiming, Watchdog, GearManager, ActionMap, Rewards
Verification/AcresVerification/Proofs/*.lean	The proofs: Queue, Clock, CommandPath, FloatFacts, GearManager, ActionMap, Rewards, FailureBound, Links
Verification/AcresVerification/Shield/	Residual.lean and Shield.lean (models); Proofs/
Verification/AcresVerification/Mission/	Automaton.lean (model); Proofs.lean
Verification/AcresVerification/Shaping/	Model.lean; Telescoping.lean, Mdp.lean, Potential.lean, Augmented.lean
Verification/AcresVerification/Reward/	Residual.lean (model); ResidualProofs.lean, FailureEvent.lean, Spec.lean, FloatFacts.lean
Verification/AcresVerification/Planner/	Model.lean; Optimality.lean, CodeCost.lean, Regret.lean, RegretTight.lean, Checker.lean
Verification/Main.lean, ShieldMain.lean, Golden.lean	The executables acres_model, acres_shield and acres_golden
Verification/AuditAll.lean, audit_project.py	The complete project-constant audit
Verification/Audit.lean, AuditShield.lean, AuditFramework.lean	Named theorem lists
Verification/mutation_tests.py	Deliberate-failure tests in a temporary copy
Verification/Differential/reward_assumptions.py	Reward configuration and map checks
Verification/Differential/	dbw_harness.cpp, run_differential.py, shield_check.py, mission_check.py, shaping_differential.py, reward_differential.py, planner_differential.py, the two test oracles
Verification/Differential/golden/	The 12 golden files
Verification/check.sh	The check script

Proofs/Links.lean connects the abstractions of the proofs to the executable definitions. These are the queue and clock calls of DbwPath, the fresh flag, the age, the enabled flag and the action map over ℚ.