The six-round differential optimum of ARADI is 82: a machine-checked lower bound

The automated study of the NSA block cipher ARADI by Bellini et al. (CLAASPing ARADI, INDOCRYPT 2024) reports in its Table 4 that the best single-key differential trail over six rounds has weight 84, printed in bold to denote optimality. Using the authors' own CLAASP model of ARADI we show that this value is not optimal: a single-key differential trail of weight 82 exists over six rounds, and no trail of weight 81 or less exists. The upper bound is a weight-82 trail of CLAASP's S-box model, confirmed by re-fixing it in the model and by the designers' round-function formula; CLAASP's own search returns weight-82 trails directly, and Monte-Carlo estimation agrees. The lower bound is obtained by a hybrid CNF (CLAASP's own component clauses together with a bidirectional sequential-counter encoding of the weight and Matsui-style window constraints), split by cube-and-conquer into 945 subproblems, every one of which is UNSAT; all 945 UNSAT results, together with the twenty one-to-five-round Matsui bounds they rely on, carry a DRAT certificate verified by drat-trim. The six-round optimum of 82 is therefore the first machine-checked optimal differential weight reported for round-reduced ARADI. The same weight-82 trail is also optimal under CLAASP's bit-sliced (AND-gate-count) model, whose six-round optimum we likewise show to be 82, so 84 is not optimal in either weight definition. The seven- and eight-round upper bounds of 106 and 122 in Table 4 are reproduced and thereby confirmed. We report the result as a single corrected table cell supported by a reproducible certificate, not as a break of the cipher.