5.3. Per-Record Nonce

RFC 8446

A 64-bit sequence number is maintained separately for reading and
writing records.  The appropriate sequence number is incremented by
one after reading or writing each record.  Each sequence number is
set to zero at the beginning of a connection and whenever the key is
changed; the first record transmitted under a particular traffic key
MUST use sequence number 0.

As explained in section 5 the modelling of the Record Protocol is quite coarse. The Per-Record Nonce is not modelled at the moment.