Formal Verification

The folder Verification/ holds a Lean 4 development. It models parts of the vehicle software, proves properties of the models and tests the models against the C++ code. This page gives what the proofs say, how they connect to the code, what they do not cover, and how to run the checks.

What the Proofs Cover

Inputs	Outputs
The Lean models: shield, speed envelope, trajectory checker, planner, plan checker, command path, gear logic, mission automaton	Theorems over exact numbers (\(\mathbb{Q}\), \(\mathbb{R}\)) and named cases over doubles
The C++ run-time library and the command path of the game	Evidence that the code does what the model does: differential tests, golden vectors, a constants check, an axiom audit

The proofs are about the Lean models. Four checks connect the models to the C++ code. The moving dashes show the direction of the evidence. Open the diagram

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	acres_runtime_gear (Runtime/Source/command_chain.cpp)	GearManager.lean	Proofs/GearManager.lean	Differential test
Command row	acres_runtime_command_row (command_chain.cpp)	ActionMap.lean (commandRowsClip)	Shield/Proofs/CommandRow.lean	Differential test
Shield	acres_runtime_shield, acres_runtime_shield_curvature (shield.cpp)	Shield/Shield.lean	Shield/Proofs/	Golden vectors, bit for bit. Differential test
Speed envelope	detail::envelope_entry, acres_runtime_worst_limits, acres_runtime_effective_level	Shield/Envelope.lean	Shield/Proofs/Envelope.lean, Trajectory/Envelope.lean	Golden vectors
Mission automaton	acres_runtime_automaton_step, detail::automaton_leg (tracker.cpp)	Mission/Automaton.lean	Mission/Proofs.lean	Golden vectors. Differential test
Interpolation	detail::interpolate	Interpolation.lean (npInterp)	None	Differential test
Planner	acres_runtime_planner_solve (planner.cpp)	Planner/Model.lean (solve)	Planner/Optimality.lean, CodeCost.lean, Regret.lean, RegretTight.lean	Differential test. Golden vectors
Plan checker	acres_runtime_plan_check, acres_runtime_plan_check_mission (plan_check.cpp)	Planner/Model.lean (checkProposal)	Planner/Checker.lean	Golden vectors. Differential test
Trajectory checker and tube test	acres_runtime_check_items, acres_runtime_tube: the compiled Lean model in the checker plug-in (Runtime/Lean/)	Trajectory/Model.lean (check, tubeCheck)	Trajectory/Proofs.lean, Geometry.lean, Turn.lean, Tube.lean. Fast.lean (the fast forms that the run-time library compiles), Raster.lean (the bounds of the corridor rasters)	Golden vectors. Differential test. Corridor and Checker

The Lean files are in Verification/AcresVerification/. The C++ files of the library are in Runtime/Source/.

How It Works

Method

1. One model for each component. Each model follows the 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, std::min, numpy.clip and numpy.interp, which the C++ code follows.
2. A model before the code. For the shield, the mission automaton, the plan checker and the trajectory checker, the Lean model is the specification. The code 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, command row
   acres_shield	ShieldMain.lean	Shield, mission automaton
   acres_golden	Golden.lean	Planner, plan checker, trajectory checker, speed envelope, interpolation

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 the permitted axioms. 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 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 (Shield/Proofs/FloatFacts.lean).

Command Path and Gear Logic

The command path and the gear logic have these theorems.

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

Shield

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, not about the motion of the vehicle. Vehicle Software gives the rules.

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 of the Shield

Rule	Statement	Theorems
Actuator limits	For each input, the output is inside the limits. The clip of the command row 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.

Worked Example

The theorem no_return_is_safe says that a scan with no return needs no speed limit. Each entry of the speed envelope must stop inside the reach of the scan, 40 m. For the fastest entry (7.8 m/s on asphalt, \(d_m = 2.5\) m, \(T = 1.0\) s, \(a = 1.2\) m/s²):

\[ d_m + v\,T + \frac{v^2}{2a} = 2.5 + 7.8 + \frac{7.8^2}{2.4} = 35.65\ \text{m} \le 40\ \text{m} \]

The kernel evaluates the same inequality for each entry of the table (rangerEnvelope). A change of the table that breaks it fails the build of the proofs.

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=python3 Verification/check.sh
   

   Expected result

   The script ends with no failure. A run takes approximately 80 s with a library from an earlier build.

check.sh builds the models and audits each project constant. It writes the golden vectors again and compares them with the committed files. It then runs the differential tests of the command path and of the run-time library, and the test programs that read the golden vectors. Verification/mutation_tests.py makes changes on purpose in the code and expects check.sh to fail for each change.

Validation

The proofs are only as good as the items that they trust.

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
The production code Runtime/	Checked against the golden files and against the Lean executables on fresh inputs. Not a proof
The C++ compiler and libm	The build of the library uses no fused multiply-add and no fast-math option
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 of the brake run	Stated, not proved
Sensors, map, localization, vehicle dynamics	Outside the models
Neural networks	Outside the models

Not Proved

• A learned model. No theorem is about a learned model.
• 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 deceleration of the speed envelope and the brake run are assumptions.
• Perception and localization. The pose, the map, the half widths and the LiDAR scan are trusted inputs. The geometry of the swept corridor has a Lean model for the ring of the plan box only (Shield/Proofs/Sweep.lean). The distance to a return in the ring has none. No theorem says that each command of a skill is an output of the shield.
• The code. No theorem is about the C++ code. The trajectory checker of the library is the compiled Lean model. Tests compare the other functions with their models.
• 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 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.

Files

Path	Content
Verification/AcresVerification/Scalar.lean	The scalar helpers
Verification/AcresVerification/*.lean	The models: CommandTiming, Watchdog, GearManager, ActionMap (the clip of the command row), Interpolation
Verification/AcresVerification/Proofs/*.lean	The proofs: Queue, Clock, CommandPath, FloatFacts, GearManager, Links
Verification/AcresVerification/Shield/	Shield.lean and Envelope.lean (models). Proofs/
Verification/AcresVerification/Mission/	Automaton.lean (model). Proofs.lean
Verification/AcresVerification/Planner/	Model.lean. Optimality.lean, CodeCost.lean, Regret.lean, RegretTight.lean, Checker.lean
Verification/AcresVerification/Trajectory/	Model.lean. Proofs.lean, Geometry.lean, Turn.lean, Tube.lean, Envelope.lean, Fast.lean, Raster.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	The changes on purpose that the check script must catch
Verification/Differential/	dbw_harness.cpp and run_differential.py (the command path of the game), runtime_harness.cpp and cpp_differential.py (the run-time library), shield_check.py and mission_check.py with the two mirrors, the folder golden/
Verification/Differential/golden/	The 10 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 and the enabled flag.