Formal robustness verification with ISO/IEC 24029-2:2023

What the obligation asks for

Art. 15(1) of Regulation (EU) 2024/1689 requires a high-risk AI system to achieve an appropriate level of robustness and to perform consistently in that respect throughout its lifecycle, and Art. 15(4), first subparagraph, requires resilience to errors, faults and inconsistencies in the system or its environment. The obligation record lists the testable element this guide serves: outputs stay within the declared performance under input perturbation, noise, malformed input, edge cases and inconsistent signals from natural persons or connected systems. The level the result is compared with is the one the provider declares in the instructions for use under Art. 15(3) and Art. 13(3)(b)(ii). For an Annex III system these requirements apply from the Annex III application date 2027-12-02Deferred.

A robustness assessment for a neural network uses one of three method categories, statistical, formal or empirical, named in ISO/IEC TR 24029-1:2021Published. The formal category shows that a property holds for every point of a bounded input region, or produces a point where it fails. ISO/IEC 24029-2:2023Published supplies the way to state such a property, the method families that decide it and the three result terms: proven over the stated region, falsified with a counterexample, or undetermined. The statistical route, which samples perturbations and estimates a metric with a confidence interval, is the subject of the companion guide on robustness testing with the published technical report ISO/IEC TR 24029-1:2021Published. For a general-purpose AI model with systemic risk, the same result terms feed the evaluation record under Art. 55(1) for any bounded component the provider's evaluation plan puts under a formal property, from the GPAI application date 2025-08-02In force.

Inputs

From the inputs table of the protocol page, the formal route needs:

• Model weights at a fixed version, with the version hash; an inference endpoint is not enough, because the verifier reads the network structure and parameters
• The preprocessing specification: normalisation constants, input ordering and any clipping applied before the first layer
• The instructions for use with the declared robustness level and its conditions (Art. 15(3))
• The risk management file with the prior defined metrics and thresholds that name a perturbation magnitude (Art. 9(8)), where one exists
• The held-out set provenance record, from which the region centres are drawn
• The verifier, its version and its time limit, recorded before the first run
• The environment manifest written in step 1 of the protocol

Procedure

The steps below are the formal-method slice of PR-15-ROB v1.0, with the property terms of ISO/IEC 24029-2:2023Published on the steps that state and report a property. Every path, value and hash in the examples is synthetic.

1. Record the model version hash, preprocessing specification, verifier name and version, time limit and seeds in one manifest.

   Record Environment manifest with the model version hash, the verifier version and the time limit

   [PR-15-ROB step 1]

2. Extract the declared robustness level and the conditions it is declared for from the instructions for use.

   Record Declared-level extract with the robustness statement and its conditions

   [Regulation (EU) 2024/1689, Art. 15(3) and Art. 13(3)(b)(ii); PR-15-ROB step 3]

3. State each robustness goal as a property, an input region, a metric and a bound.

   Record Region table with one row per property: goal, centre sample, norm, half-width, output condition

   [ISO/IEC TR 24029-1:2021, clause on robustness goals and their statement; PR-15-ROB step 6]

4. Select the formal method for each goal that needs a result over a whole region and record the reason.

   Record Method selection record with the reason per goal, the input dimension and the network size

   [ISO/IEC TR 24029-1:2021, clauses on statistical, formal and empirical methods; PR-15-ROB step 7]

5. Write each property in the verifier's input format with the region bounds and the negated output condition.

   Record Property file per property with its hash

   [ISO/IEC 24029-2:2023, clause on stating robustness properties]

6. Export the frozen model to the verifier's model format and hash the exported file.

   Record Exported model file with its hash next to the version hash

   [AIAssuranceLabs procedure]

7. Run the verifier on each property with the recorded time limit and keep the full log.

   Record Verifier run log per property with the result line, the run time and the counterexample where one exists

   [ISO/IEC 24029-2:2023, clauses on stating robustness properties and reporting results; PR-15-ROB step 19]

8. Replay each counterexample through the frozen model and confirm that the output violates the property.

   Record Counterexample replay record with the model output at the returned point

   [AIAssuranceLabs procedure]

9. Classify each result as proven, falsified or undetermined, and record a time limit hit as undetermined.

   Record Formal result per property: proven, falsified or undetermined

   [ISO/IEC 24029-2:2023, clause on reporting results; PR-15-ROB, Limitations]

10. Compare each result with the declared robustness level and record the outcome per property.

    Record Declared-level comparison row per property with meets, does not meet or not comparable

    [Regulation (EU) 2024/1689, Art. 15(3); PR-15-ROB step 33]

11. Write the formal section of the robustness test report with the region, method, result and counterexample per property.

    Record Formal section of the robustness test report, grouped by property

    [ISO/IEC 24029-2:2023, clause on reporting results; PR-15-ROB step 40]

12. Record that a change to the weights, the preprocessing or the region invalidates every formal result.

    Record Re-test trigger list naming the weight, preprocessing and region changes that invalidate each result

    [Regulation (EU) 2024/1689, Art. 15(1); PR-15-ROB step 45]

The region table of step 3 fixes what each property claims before any verifier runs. The layout below is a synthetic example for a classifier with three normalised inputs and two output scores; the half-widths are inputs of the example and not a requirement of the Act.

Example for step 5. The property file uses the VNN-LIB format that published verifiers read. The output assertion states the violation, so the verifier searches the box for a point where the second score reaches the first; the file is a synthetic example for RP-01.

; synthetic example: property RP-01, box of half-width 0.10 around sample S-017
; the output assertion is the negation of the property: a point that satisfies it is a counterexample
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const Y_0 Real)
(declare-const Y_1 Real)
(assert (>= X_0 0.40))
(assert (<= X_0 0.60))
(assert (>= X_1 -0.10))
(assert (<= X_1 0.10))
(assert (>= X_2 0.15))
(assert (<= X_2 0.35))
(assert (>= Y_1 Y_0))

Example for step 6. The frozen PyTorch model is exported to ONNX with the input and output names the property file refers to, and both files are hashed into the manifest; the paths are synthetic.

# synthetic example: export the frozen model for the verifier
import torch

model = torch.load("model_v3f2a9c1.pt", weights_only=False).eval()
dummy = torch.zeros(1, 3)
torch.onnx.export(
    model, dummy, "model_v3f2a9c1.onnx",
    input_names=["X"], output_names=["Y"], opset_version=17,
)

sha256sum model_v3f2a9c1.onnx RP-01.vnnlib RP-02.vnnlib RP-03.vnnlib >> manifest_hashes.txt

Example for step 7 with a complete verifier. alpha-beta-CROWN is one published verifier of its class; it takes a YAML configuration that names the model, the property and the time limit, and it writes a result line per property. The configuration is a synthetic example; the time limit is an input of the example, recorded in the manifest of step 1.

# synthetic example: RP-01.yaml
general:
  device: cpu
  results_file: RP-01_result.txt
model:
  onnx_path: model_v3f2a9c1.onnx
specification:
  vnnlib_path: RP-01.vnnlib
bab:
  timeout: 600

python abcrown.py --config RP-01.yaml 2>&1 | tee RP-01_run.log

The verifier's result vocabulary maps onto the three terms of the standard as follows: a verified or unsat line is proven over the region; a falsified, unsafe or sat line is falsified, and the returned input is the counterexample for step 8; a timeout or unknown line is undetermined. The mapping is written into the result record, not left to the reader of the report.

Example for step 7 with an incomplete method. auto_LiRPA is a published bound-propagation library, another example of the class; it computes an interval for each output over the box. When the lower bound of the first score exceeds the upper bound of the second, the property is proven over the region; when it does not, the outcome is undetermined, because bound propagation alone never returns falsified.

# synthetic example: bound propagation for RP-01 on the frozen model
import torch
from auto_LiRPA import BoundedModule, BoundedTensor, PerturbationLpNorm

model = torch.load("model_v3f2a9c1.pt", weights_only=False).eval()
x0 = torch.tensor([[0.50, 0.00, 0.25]])                      # centre of the box for S-017
ptb = PerturbationLpNorm(norm=float("inf"), eps=0.10)         # half-width from the region table
bounded = BoundedModule(model, x0)
lb, ub = bounded.compute_bounds(x=(BoundedTensor(x0, ptb),), method="backward")
holds = bool(lb[0, 0] > ub[0, 1])
print("proven" if holds else "undetermined")  # this method alone never returns falsified

The result record of step 9 has one entry per property. The layout below is synthetic; the values are placeholders.

{
  "property_id": "RP-01",
  "goal": "<robustness goal id from step 3>",
  "region": {
    "centre_sample": "S-017",
    "norm": "linf",
    "half_width": 0.10,
    "property_file": "RP-01.vnnlib",
    "property_hash": "<sha256 from step 6>"
  },
  "model": {
    "version_hash": "<from the manifest, step 1>",
    "exported_file_hash": "<sha256 from step 6>",
    "preprocessing": "<specification id>"
  },
  "verifier": {
    "name": "<verifier and version>",
    "method": "<complete | incomplete>",
    "time_limit_s": "<from the manifest, step 1>",
    "run_time_s": "<from the run log, step 7>"
  },
  "result": "<proven | falsified | undetermined>",
  "counterexample": {
    "input": "<vector, or null>",
    "replayed_output": "<vector, or null>",
    "violation_confirmed": "<true | false | null>"
  },
  "declared_level_comparison": "<meets | does not meet | not comparable>",
  "run_log": "<log file id>",
  "recorded_by": "AIAssuranceLabs"
}

A pitfall that vendor documentation omits

An undetermined result is not a pass, and a region is not the input space. The Limitations section of PR-15-ROB v1.0 states both: a formal result holds only over the bounded input region stated in step 19, and an undetermined result is recorded as undetermined. Verifier documentation describes what a tool proves; it does not say what a report built from its output may claim. Two cases produce an undetermined result that reads like a pass in a summary table. A bound-propagation method is sound but incomplete: when its interval is too loose to separate the two scores, it returns no result, and the property may still hold or fail. A complete verifier that hits its time limit stops without a verdict. The result terms of ISO/IEC 24029-2:2023Published keep undetermined separate from both proven and falsified, and the report keeps the same three columns; a table that collapses undetermined into "no counterexample found" misstates the evidence. The same holds across regions: a property proven over each of the boxes in the region table says nothing about the inputs between them, and a result for the centre sample S-017 is not a result for a different sample.

The half-width of the box is the provider's choice and the Act sets none. Art. 15(1) requires an appropriate level; Art. 15(3) requires the provider to declare it; Art. 9(8) requires prior defined metrics and probabilistic thresholds in the risk management file. Where the risk management file names a sensor tolerance or a perturbation magnitude, the half-width comes from there. Where it does not, the source hierarchy applies: a harmonised standard cited in the Official Journal, of which none is cited as of the anchor date shown on the standards page, so no presumption of conformity exists; the JTC 21 draft prEN 18229-2Draft for the perturbation classes, which publishes no numeric magnitude; the published ISO/IEC 24029-2:2023Published for the form of the property, which publishes none either; a Commission guideline or code of practice; NIST AI RMF 1.0Published or a sector framework; or the state of the art the provider justifies. Step 9 of the protocol records the value, its source level and the justification. A related error sits in the property file itself: the VNN-LIB format used by published verifiers asserts the violation, so a file that asserts the property in the output line inverts every result, and a run that reports a counterexample then reads as a pass. Step 8, the counterexample replay, catches the inversion, because a replayed point that does not violate the stated property shows the file encoded the wrong condition.

What the result shows and what it does not

A formal result holds for the model version in the environment manifest, the exported file whose hash sits next to it, the preprocessing specification and the region in the property file; a change to any of these invalidates the result, and step 12 records the trigger. The result shows whether the stated property holds at every point of the stated box, or names a point where it fails; it does not show that the box, the property or the declared level is the appropriate one for the intended purpose, a judgement the provider holds under Art. 15(1) and Art. 9(5) and that a notified body and counsel review where a conformity assessment follows. The result is evidence for the provider's own technical file, delivered inside the robustness test report as one section of the robustness and adversarial testing service, within the limits on what we cannot do; it is not a conformity assessment.

Related pages

The obligation page, the protocol page and the ICP hubs below carry the rest of the Art. 15 evidence; the companion guide covers the statistical route.

Obligations

• Art. 15

Protocols

• PR-15-ROB v1.0

Related guides

• Robustness testing with ISO/IEC TR 24029-1

ICP hubs

• Annex III providers
• GPAI providers

Questions

+−What is ISO/IEC TR 24029-2?

The designation with TR is a common search form, and it does not match the published designation. Part 2 of the series was published as an International Standard, ISO/IEC 24029-2:2023, on the use of formal methods to assess the robustness of neural networks: how to state a property over a bounded input region and how to report a result as proven, falsified or undetermined. Part 1 is the published Technical Report ISO/IEC TR 24029-1:2021, which gives the overview of statistical, formal and empirical methods. Neither document is cited in the Official Journal, so no presumption of conformity exists for either.

Every inquiry receives a reply within 24 hours. Scope and availability are discussed per request.

Ask about scopehello@aiassurancelabs.com