RFC 5880 - Bidirectional Forwarding Detection (BFD)

Overview

Positive

what Ze has

Neutral

measures that are neither good news nor bad

Negative

what Ze owes

The 8 shares marked as a part above are the whole of the 111 gated MUSTs: they add to 100%. Proven by a recorded break is a share of TAGGED UNITS, a different population, so it is not one of them.

At a glance

Enrolment

Enrolled: Bidirectional Forwarding Detection (BFD)

What the public ledger says

Status: Partial

Coverage

Positive and negative tests (90): RFC5880-4.1-1, RFC5880-4.1-2, RFC5880-6.3-1, RFC5880-6.8.1-3, RFC5880-6.8.1-4, RFC5880-6.8.1-5, RFC5880-6.8.1-6, RFC5880-6.8.1-7, RFC5880-6.8.1-8, RFC5880-6.8.1-9, RFC5880-6.8.1-10, RFC5880-6.8.1-12, RFC5880-6.8.1-14, RFC5880-6.1-1, RFC5880-6.1-2, RFC5880-6.8.3-1, RFC5880-6.8.3-2, RFC5880-6.8.3-3, RFC5880-6.8.3-4, RFC5880-6.8.3-5, RFC5880-6.8.3-6, RFC5880-6.5-1, RFC5880-6.5-2, RFC5880-6.6-1, RFC5880-6.7-1, RFC5880-4.2-1, RFC5880-6.7.2-1, RFC5880-6.7.2-8, RFC5880-6.7.3-1, RFC5880-6.7.3-2, RFC5880-6.7.3-4, RFC5880-6.7.3-13, RFC5880-6.7.4-1, RFC5880-6.7.4-2, RFC5880-6.7.4-4, RFC5880-6.7.4-5, RFC5880-6.7.4-7, RFC5880-6.7.3-15, RFC5880-6.7.4-10, RFC5880-6.7.4-11, RFC5880-6.8.6-1, RFC5880-6.8.6-2, RFC5880-6.8.6-3, RFC5880-6.8.6-4, RFC5880-6.8.6-5, RFC5880-6.8.6-6, RFC5880-6.8.6-7, RFC5880-6.8.6-8, RFC5880-6.8.6-9, RFC5880-6.8.6-10, RFC5880-6.8.6-11, RFC5880-6.8.6-12, RFC5880-6.8.6-13, RFC5880-6.8.6-16, RFC5880-6.8.6-18, RFC5880-6.8.7-1, RFC5880-6.8.7-2, RFC5880-6.8.7-3, RFC5880-6.8.7-4, RFC5880-6.8.7-5, RFC5880-6.8.4-1, RFC5880-6.8.5-1, RFC5880-6.8.16-4, RFC5880-6.8.16-5, RFC5880-6.8.8-1, RFC5880-6.8.8-2, RFC5880-6.8.9-1, RFC5880-6.8.9-2, RFC5880-6.8.9-3, RFC5880-9-2, RFC5880-6.7.3-7, RFC5880-6.7.2-3, RFC5880-6.7.3-8, RFC5880-6.7.2-4, RFC5880-6.7.2-5, RFC5880-6.7.2-6, RFC5880-6.7.3-16, RFC5880-6.7.3-17, RFC5880-6.7.3-18, RFC5880-6.7.4-14, RFC5880-6.7.4-15, RFC5880-6.7.4-16, RFC5880-6.7.2-7, RFC5880-6.7.3-9, RFC5880-6.7.3-10, RFC5880-6.7.3-11, RFC5880-6.7.4-12, RFC5880-6.7.4-13, RFC5880-6.7.4-17, RFC5880-6.7.3-12

Annotated (including scoped evidence) (21): RFC5880-6.8.1-1, RFC5880-6.8.1-2, RFC5880-6.8.1-11, RFC5880-6.8.1-13, RFC5880-6.1-3, RFC5880-6.6-2, RFC5880-6.6-3, RFC5880-6.7.3-3, RFC5880-6.7.4-3, RFC5880-6.8.6-14, RFC5880-6.8.6-15, RFC5880-6.8.7-6, RFC5880-6.8.7-7, RFC5880-6.8.7-8, RFC5880-6.8.15-1, RFC5880-7-1, RFC5880-7-2, RFC5880-4.3-1, RFC5880-6.8.14-1, RFC5880-6.8.17-1, RFC5880-6.8.3-8

Requirements

Gaps and untested MUSTs

Proof state

A tagged unit reads unproven where no discrimination record exists for it: nothing in this tree has been observed to break it, so the claim its tag makes is unproven.

RFC5880-4.1-1

The contents of transmitted BFD Control packets MUST be set as follows: Version Set to the current version number (1). (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, subnet). Row quotes §6.8.7 "Version Set to the current version number (1)" (dated correction explains the kept id). + session TestRFC5880TransmittedControlCarriesVersionOne encodes Build in Down/Init/Up/AdminDown and BuildFinal through WriteTo and asserts octet0>>5 == 1; - session TestRFC5880TransmittedVersionNeverOverwrittenByDiag (Diag 0xFF cannot write into the version bits, packet still parses). Records: + revert session/fsm.go::Build, - revert packet/control.go::WriteTo, both observed red; author overlay dropping the Diag mask reds only the -. Residual: the older packet-level negative TestRFC5880VersionNotOneDiscarded asserts the receive discard, which is RFC5880-6.8.6-1, not this transmit row; it stays tagged but carries no weight here.

RFC5880-4.1-2

It MUST be zero on both transmit and receipt. (§4.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, subnet). §4.1 "It MUST be zero on both transmit and receipt." Transmit clause: + session TestRFC5880TransmittedControlMultipointZero asserts the M bit clear on the session's own Build/BuildFinal wire in every transmitting state (record: revert session/fsm.go::Build, observed red); a property of every transmitted packet, single polarity is valid. Receipt clause: - packet TestRFC5880MultipointSetDiscarded (ParseControl refuses M=1) and + TestRFC5880MultipointZeroAccepted.

RFC5880-6.3-1

Each system MUST choose an opaque discriminator value that identifies each session, and which MUST be unique among all BFD sessions on the system. (§6.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: discriminator 0 or a value held by another session. Red: TestRFC5880DiscriminatorsAreNonZeroAndUnique Fatalf on d==0 or a repeat across 32 EnsureSession calls; TestRFC5880DiscriminatorAllocatorSkipsReservedAndTaken parks nextDiscr on 0 with 1 and 2 taken and Fatalf if 0, 1 or 2 is returned. 'Opaque' carries no testable behaviour.

RFC5880-6.8.1-1

This variable MUST be initialized to Down. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity positive: Init state is Down.

RFC5880-6.8.1-2

This variable MUST be initialized to Down. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity positive: RemoteSessionState is Down after Init.

RFC5880-6.8.1-3

It MUST be unique across all BFD sessions on this system, and nonzero. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. same allocator tests as 6.3-1: nonzero and unique LocalDiscr, skip of 0 and taken values.

RFC5880-6.8.1-4

This MUST be initialized to zero. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Positive TestRFC5880InitVariableDefaults fails on RemoteDiscriminator()!=0 after Init. Genuine negative (R1 route b) TestRFC5880InitClearsLearnedRemoteDiscr: a Machine that learned the peer discriminator 1 is Init-ed again and must hold 0. Targeted break Init literal RemoteDiscr: 0 -> m.vars.RemoteDiscr (carry the learned value) observed red on the negative (the positive stays green under it, since a fresh Machine holds 0 anyway). The old negative tag (Receive installing My Discriminator, a 6.8.6 step) was removed with approval.

RFC5880-6.8.1-5

If a period of a Detection Time passes without the receipt of a valid, authenticated BFD packet from the remote system, this variable MUST be set to zero. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). Adds TestRFC5880RemoteDiscrClearedDespiteInvalidPackets: on an authenticated Up session an A-bit-clear packet (ErrAuthMismatch) and a Your-Discriminator-0 Up packet (ErrYourDiscriminatorReset) inside the Detection Time leave CheckDetection to clear bfd.RemoteDiscr at its end, so the 'valid, authenticated' clause is asserted; mutant fsm.go discard guard observed red. Expiry clauses and the neighbor-signaled-Down negative stand as before. Digest failures are refused in the engine before Receive (auth rows).

RFC5880-6.8.1-6

This MUST be initialized to zero (No Diagnostic). (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Unit re-read after TestRFC5880InitVariablesAreNotConstants lost its 6.8.1-4 tag (doc comment only, body unchanged). Judgement unchanged: Forbidden: bfd.LocalDiag initialised to anything but 0. TestRFC5880InitVariableDefaults fails on LocalDiag() != DiagNone straight after Init. Negative TestRFC5880InitVariablesAreNotConstants shows the value is an initial value, not a constant: a peer-signalled Down moves it to DiagNeighborSignaledDown.

RFC5880-6.8.1-7

This MUST be initialized to a value of at least one second (1,000,000 microseconds) according to the rules described in section 6.8.3. (§6.8.1, §6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD strict re-read 2026-09-27. One clause: bfd.DesiredMinTxInterval initialised to at least 1,000,000 us. Forbidden: Init storing a value below 1 s (here the configured 300 ms). Red: TestRFC5880SlowStartFloorWhileNotUp Fatalf when DesiredMinTxIntervalUs() < 1000000 straight after Init (Init, session.go, assigns SlowStartIntervalUs), and when TransmitInterval is below 1 s while Down. Contrast: TestRFC5880SlowStartFloorLiftedWhenUp fails unless the same accessor reads the configured 300000 at Up, so the positive cannot pass on a constant.

RFC5880-6.8.1-8

The last value of Required Min RX Interval received from the remote system in a BFD Control packet. This variable MUST be initialized to 1. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Unit re-read after TestRFC5880InitVariablesAreNotConstants lost its 6.8.1-4 tag (doc comment only, body unchanged). Judgement unchanged: Forbidden: bfd.RemoteMinRxInterval initialised to anything but 1. TestRFC5880InitVariableDefaults fails on RemoteMinRxInterval != 1 after Init. Negative TestRFC5880InitVariablesAreNotConstants shows the value is replaced by the advertised 700000, so the 1 is an initial value.

RFC5880-6.8.1-9

This variable MUST be initialized to zero. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Unit re-read after TestRFC5880InitVariablesAreNotConstants lost its 6.8.1-4 tag (doc comment only, body unchanged). Judgement unchanged: Forbidden: bfd.RemoteDemandMode initialised true. TestRFC5880InitVariableDefaults fails on RemoteDemandMode true after Init. Negative TestRFC5880InitVariablesAreNotConstants shows it follows a received D=1, so false is an initial value.

RFC5880-6.8.1-10

This variable MUST be a nonzero integer, and is otherwise outside the scope of this specification. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: bfd.DetectMult zero. Red: TestRFC5880DetectMultZeroRequestSubstituted Inits with DetectMult 0 and Fatalf if DetectMult()==0 or != DefaultDetectMult; positive keeps the configured 3. Init (session/session.go:256) is the only writer of vars.DetectMult.

RFC5880-6.8.1-11

This variable MUST be initialized to a random 32-bit value. (§6.8.1)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.1-11, so no unit is bound to it.

RFC5880-6.8.1-12

This variable MUST be initialized to zero. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28. Positive TestRFC5880NewSessionAuthSeqKnownZero: a new Machine with SetAuth has AuthSeqKnown 0 and accepts a first packet at 0x80000000, which Check would refuse from any initialized floor of 0. Negative TestRFC5880AuthSeqKnownOneDiscardsFirstPacket builds the violating initial state (AuthSeqKnown 1) and shows the same packet is refused, so the observable outcome depends on the zero start; an initialization has no refusal path, and the violating state is the non-conforming input.

RFC5880-6.8.1-13

This variable MUST be set to zero after no packets have been received on this session for at least twice the Detection Time. (§6.8.1)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.1-13, so no unit is bound to it.

RFC5880-6.8.1-14

Once session state is created, and at least one BFD Control packet is received from the remote end, it MUST be preserved for at least one Detection Time (see section 6.8.4) subsequent to the receipt of the last BFD Control packet, regardless of the session state. (§6.8.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd AdminDown). Positive TestRFC5880ReleasedSessionPreservedForOneDetectionTime edited under D-15: the peer keeps sending past AdminDownTransmitEnd so the final removal is the one 6.8.1 sets, entry present one ns before the last deadline and gone at it; retention can now only be longer than 6.8.1 (retireReleasedLocked also waits for the 6.8.16 window), never shorter. Session-level positive TestRFC5880StatePreservedForOneDetectionTime and negative TestRFC5880ReleasedSessionAskedAgainKeepsRemoteState unchanged (revive keeps Machine, discriminator, RemoteDiscr, RemoteMinRx, LastReceived). Records: revert retireReleasedLocked (+) and reviveReleasedLocked (-) observed red.

RFC5880-6.1-1

A system taking the Active role MUST send BFD Control packets for a particular session, regardless of whether it has received any BFD packets for that session. (§6.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Stale only because the RFC5880-6.1-3 negative tag comment was removed from session TestRFC5880PassiveRoleSilentUntilReception; body unchanged. Proof unchanged: + engine TestRFC5880ActiveSessionSendsBeforeAnyReception; - engine TestRFC5880ActiveSessionSendsAfterThePeerFallsSilent, both recorded revert loop.go::tick observed red. The session-level negative stays supplementary.

RFC5880-6.1-2

A system taking the Passive role MUST NOT begin sending BFD packets for a particular session until it has received a BFD packet for that session, and thus has learned the remote system's discriminator value. (§6.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Stale only because the RFC5880-6.1-3 negative tag comment was removed from session TestRFC5880PassiveRoleSilentUntilReception; body unchanged. + engine TestRFC5880PassiveSessionSilentThroughTicksUntilReception; - engine TestRFC5880PassiveSessionSendsOnceThePeerSpoke; both recorded revert loop.go::tick observed red.

RFC5880-6.1-3

At least one system MUST take the Active role (possibly both). (§6.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Owner ruling 2026-09-30 ('we can not see the peer'): no refusal path exists, so the HEAD negative (TestRFC5880PassiveRoleSilentUntilReception, which proved RFC5880-6.1-1 and 6.1-2, where it stays) was removed and the row carries {single-polarity: positive}. + session TestRFC5880ActiveRoleTransmitsWithoutReception: a request with Passive unset gives RoleActive and arms the TX deadline with RemoteDiscr 0; record revert session.go::Init observed red. Operator default reaches that request (ze-bfd-conf.yang passive default false; single-hop Passive refused per RFC 5881 Section 3). The pair obligation beyond Ze's own role is not observable by Ze.

RFC5880-6.8.3-1

When bfd.SessionState is not Up, the system MUST set bfd.DesiredMinTxInterval to a value of not less than one second (1,000,000 microseconds). (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). TestRFC5880SlowStartFloorInEveryStateButUp adds the floor (live variable and Build field) in Init, on Up->Down by detection expiry, by peer Down and by peer AdminDown, with 300 ms in Up between, closing the gap the earlier note named; local AdminDown stays covered by FloorRestoredOnAdminDown, negative LiftedWhenUp. Mutant onStateChange state guard and whole-body revert both observed red after the Poll fix.

RFC5880-6.8.3-2

If either bfd.DesiredMinTxInterval is changed or bfd.RequiredMinRxInterval is changed, a Poll Sequence MUST be initiated (see section 6.5). (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). Each clause alone: TestRFC5880PollInitiatedForEachIntervalAlone (TX alone on the move to Up, RX alone by the echo slow-down) and the Down-entry case now fixed in onStateChange: TestRFC5880PollInitiatedWhenDownEntryRaisesDesiredMinTx sets PollOutstanding when leaving Up raises bfd.DesiredMinTxInterval to 1 s. The Poll is set after the Down-entry reset, so it survives; it rides periodic packets only (6.5-2), a Passive session with no RemoteDiscr sends none, and Build/BuildFinal never set P and F together. Negative NoPollWhenIntervalsUnchanged. Mutants || -> && and the new != -> == observed red. AdminEnable leaves the floor unchanged, so no Poll is owed there.

RFC5880-6.8.3-3

If bfd.DesiredMinTxInterval is increased and bfd.SessionState is Up, the actual transmission interval used MUST NOT change until the Poll Sequence described above has terminated. (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD3 first verdict 2026-09-27 (gap closed by DF-BFD-7: desiredMinTxInForceUs, holdDesiredMinTxLocked, releaseDesiredMinTxLocked in timers.go). The sentence has one condition pair (increase AND Up) and one prohibition (actual interval unchanged until the Poll terminates). Forbidden behaviour: TX at the raised interval while the Poll is outstanding. Both writers of an increase in Up are driven by the positive TestRFC5880RaisedDesiredMinTxHeldUntilPollTerminates: echo slow-down (300 ms to 1 s, RemoteMinRx 100 ms) requires TransmitInterval == 300 ms, NextTxDeadline == last TX + 300 ms after AdvanceTxWithJitter, and still +300 ms after a non-Final packet (the Receive reschedule path); Up transition with a 2 s configured interval requires TransmitInterval == 1 s (remote 300 ms) with the Poll outstanding. Each goes red if TransmitInterval reads the live bfd.DesiredMinTxInterval (1 s, 2 s). Negative TestRFC5880RaisedDesiredMinTxAppliedAtFinal: the terminating Final makes TransmitInterval 1 s and moves the pending deadline to last TX + 1 s, red on a hold that is never released or released without rescheduling; a session leaving Up drops the hold (TransmitInterval 1 s slow-start, not the held 300 ms). The only runtime writers of bfd.DesiredMinTxInterval in Up are ApplyEchoSlowdown and onStateChange, both covered; a decrease (revertEchoSlowdownLocked) is not held, as the sentence covers only an increase. Re-judge 2026-10-12 (independent auditor) after 0e0e98810f added a third writer of an increase in Up, Machine.ApplyTimers (profile edit) through applyPendingTimersLocked, and tagged TestApplyTimersIncreaseHeldUntilFinal positive. RFC 5880 Section 6.8.3 re-read: 'If bfd.DesiredMinTxInterval is increased and bfd.SessionState is Up, the actual transmission interval used MUST NOT change until the Poll Sequence described above has terminated.' applyPendingTimersLocked calls holdDesiredMinTxLocked before writing the raised value and starts the Poll in the same step; the new unit raises 300 ms to 1 s on a settled Up session with RemoteMinRx 50 ms, requires TransmitInterval 300 ms while the Poll is outstanding (1 s if TransmitInterval read the live variable) and 1 s after the Final. The earlier claim that ApplyEchoSlowdown and onStateChange are the only Up writers is superseded: ApplyTimers is the third, and every one of the three now has a positive. The new unit checks TransmitInterval, not NextTxDeadline, for the ApplyTimers path; rescheduleTxLocked after the write derives the deadline from the same in-force value, and the deadline itself stays proven by TestRFC5880RaisedDesiredMinTxHeldUntilPollTerminates. Revert record on holdDesiredMinTxLocked observed red. Verdict unchanged.

RFC5880-6.8.3-4

If bfd.RequiredMinRxInterval is reduced and bfd.SessionState is Up, the previous value of bfd.RequiredMinRxInterval MUST be used when calculating the Detection Time for the remote system until the Poll Sequence described above has terminated. (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-10-12 (independent auditor). RFC 5880 Section 6.8.3 read: 'If bfd.RequiredMinRxInterval is reduced and bfd.SessionState is Up, the previous value of bfd.RequiredMinRxInterval MUST be used when calculating the Detection Time for the remote system until the Poll Sequence described above has terminated.' Producer: DetectionInterval (and armDetectionLocked through it) reads requiredMinRxInForceUs, which answers the held value while rxRequiredHeld; holdRequiredMinRxLocked records it on a reduction in Up, called by every Up writer of a reduction (applyPendingTimersLocked for ApplyTimers, revertEchoSlowdownLocked, the Up transition in onStateChange); Receive clears it on the Final and leaving Up clears it. Positive TestRequiredMinRxReductionHeldUntilFinal: profile edit 300 ms to 100 ms with RemoteDesiredMinTx 10 ms requires 900 ms while the Poll is outstanding (300 ms if the live value were read), and the echo slow-down revert 1 s to 300 ms requires 3 s (900 ms if read live); both assert the precondition that the reduced value was written and the Poll is outstanding, so the buffer isolates the hold. Negative TestRequiredMinRxReductionAppliedAtFinal: the Final makes the Detection Time 300 ms (red on a hold never released), and a session leaving Up drops the hold. The Up-transition writer has no unit for a reduction: outside Up every other writer (session.go applyRequest/Reconfigure, the non-Up branch of ApplyTimers) sets bfd.RequiredMinRxInterval to the configured value, so the Up transition can reduce it only if an echo slow-down value outlived the session leaving Up; the code holds that case and no unit exercises it. Revert records observed red on holdRequiredMinRxLocked (positive) and fsm.go Receive (negative).

RFC5880-6.8.3-5

If the local system reduces its transmit interval due to bfd.RemoteMinRxInterval being reduced (the remote system has advertised a reduced value in Required Min RX Interval), and the remote system is not in Demand mode, the local system MUST honor the new interval immediately. (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD2 strict re-read 2026-09-27 (stale on Receive: echo reschedule and pollSettling added after rescheduleTxLocked, which is still called on every accepted packet). Forbidden: keeping the old, longer wait after a reduction. TestRFC5880RemoteMinRxChangeReschedulesNextTx requires last TX + 400 ms after 900 to 400 ms, and a jittered 900 of 1.2 s rescaled to 300 of 400 ms, already due. TestRFC5880RemoteMinRxReductionHonoredImmediately pins TransmitInterval at 400 ms at once. Negatives: TestRFC5880UnchangedRemoteMinRxKeepsNextTx (no change, deadline kept) and TestRFC5880TransmitIntervalFlooredByLocalDesired (a reduction below the local desired value does not shorten TX). The Demand-mode condition only removes the obligation; Ze runs no Demand mode, so it always honours the reduction.

RFC5880-6.8.3-6

Therefore, if multiple changes are made that require the use of a Poll Sequence, there are three choices: 1) they MUST be communicated in a single BFD Control packet (so the semantics of the Final reply are clear), or 2) sufficient time must have transpired since the Poll Sequence was completed to disambiguate the situation (at least a round trip time since the last Poll was transmitted) prior to the initiation of another Poll Sequence, or 3) an additional BFD Control packet with the Final (F) bit *clear* MUST be received after the Poll Sequence has completed prior to the initiation of another Poll Sequence (this option is not available when Demand mode is active). (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD2 strict re-read 2026-09-27, raised from weak: the RA-BFD defect is fixed at the producer. Every Poll initiator is choice 1 or choice 3: onStateChange changes both intervals under one PollOutstanding (and can only fire from Down/Init, where Down entry clears PollOutstanding and pollSettling); ApplyEchoSlowdown and revertEchoSlowdownLocked (while Up) return with the flag unchanged unless pollSequenceIdle, which Receive clears only on the Final that ends the Poll (pollSettling set) followed by a packet with F clear. Forbidden second Poll during an outstanding Poll: TestRFC5880EchoSlowdownWaitsForOutstandingPoll (tx and rx stay 10000 during the Up Poll) and TestRFC5880EchoSlowdownRevertWaitsForOutstandingPoll (stays 1000000). Forbidden Poll after the Final before an F-clear packet: both tests assert no Poll and the old intervals. Positive: TestRFC5880EchoSlowdownPollsAfterSettledPoll (P set, both intervals 1000000 in one packet) and TestRFC5880PollInitiatedOnIntervalChange (single packet). Choice 2 is an alternative Ze does not take; Demand mode is not driven, so choice 3 is always available.

RFC5880-6.5-1

A BFD Control packet MUST NOT have both the Poll (P) and Final (F) bits set. (§6.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: P and F both set. Red: TestRFC5880PollPacketHasNoFinalBit Fatalf on c.Final from Build with PollOutstanding; TestRFC5880FinalReplyClearsPollBit Fatalf on f.Poll from BuildFinal with PollOutstanding true, the state where inheriting P would set both. Build and BuildFinal are the only packets sendLocked is handed (engine/loop.go).

RFC5880-6.5-2

If periodic BFD Control packets are already being sent (the remote system is not in Demand mode), the Poll Sequence MUST be performed by setting the Poll (P) bit on those scheduled periodic transmissions; additional packets MUST NOT be sent. (§6.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). TestRFC5880PollRidesTheScheduledPacket: a Poll raised in Up leaves NextTxDeadline unchanged and the packet built at that deadline carries P; the engine has no send path keyed on PollOutstanding (only BuildFinal answers a received Poll), so no additional packet exists. Mutant ApplyEchoSlowdown pollSequenceIdle guard observed red. P-bit negative unchanged.

RFC5880-6.6-1

A system MUST NOT set the Demand (D) bit unless bfd.DemandMode is 1, bfd.SessionState is Up, and bfd.RemoteSessionState is Up. (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: D set while DemandMode, local Up or remote Up is false. Red: TestRFC5880DemandBitClearWhenAnyConditionFails Fatalf on Build().Demand with each condition dropped alone and with both states Down; positive TestRFC5880DemandBitSetWhenAllConditionsHold shows D is set when all hold, so the clear cases are not a constant false.

RFC5880-6.6-2

When the transmitted value of the Demand (D) bit is to be changed, the transmitting system MUST initiate a Poll Sequence in conjunction with changing the bit in order to ensure that both systems are aware of the change. (§6.6)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.6-2, so no unit is bound to it.

RFC5880-6.6-3

If Demand mode is active on either or both systems, a Poll Sequence MUST be initiated whenever the contents of the next BFD Control packet to be sent would be different than the contents of the previous packet, with the exception of the Poll (P) and Final (F) bits. (§6.6)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.6-3, so no unit is bound to it.

RFC5880-6.7-1

Implementations supporting authentication MUST support both types of SHA1 authentication. (§6.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28. Positive: TestRFC5880BothSHA1VariantsSupported round-trips types 4 and 5. Negative: TestRFC5880SHA1TypesEnforcedDistinctly shows each SHA1 type is really implemented: a flipped hash is refused for each, each refuses the other's section, and a repeated sequence is accepted by 4 and refused by 5, so a stub or an aliased Meticulous type goes red. The older negative (types 0/6/200 refused) stays tagged but does not violate this row.

RFC5880-4.2-1

The password is a binary string, and MUST be from 1 to 16 bytes in length. (§4.2, §6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 re-stamp: the bfd TestRFC5880SimplePasswordLengthOutOfRangeRefused unit lost only its 6.7.2-1 tag (D-15); body unchanged. Forbidden: a 0-byte or over-16-byte password accepted. Red: auth TestRFC5880SimplePasswordLengthOutOfRangeRefused Fatalf unless NewSigner and NewVerifier return ErrKeyLengthInvalid for 0, 17, 32, 255 bytes; bfd TestRFC5880SimplePasswordLengthOutOfRangeRefused Fatalf when parseAuthConfig accepts 0, 17 or 32 bytes. Positive: 1, 8, 16 bytes encode (auth SectionHeader) and 1, 14, 16 bytes parse (SimplePasswordManagementAcceptsASCIIStrings), both range ends.

RFC5880-6.7.2-1

For interoperability, the management interface by which the password is configured MUST accept ASCII strings (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30. Now driven through the operator's entry: config text parsed against the bfd YANG, the plugin config section, parseSections, resolveProfile, asserting the session request's Auth.Secret byte for byte. Positive: a plain ASCII password for simple-password. Negative (R1b, inputs forced toward the violation): every ASCII byte 0x01-0x7F including quote, backslash, ; { } # and whitespace, plus leading/trailing spaces, in 16-byte chunks. Judge's own break (parseAuthConfig strips one trailing space) reds the negative in all 5 types while the positive stays green; revert records observed red on both. Old direct parseAuthConfig positive kept; the 4.2-1 length refusal no longer carries this row (D-15).

RFC5880-6.7.2-8

The Auth Type field MUST be set to 1 (Simple Password). The Auth Len field MUST be set to the proper length (4 to 19 bytes). (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28. Positive TestRFC5880SimplePasswordSectionHeader pins Auth Type 1 and Auth Len password+3 within 4..19. Auth Type clause negative: TestRFC5880SimplePasswordRejectsForeignSectionShape, a receiver refusing a section built against the transmit rule, isolated (no digest). Auth Len clause negative: TestRFC5880SimplePasswordSectionOutsideProperLengthNotBuilt, NewSigner refuses the 0 and 17-byte passwords that would carry Auth Len 3 and 20.

RFC5880-6.7.3-1

The Auth Type field MUST be set to 2 (Keyed MD5) or 3 (Meticulous Keyed MD5). The Auth Len field MUST be set to 24. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-29. Both clauses. Positive TestRFC5880KeyedMD5SectionHeader asserts Auth Type 2/3 and Auth Len 24 on the signed wire (observed red with digestSigner.Sign broken). Negative TestRFC5880KeyedMD5OtherAlgorithmFieldsDiscarded, types 2 and 3, hand-builds packets with Auth Type 4/5 or Auth Len 28 and computes the MD5 digest AFTER the alteration, so the digest compare would accept them and only the field checks in digestVerifier.Verify refuse (read at the producer: Control Length is left correct, so the Length check cannot fire first); exact ErrDigestMismatch, fresh SeqState per packet, the unaltered packet accepted. The Auth Type half has an observed-red mutant record; the Auth Len half is isolated by construction but its mutants timed out, so it has no record. The older confounded tags (RejectsForeignSectionShape, OversizedKeyNotSigned) are not relied on.

RFC5880-6.7.3-2

An MD5 digest MUST be calculated over the entire BFD Control packet. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28. Positive TestRFC5880DigestSpansEntirePacket compares Sign's digest with crypto/md5 computed independently over bytes 0..Length with the padded key, and accepts a hand-built packet. Negative TestRFC5880DigestOverPartialPacketDiscarded refuses digests over 24, off+4, off+8 and Length-1 bytes and every single-byte flip of the mandatory section, Reserved byte and Sequence Number (fresh SeqState, so D-14 seeding precedes and the window cannot refuse first). Types 2 and 3.

RFC5880-6.7.3-3

replacing the secret key, which MUST NOT be carried in the packet (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity positive: neither the padded nor the raw secret appears in the emitted bytes.

RFC5880-6.7.3-4

For Meticulous Keyed MD5, bfd.XmitAuthSeq MUST be incremented in a circular fashion (when treated as an unsigned 32-bit value). (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-29. Both clauses. Positive TestRFC5880MeticulousXmitAuthSeqWrapsAt32Bits puts 0xFFFFFFFE, 0xFFFFFFFF, 0, 1 on the wire through Machine.Sign/AdvanceAuthSeq (observed red with AdvanceAuthSeq broken), so a saturating or non-incrementing XmitAuthSeq goes red. Negative TestRFC5880MeticulousNonCircularRepeatAtWrapDiscarded (type 3) signs 0xFFFFFFFF twice through Machine.Sign, the exact output of a non-circular transmitter, and the peer refuses the repeat with ErrSequenceOutsideWindow, then accepts the circular successor 0 in the same state (observed red with the meticulous.go equality check mutated). The held incremented-clause negative stays.

RFC5880-6.7.3-13

The authentication key value is a binary string of up to 16 bytes, and MUST be placed into the Auth Key/Digest field, padded with trailing zero bytes as necessary. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-18 (independent auditor, after 97686ea267). RFC 5880 Section 6.7.3: "The authentication key value is a binary string of up to 16 bytes, and MUST be placed into the Auth Key/Digest field, padded with trailing zero bytes as necessary." parseAuthConfig now takes the secret from parseAuthSecret (ASCII or decoded hex) and still refuses a decoded MD5 key over packet.KeyedMD5KeyLenMax before any session exists; NewSigner and NewVerifier refuse the same at the auth boundary and newDigestSigner copies the key into a zero-filled 16-byte slot. Positive: TestRFC5880ShortKeyZeroPaddedIntoDigestField recomputes MD5 independently over the packet with the 11-byte key plus five zero bytes and requires Sign's digest to match; TestParseAuthConfigKeyedSecretLength and TestKeyedSecretLongerThanSlotRefused accept 16 bytes. Negative: both refuse 17 bytes. An overlay mutation disabling the MD5 length check in current parseAuthConfig turned TestParseAuthConfigKeyedSecretLength red (and the untagged hex refusal case), so the change did not weaken the parser-side check.

RFC5880-6.7.4-1

The Auth Type field MUST be set to 4 (Keyed SHA1) or 5 (Meticulous Keyed SHA1). The Auth Len field MUST be set to 28. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-29. Both clauses. Positive TestRFC5880KeyedSHA1SectionHeader asserts Auth Type 4/5 and Auth Len 28 (observed red with digestSigner.Sign broken). Negative TestRFC5880KeyedSHA1OtherAlgorithmFieldsDiscarded, types 4 and 5, hashes Auth Type 2/3 or Auth Len 24 in after the alteration, exact ErrDigestMismatch, unaltered accepted; isolated as for 6.7.3-1 (Control Length correct, digest valid). Auth Type half recorded by mutant; Auth Len half isolated by construction, no record. Older confounded tags not relied on.

RFC5880-6.7.4-2

A SHA1 hash MUST be calculated over the entire BFD control packet. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28. Same units as RFC5880-6.7.3-2 for types 4 and 5: Sign's hash equals crypto/sha1 over the entire packet computed independently, and hashes over 24, off+4, off+8, Length-1 bytes plus every single-byte flip of the mandatory section, Reserved byte and Sequence Number are refused with ErrDigestMismatch.

RFC5880-6.7.4-3

the secret key, which MUST NOT be carried in the packet (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC5880SecretKeyNotCarriedInPacket asserts neither the padded nor the raw secret appears in the emitted SHA1 packet (single-polarity).

RFC5880-6.7.4-4

For Meticulous Keyed SHA1, bfd.XmitAuthSeq MUST be incremented in a circular fashion (when treated as an unsigned 32-bit value). (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-29. Same units as 6.7.3-4 over type 5: the positive wrap test runs type 5 through Machine.Sign, and the negative loop runs type 5 after type 3 through the same Verify/Check path, repeat refused with ErrSequenceOutsideWindow and 0 accepted. The recorded red fired on the type-3 iteration; the type-5 iteration asserts the same outcome over the SHA1 verifier.

RFC5880-6.7.4-5

the management interface by which the key is configured MUST accept ASCII strings (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30. Same units as 6.7.3-7 over keyed-sha1 and meticulous-keyed-sha1 (keys up to 20 bytes, the sweep chunked at 20); judge's trailing-space-strip break reds both SHA1 negative subtests. Revert records observed red. Incomplete-block negative untagged (D-15).

RFC5880-6.7.4-7

The authentication key value is a binary string of up to 20 bytes, and MUST be placed into the Auth Key/Hash field, padding with trailing zero bytes as necessary. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-18 (independent auditor, after 97686ea267). RFC 5880 Section 6.7.4: "The authentication key value is a binary string of up to 20 bytes, and MUST be placed into the Auth Key/Hash field, padding with trailing zero bytes as necessary." parseAuthConfig applies the packet.KeyedSHA1KeyLenMax refusal to the secret parseAuthSecret returns, so the ASCII and hex forms meet the same limit (a hex form over 20 bytes is also refused earlier by the YANG length 2..40); NewSigner and NewVerifier refuse it again and newDigestSigner zero-pads into the 20-byte slot. Positive: TestRFC5880ShortKeyZeroPaddedIntoDigestField recomputes SHA1 over the packet with the 11-byte key plus nine zero bytes and requires Sign's hash to match; TestParseAuthConfigKeyedSecretLength and TestKeyedSecretLongerThanSlotRefused accept 20 bytes. Negative: both refuse 21 bytes, and by inspection removing the SHA1 check in parseAuthConfig leaves the 21-byte case accepted, which the test fails on.

RFC5880-6.7.3-15

The Auth Key ID field MUST be set to the ID of the current authentication key. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880MD5AuthKeyIDIsTheCurrentKey: both MD5 types, key ids 0/1/200/255 read back at MandatoryLen+2 and verified. Negative (R1b, forced input) TestRFC5880MD5AuthKeyIDOverwritesStaleBuffer: section pre-filled 0xFF, Sign must leave key 7. Judge break digestSigner.Sign writing buf[off+2] unchanged reds both (and the positive at ids 1..255).

RFC5880-6.7.4-10

The Auth Key ID field MUST be set to the ID of the current authentication key. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880AuthKeyIDIsTheConfiguredKey (Keyed SHA1, ids 0/1/200/255 on the wire); judge break of the key-id write in digestSigner.Sign reds it. Negative TestRFC5880AuthKeyIDMismatchDiscarded is the receive-side handling of a peer PDU with a key id other than the configured one (owner ruling 2 reading of a generate row); judge break removing the key-id check in digestVerifier.Verify reds it through its replay-floor assertion, so it is isolated from the digest.

RFC5880-6.7.4-11

The Sequence Number field MUST be set to bfd.XmitAuthSeq. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Keyed SHA1 via session Machine.Sign: positive TestRFC5880AuthSequenceFieldIsXmitAuthSeq pins 0x11223344 in the field; negative (forced input) TestRFC5880AuthSequenceFieldFollowsAdvance requires the field to follow AdvanceAuthSeq to first+1, so a constant or ignored seq fails; revert records observed red. Limit: neither unit drives the variable above 0x7FFFFFFF; the full-range unit TestRFC5880SequenceFieldIsXmitAuthSeqAcrossTheCounterRange loops the SHA1 types too but is tagged on 6.7.3-8 only (shared digestSigner.Sign producer).

RFC5880-6.8.6-1

If the version number is not correct (1), the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting a Version other than 1. TestRFC5880VersionNotOneDiscarded fails unless ParseControl returns exactly ErrBadVersion for 0, 2, 3 and 7 (version is the first check, so no other rule trips); handleInbound returns on any ParseControl error. Positive TestRFC5880VersionOneAccepted: version 1 parses with no error.

RFC5880-6.8.6-2

If the Length field is less than the minimum correct value (24 if the A bit is clear, or 26 if the A bit is set), the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). Section 6.8.6: Length below 24 (A=0) or 26 (A=1) MUST be discarded. Both floors now proven from both sides at ParseControl: + TestRFC5880LengthMinimumAccepted (24 A=0, 26 A=1); - TestRFC5880LengthBelowMinimumDiscarded (23, 24 A=1) and NEW TestRFC5880AuthenticatedLengthOneBelowMinimumDiscarded (A=1 Length 25 -> ErrLengthTooSmall), which closes the 25-byte gap: a targeted overlay setting the A=1 floor to MandatoryLen+1 reds only the new unit (job-ov6). Record: revert control.go::ParseControl observed red.

RFC5880-6.8.6-3

If the Length field is greater than the payload of the encapsulating protocol, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting Length > payload. TestRFC5880LengthOverPayloadDiscarded fails unless ParseControl returns ErrLengthOverBuffer for Length = payload + 8; TestRFC5880LengthEqualsPayloadAccepted fails if Length == payload is rejected, which catches a >= mutation. handleInbound returns on the error.

RFC5880-6.8.6-4

If the Detect Mult field is zero, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting Detect Mult 0. TestRFC5880DetectMultZeroDiscarded fails unless ParseControl returns ErrZeroDetectMult; TestRFC5880DetectMultNonZeroAccepted fails if 1, 3 or 255 is rejected or mis-decoded. handleInbound returns on the error.

RFC5880-6.8.6-5

If the Multipoint (M) bit is nonzero, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting M=1. TestRFC5880MultipointSetDiscarded fails unless ParseControl returns ErrMultipointSet; TestRFC5880MultipointZeroAccepted fails if an M=0 packet is rejected. handleInbound returns on the error.

RFC5880-6.8.6-6

If the My Discriminator field is zero, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting My Discriminator 0. TestRFC5880MyDiscriminatorZeroDiscarded fails unless ParseControl returns ErrZeroMyDisc; TestRFC5880MyDiscriminatorNonZeroAccepted fails if a nonzero value is rejected or mis-decoded. handleInbound returns on the error.

RFC5880-6.8.6-7

If the Your Discriminator field is nonzero, it MUST be used to select the session with which this BFD packet is associated. If no session is found, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). Selection clause: NEW TestRFC5880YourDiscriminatorSelectsAmongSessions holds two sessions to one peer on eth0/eth1; a packet arriving on eth0 naming eth1's discriminator reaches eth1's session only (first RemoteDiscr stays 0) and the mirror reaches the first, so selection by arrival tuple goes red (overlay selecting by byKey when YD != 0 reds it and the discard negative, job-ov8). Discard clause: - TestRFC5880UnknownYourDiscriminatorDiscarded unchanged and sound. Old one-session + kept as supplementary. Record: revert loop.go::handleInbound observed red.

RFC5880-6.8.6-8

If the Your Discriminator field is zero and the State field is not Down or AdminDown, the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD2 strict re-read 2026-09-27 (stale on Receive: additions sit after the discard test, which is still the first statement). Both State values the sentence names are driven: TestRFC5880ZeroYourDiscriminatorDiscardedWhenLive sends Your Discriminator 0 with State Init and Up to local Down, Init and Up, and requires ErrYourDiscriminatorReset, unchanged state and unchanged RemoteDiscr (a guard moved below the field updates goes red on RemoteDiscr). Positive TestRFC5880ZeroYourDiscriminatorAcceptedWhenDown accepts State Down and AdminDown in Down, AdminDown and Up. Local AdminDown is not in the negative loop; the sentence conditions only on the packet's State.

RFC5880-6.8.6-9

If the A bit is set and no authentication is in use (bfd.AuthType is zero), the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: processing A=1 at an AuthType-0 session. TestRFC5880UnauthenticatedSessionDiscardsAuthenticatedPacket fails unless Receive returns ErrAuthMismatch and the state stays Down; the engine hands such a packet to Receive because HasAuth is false. Positive TestRFC5880UnauthenticatedSessionAcceptsUnauthenticatedPacket: A=0 accepted.

RFC5880-6.8.6-10

If the A bit is clear and authentication is in use (bfd.AuthType is nonzero), the packet MUST be discarded. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: processing A=0 at an authenticated session. TestRFC5880AuthenticatedSessionDiscardsUnauthenticatedPacket fails unless Receive returns ErrAuthMismatch with the state unchanged; the engine skips Verify for A=0 and relies on this check. Positive TestRFC5880AuthenticatedSessionAcceptsAuthenticatedPacket: A=1 accepted.

RFC5880-6.8.6-11

If the A bit is set, the packet MUST be authenticated under the rules of section 6.7, based on the authentication type in use (bfd.AuthType). (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30. Positive TestRFC5880AuthenticatedUnderEachSessionAuthType: for each of the 5 Auth Types a session configured with it delivers a packet signed under it through handleInbound (RemoteDiscr learned), so a verifier fixed on one type fails. Negative TestRFC5880AuthenticatedPacketOfAnotherAuthTypeDiscarded: every configured type x every other type, same key id and secret, correctly signed, is discarded (RemoteDiscr 0); the Keyed-vs-Meticulous pairs of one hash isolate the Auth Type byte (same length and digest). Judge's own break (sha1.go Verify accepts any nonzero Auth Type) reds exactly those 4 pairs while the positive and both old Keyed SHA1 units stay green. Old tamper/wrong-key units kept.

RFC5880-6.8.6-12

If the Required Min Echo RX Interval field is zero, the transmission of Echo packets, if any, MUST cease. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD strict re-read 2026-09-27. One clause: a received Required Min Echo RX of zero ends echo transmission. Forbidden: an echo sent after that packet. Red: TestRFC5880EchoCeasesWhenPeerAdvertisesZero Fatal when EchoEnabled stays true, when PrimeEcho leaves the already-armed deadline set, or when EchoInterval is nonzero. The engine sends only from an armed deadline after its own EchoEnabled gate (echoTickLocked, echo.go), and PrimeEcho clears the deadline when echo is off, so removing either gate alone sends nothing and removing PrimeEcho's check reddens this unit. Contrast: TestRFC5880EchoEnabledWhenPeerAdvertisesNonZero keeps echo enabled and armed on a nonzero value.

RFC5880-6.8.6-13

If a Poll Sequence is being transmitted by the local system and the Final (F) bit in the received packet is set, the Poll Sequence MUST be terminated. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: a Poll that survives F=1. TestRFC5880FinalTerminatesPoll fails if PollOutstanding stays set after F=1; TestRFC5880NonFinalDoesNotTerminatePoll fails if F=0 clears it, so a clear-on-any-packet mutation goes red.

RFC5880-6.8.6-14

If bfd.RemoteDemandMode is 1, bfd.SessionState is Up, and bfd.RemoteSessionState is Up, Demand mode is active on the remote system and the local system MUST cease the periodic transmission of BFD Control packets (see section 6.8.7). (§6.8.6)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.6-14, so no unit is bound to it.

RFC5880-6.8.6-15

If bfd.RemoteDemandMode is 0, or bfd.SessionState is not Up, or bfd.RemoteSessionState is not Up, Demand mode is not active on the remote system and the local system MUST send periodic BFD Control packets (see section 6.8.7). (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Owner ruling 2026-09-30: no genuine negative exists, so the HEAD negative on TestRFC5880NoPeriodicTransmitWhileAdminDown (which proves the RFC5880-6.8.16-3 window, where it stays) was removed and the row carries {single-polarity: positive}. Judged on the positives: engine/rfc5880_demand_disjunct_test.go, one positive per disjunct with the other two false (ClearBothUp, SetLocalNotUpRemoteUp, SetLocalUpRemoteNotUp), each with a revert record on loop.go::tick observed red; rfc5880_demand_periodic_test.go and TestRFC5880PeriodicTransmitWhenRemoteDemandInactive supplementary. Ze never reads bfd.RemoteDemandMode, so it never enters the suppression the complement permits.

RFC5880-6.8.6-16

If a BFD Control packet is received with the Poll (P) bit set to 1, the receiving system MUST transmit a BFD Control packet with the Poll (P) bit clear and the Final (F) bit set as soon as practicable (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: no immediate F=1/P=0 reply to P=1. TestRFC5880PollAnsweredWithImmediateFinal fails if handleInbound sends nothing, or the reply lacks F or sets P; TestRFC5880NonPollProducesNoImmediateReply fails if a P=0 packet triggers a reply.

RFC5880-6.8.6-18

If the Your Discriminator field is zero, the session MUST be selected based on some combination of other fields, possibly including source addressing information, the My Discriminator field, and the interface over which the packet was received. (§6.8.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: selecting a zero-discriminator packet on nothing, or on fields the receiver cannot observe. TestRFC5881FirstPacketMatchesByTuple fails if the matching tuple is not delivered; TestRFC5881FirstPacketWrongSourceDropped fails if a wrong source is delivered; TestFirstPacketMatchesWhatTheTransportSurfaces fails if another interface or the wildcard local address selects the session.

RFC5880-6.8.7-1

With the exceptions listed in the remainder of this section, a system MUST NOT transmit BFD Control packets at an interval less than the larger of bfd.DesiredMinTxInterval and bfd.RemoteMinRxInterval, less applied jitter (see below). (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Engine TestRFC5880TickSpacesControlPacketsByLargerInterval ticks every 1 ms for 20 s with the peer Required Min RX 2 s above the 1 s floor and asserts every sent gap lies in [1.5 s, 2 s + 1 ms]. Targeted breaks observed red: TransmitInterval using DesiredMinTx alone (765 ms gap), tick ignoring the deadline (1 ms gap). Session units prove the larger-of in both orders and the jitter bound.

RFC5880-6.8.7-2

The periodic transmission of BFD Control packets MUST be jittered on a per-packet basis by up to 25%, that is, the interval MUST be reduced by a random value of 0 to 25% (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). The audit gap (tick never driven) is closed: NEW TestRFC5880PeriodicTransmitJitteredPerPacket drives Loop.tick through a stepped clock and a stamping transport for 200 sends at DetectMult 3; every gap between transmitted packets lies in (75%,100%] of TransmitInterval, >= 50 distinct gaps, and one reduced by more than 5%, so tick passing no reduction or a reused one goes red (overlay 'reduction * 0' reds both tick tests and no old one, job-ov10a; record revert loop.go::tick observed red). applyJitter + and band - kept.

RFC5880-6.8.7-3

If bfd.DetectMult is equal to 1, the interval between transmitted BFD Control packets MUST be no more than 90% of the negotiated transmission interval, and MUST be no less than 75% of the negotiated transmission interval. (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). NEW TestRFC5880PeriodicTransmitDetectMultOneWindow drives tick for 200 sends at DetectMult 1 and bounds every transmitted interval to [75%,90%] of TransmitInterval; overlay 'applyJitter(base, 3)' in tick reds ONLY this unit (job-ov10b); record revert loop.go::tick observed red. applyJitter-level + (DetectMultOneWindow) and - (floor only for DetectMult 1) kept.

RFC5880-6.8.7-4

The transmit interval MUST be recalculated whenever bfd.DesiredMinTxInterval changes, or whenever bfd.RemoteMinRxInterval changes, and is equal to the greater of those two values. (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. RA-BFD3 strict re-read 2026-09-27 after DF-BFD-7 moved settlePoll before the 1 s precondition in TestRFC5880DesiredMinTxChangeReschedulesNextTx (the old order asserted the Section 6.8.3 defect; no assertion removed). Clause 1, recalculated when bfd.DesiredMinTxInterval changes: forbidden is a pending TX still drawn from the old interval. Decrease: after the revert (1 s to 300 ms, RemoteMinRx 100 ms) the final Fatalf requires NextTxDeadline == last TX + 300 ms, red without the rescheduleTxLocked call in revertEchoSlowdownLocked (deadline stays at +1 s). Increase: the precondition Fatalf requires last TX + 1 s once the slow-down Poll has settled, red if TransmitInterval ignored the raised variable. Clause 2, recalculated when bfd.RemoteMinRxInterval changes: TestRFC5880RemoteMinRxChangeReschedulesNextTx requires the pending deadline at +400 ms after 900 to 400 and at +1.2 s after 400 to 1.2 s, red without the Receive reschedule. Clause 3, equal to the greater: 900 remote over 300 local (RemoteMinRxReductionHonoredImmediately), 1.2 s remote over 300 local, 300 local over 1 us remote (TransmitIntervalFlooredByLocalDesired, which is the negative: a remote value below the local target must not shorten TX, and RequiredMinRx alone must not move it). An increase of DesiredMinTx while Up is held until its Poll ends by Section 6.8.3, judged under RFC5880-6.8.3-3.

RFC5880-6.8.7-5

A system MUST NOT transmit BFD Control packets if bfd.RemoteDiscr is zero and the system is taking the Passive role. (§6.8.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Stale only because the RFC5880-6.1-3 negative tag comment was removed from session TestRFC5880PassiveRoleSilentUntilReception; body unchanged. Engine TestRFC5880PassiveTickSendsNothingWithoutRemoteDiscr recorded revert loop.go::tick; session TestRFC5880PassiveSilentOnceRemoteDiscrCleared (+) and TestRFC5880PassiveTransmitsAgainOnceRemoteDiscrLearned (-) recorded revert timers.go::transmitPermitted, all observed red.

RFC5880-6.8.7-6

A system MUST NOT periodically transmit BFD Control packets if bfd.RemoteMinRxInterval is zero. (§6.8.7)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.7-6, so no unit is bound to it.

RFC5880-6.8.7-7

A system MUST NOT periodically transmit BFD Control packets if Demand mode is active on the remote system (bfd.RemoteDemandMode is 1, bfd.SessionState is Up, and bfd.RemoteSessionState is Up) and a Poll Sequence is not being transmitted. (§6.8.7)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.7-7, so no unit is bound to it.

RFC5880-6.8.7-8

If rate limiting is in effect, the advertised value of Desired Min TX Interval MUST be greater than or equal to the interval between transmitted packets imposed by the rate limiting function. (§6.8.7)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.7-8, so no unit is bound to it.

RFC5880-6.8.4-1

If Demand mode is not active, and a period of time equal to the Detection Time passes without receiving a BFD Control packet from the remote system, and bfd.SessionState is Init or Up, the session has gone down -- the local system MUST set bfd.SessionState to Down and bfd.LocalDiag to 1 (Control Detection Time Expired). (§6.8.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). TestRFC5880DetectionExpiryDownDiagOne lost its 6.8.1-14 negative tag (comment only, body unchanged); it still proves expiry from Init sets Down and diag 1. Judgement unchanged: Judge rejudge 2026-09-30 (bfd session+engine continuation). TestRFC5880DetectionExpiryFromUpDownDiagOne adds expiry from Up (D bit clear and set in the last packet): 1 ns early no change, at the Detection Time Down, diag 1, one notify; Init expiry and the ignored-when-Down negative stand. Ze never sets bfd.DemandMode, so the 'Demand mode is not active' condition always holds; local Demand mode is an absent feature, not a branch to test. Mutant CheckDetection state guard observed red.

RFC5880-6.8.5-1

When the Echo function is active and a sufficient number of Echo packets have not arrived as they should, the session has gone down -- the local system MUST set bfd.SessionState to Down and bfd.LocalDiag to 2 (Echo Function Failed). (§6.8.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Engine TestRFC5880EngineFailsSessionOnMissingEchoes: echoTickLocked sends an echo, none returns, and the tick after the echo detection time leaves Down with diag 2; the test never calls EchoFail. The targeted break the earlier note named, removing the EchoFail call in echoTickLocked, observed red (state stays Up). Session +/- units unchanged.

RFC5880-6.8.15-1

When the forwarding plane in the local system is reset for some reason, such that the remote system can no longer rely on the local forwarding state, the local system MUST set bfd.LocalDiag to 4 (Forwarding Plane Reset), and set bfd.SessionState to Down. (§6.8.15)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.15-1, so no unit is bound to it.

RFC5880-6.8.16-4

If enabling session Set bfd.SessionState to Down (§6.8.16)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, netns+pinning). RFC 5880 §6.8.16 "If enabling session Set bfd.SessionState to Down". Positive TestRFC5880AdministrativeDisableEnable asserts exact Down after AdminEnable on an AdminDown session. Negative TestRFC5880EnableLandsOnDownWhilePeerSaysUpOrInit (R1 b) pushes the inputs toward the violation: Up session disabled, peer keeps sending Up then Init so bfd.RemoteSessionState is Up/Init (asserted as precondition), AdminEnable still lands on Down and Build() announces Down; an overlay adopting RemoteSessionState reds it (author e4-ov7). Old TestRFC5880AdministrativeCallsAreGuarded untagged (asserted a Ze guard, not this row). Revert records on fsm.go::AdminEnable observed red for both.

RFC5880-6.8.16-5

Else Set bfd.SessionState to AdminDown Set bfd.LocalDiag to an appropriate value Cease the transmission of BFD Echo packets (§6.8.16)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30. Row quotes the three disable steps of §6.8.16 verbatim. State and diag: session TestRFC5880AdministrativeDisableEnable asserts AdminDown and LocalDiag 7 after AdminDown from Up; engine TestRFC5880AdminDisableCeasesEchoes asserts the same through handle.Shutdown. Cease Echo: CeasesEchoes returns the first echo so detection stays clear, then 100 ticks at 1 ms (twice the 50 ms Required Min Echo RX) send nothing; the negative TestRFC5880AdminDisableIgnoresPeerEchoRequest forces the input toward the violation (peer keeps sending Up with a 50 ms echo request every 10 ms) and asserts no echo and AdminDown/diag 7. Judge re-observed: overlay break echo.go echoTickLocked gate `!= StateUp` -> `== StateDown` reddens both engine units at 50 ms. Revert records on echoTickLocked and AdminDown verify.

RFC5880-6.8.8-1

A received BFD Echo packet MUST be demultiplexed to the appropriate session for processing. (§6.8.8)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). NEW TestRFC5880EchoDemultiplexedAmongSessions: two Up echo sessions in one loop; a returning echo naming session 2 records its RTT on session 2 and leaves session 1 at zero, then one naming session 1 records on session 1, so delivery to 'the only/first session' goes red. Record revert echo.go::handleEchoInbound observed red. - TestRFC5880UnknownEchoDropped sound; old one-session + kept.

RFC5880-6.8.8-2

A means of detecting missing Echo packets MUST be implemented, which most likely involves processing of the Echo packets that are received. (§6.8.8)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Positive: engine TestRFC5880EngineFailsSessionOnMissingEchoes (the engine consults EchoDetectionExpired on its tick; removing the EchoFail branch observed red). Negative: engine TestRFC5880EngineReturnedEchoesKeepSessionUp returns every echo through handleEchoInbound and stays Up for three echo detection times; targeted break recordEchoRTTLocked not calling MatchEchoRx observed red (Down, diag 2). Session detector units unchanged.

RFC5880-6.8.9-1

BFD Echo packets MUST NOT be transmitted when bfd.SessionState is not Up. (§6.8.9)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). 'Not Up' now covered beyond AdminDown: NEW TestRFC5880NoEchoTransmittedInInitOrDown drives an Init session and a Down-after-Up session with echo still negotiated through handleInbound; an echo scheduler pass sends nothing and arms no schedule, while an Up session in the same loop does send (control). Overlay gating echo on '== AdminDown' reds both subtests (job-ov7); record revert echo.go::echoTickLocked observed red. + TestRFC5880EchoTransmittedWhileUp and AdminDown - kept.

RFC5880-6.8.9-2

BFD Echo packets MUST NOT be transmitted unless the last BFD Control packet received from the remote system contains a nonzero value in Required Min Echo RX Interval. (§6.8.9)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). TestRFC5880EchoFollowsLastAdvertisement sends 50 ms, 0, 50 ms and asserts EchoEnabled and the PrimeEcho deadline follow the LAST packet each time, closing the latch gap the earlier note named; mutant EchoEnabled != -> == observed red. The engine echoTickLocked sends only for an Up session with EchoEnabled and a primed deadline.

RFC5880-6.8.9-3

The interval between transmitted BFD Echo packets MUST NOT be less than the value advertised by the remote system in Required Min Echo RX Interval (§6.8.9)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd engine 2). Engine TestRFC5880EchoSteadySpacingHonorsPeerFloor: local 10 ms, peer 50 ms, no floor change; ticks at 1..49 ms send nothing, 50 ms sends. The targeted break the earlier note named, AdvanceEcho scheduling from DesiredMinEchoTxInterval alone, observed red (echo at 10 ms). Earlier engine and session units unchanged.

RFC5880-7-1

When BFD is used across multiple hops, a congestion control mechanism MUST be implemented (§7)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-7-1, so no unit is bound to it.

RFC5880-7-2

When BFD is used across multiple hops, a congestion control mechanism MUST be implemented, and when congestion is detected, the BFD implementation MUST reduce the amount of traffic it generates. (§7)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-7-2, so no unit is bound to it.

RFC5880-4.3-1

This byte MUST be set to zero on transmit (§4.3, §4.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-28 (bfd/auth, independent of the author). TestRFC5880ReservedByteZeroedOnTransmit signs into a buffer pre-filled with 0xFF for all four keyed types, so the zero at off+3 is written by digestSigner.Sign (buf[off+3] = 0), covering both cited sections 4.3 and 4.4. The {single-polarity: positive} annotation holds: Sign writes a constant 0 and no path emits another value.

RFC5880-6.7.2-2

the management interface by which the password is configured MUST accept ASCII strings, and SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form. (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-19 (independent auditor, after 95fae5058f). RFC 5880 Section 6.7.2: "For interoperability, the management interface by which the password is configured MUST accept ASCII strings, and SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form." 95fae5058f adds one comment line ("Both forms are accepted here.") above parseAuthSecret to satisfy godot; no statement of parseAuthConfig or parseAuthSecret changed, and the tagged units in rfc5880_key_management_hex_test.go are untouched. The comment is true: parseAuthSecret takes either the ASCII secret leaf or the secret-hex leaf (hex.DecodeString). Both tagged tests pass at HEAD (go test -overlay restoring HEAD for foreign dirty files, tags ze_core ze_bgp). The prior judgment stands unchanged: the positive test requires decoded Simple Password (0x00, 0xFF, 16-byte) keys byte for byte in the resolved session request, the negative sweeps every byte 0x00-0xFF, and an overlay replacing hex.DecodeString with []byte(written) turned both red. Mechanical shift; verdict holds.

RFC5880-6.7.4-9

bfd.XmitAuthSeq SHOULD be incremented when the session state changes, or when the transmitted BFD Control packet carries different contents than the previously transmitted packet. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (re-judge, independent of the author). Row is the Keyed SHA1 §6.7.4 SHOULD, quoted verbatim (rfc5880.txt 1409). engine/rfc5880_xmit_auth_seq_test.go drives a Keyed SHA1 session through the real transmit path (Loop.tick periodic, Loop.handleInbound Final) and parses the Sequence Number of every transmitted packet. + AdvancesOnStateAndContentChange: state clause (Down->Init->Up, preconditions pin the transmitted states, each seq differs) and contents clause (Final with F set, Up, then periodic with F clear, Up: seq differs). - AdvancesForAnOutOfTimerFinal (R1b: forces the producer input toward the violation): the Final sent from handleInbound at the same instant as the previous periodic packet carries a new seq, and every differing consecutive pair carries distinct seqs. Records revert AdvanceAuthSeq (+) and sendLocked (-), observed red; author's targeted overlays (advance only after periodic / only on timer) each red only their own unit, so the two units are not one assertion wearing two hats. MD5 twin 6.7.3-5 not covered here.

RFC5880-6.7.3-14

SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-19 (independent auditor, after 95fae5058f). RFC 5880 Section 6.7.3: "For interoperability, the management interface by which the key is configured MUST accept ASCII strings, and SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form." 95fae5058f adds one comment line ("Both forms are accepted here.") above parseAuthSecret to satisfy godot; no statement of parseAuthConfig or parseAuthSecret changed, and the tagged units in rfc5880_key_management_hex_test.go are untouched. The comment is true: parseAuthSecret takes either the ASCII secret leaf or the secret-hex leaf (hex.DecodeString). Both tagged tests pass at HEAD (go test -overlay restoring HEAD for foreign dirty files, tags ze_core ze_bgp). The prior judgment stands unchanged: the positive test requires decoded Keyed MD5 (1-byte and 16-byte) keys byte for byte in the resolved session request, the negative sweeps every byte 0x00-0xFF, and an overlay replacing hex.DecodeString with []byte(written) turned both red. Mechanical shift; verdict holds.

RFC5880-6.7.4-8

SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-19 (independent auditor, after 95fae5058f). RFC 5880 Section 6.7.4: "For interoperability, the management interface by which the key is configured MUST accept ASCII strings, and SHOULD also allow for the configuration of any arbitrary binary string in hexadecimal form." 95fae5058f adds one comment line ("Both forms are accepted here.") above parseAuthSecret to satisfy godot; no statement of parseAuthConfig or parseAuthSecret changed, and the tagged units in rfc5880_key_management_hex_test.go are untouched. The comment is true: parseAuthSecret takes either the ASCII secret leaf or the secret-hex leaf (hex.DecodeString). Both tagged tests pass at HEAD (go test -overlay restoring HEAD for foreign dirty files, tags ze_core ze_bgp). The prior judgment stands unchanged: the positive test requires decoded Keyed SHA1 (1-byte and 20-byte) keys byte for byte in the resolved session request, the negative sweeps every byte 0x00-0xFF, and an overlay replacing hex.DecodeString with []byte(written) turned both red. Mechanical shift; verdict holds.

RFC5880-6.8.16-2

BFD Control packets SHOULD be transmitted for at least a Detection Time after transitioning to AdminDown state in order to ensure that the remote system is aware of the state change. (§6.8.16)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 under OWNER RULING 3 (Ze sends AdminDown Control packets for 3x the Detection Time). Producer: session/fsm.go const adminDownTransmitDetectionTimes = 3, Machine.AdminDown sets adminDownTxEnd = now + 3 x max(local DetectionInterval, DetectMult x TransmitInterval read after the 1 s non-Up floor); Loop.tick sends until then; retireReleasedLocked keeps a released entry until AdminDownTransmitEnd, so the release path stays sending for the whole window. + TestRFC5880AdminDownControlTransmittedForADetectionTime (shutdown and release, peer silent, 30 s of ticks): first packet at the transition, every packet State AdminDown Diag 7, no gap over the announced interval, packets after 1x and 2x the Detection Time, last no earlier than 3x minus one interval, Detection Time computed from the packets themselves. Stopping before one Detection Time (the SHOULD's floor) reddens it. Judge overlays: factor 1 and 2 red both subtests ('none sent after N Detection Times'); window from the local Detection Time only reds both (remote half discriminated); factor 4 leaves it green (correct: sending longer satisfies the SHOULD). Record revert loop.go::tick re-recorded, observed red. {single-polarity: positive} still accepted: the obligation is to keep sending, silence after the window is 6.8.16-3's MAY.

RFC5880-6.8.16-3

BFD Control packets MAY be transmitted indefinitely after transitioning to AdminDown state in order to maintain session state in each system (§6.8.16)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-10-02 (tag move under the 2026-09-30 owner ruling, OWNER RULING 6(b)); judged by an agent that authored neither test. Stale only because the RFC5880-6.8.6-15 negative tag comment was removed from engine TestRFC5880NoPeriodicTransmitWhileAdminDown; body unchanged. Judged under OWNER RULING 3 on that test: sends at the transition, at start+1x+1ns and start+2x+1ns, nothing at exactly 3x nor an hour later; producer session/fsm.go adminDownTransmitDetectionTimes = 3 and Loop.tick; record revert loop.go::tick observed red. {single-polarity: negative} as before.

RFC5880-9-2

When a BFD session is directly connected across a single link (physical, or a secure tunnel such as IPsec), the TTL or Hop Count MUST be set to the maximum on transmit, and checked to be equal to the maximum value on reception (and the packet dropped if this is not the case). (§9)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (rejudge, 6-2 + rest). Transmit: IPv4 IP_TTL 255 (TestRFC5880SingleHopTransmitTTLIsMaximum) and NEW IPv6 IPV6_UNICAST_HOPS 255 on a [::1] single-hop socket (TestRFC5880SingleHopTransmitHopLimitIsMaximumIPv6; record revert udp_linux.go::applySocketOptionsV6 observed red). Receive: NEW + TestRFC5880SingleHopReceiveTTLMaxAccepted (TTL 255 delivered, RemoteDiscr set; record revert loop.go::passesTTLGate observed red) beside - TestRFC5880SingleHopReceiveTTLNotMaxDiscarded, so a gate dropping every packet now goes red. Both audit gaps closed.

RFC5880-6.8.14-1

If Demand mode is no longer active on the remote system, the local system MUST begin transmitting periodic BFD Control packets (§6.8.14)

Audit verdict: not audited: no reader has judged these tests

RFC5880-6.8.17-1

If Demand mode is active on the remote system (the local system is not transmitting periodic BFD Control packets), a Poll Sequence MUST be initiated to ensure that the diagnostic code is transmitted. (§6.8.17)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC5880-6.8.17-1, so no unit is bound to it.

RFC5880-6.8.3-8

In any case other than those explicitly called out above, timing parameter changes MUST be effected immediately (changing the transmission rate and/or the Detection Time). (§6.8.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (bfd session+engine continuation). Row is {single-polarity: positive}. TestRFC5880RemoteTimingChangeMovesDetectionTimeAtOnce adds the Detection Time half: a received Desired Min TX 600 ms moves it 900 ms -> 1.8 s at once (no expiry at 901 ms, expiry at 1.8 s) and Detect Mult 5 moves it to 1.5 s; the TX half stays on RemoteMinRxReductionHonoredImmediately. Mutant DetectionInterval mult guard observed red.

RFC5880-6.7.3-7

the management interface by which the key is configured MUST accept ASCII strings (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30. Same config-text -> YANG -> plugin section -> resolveProfile units as 6.7.2-1, keyed-md5 and meticulous-keyed-md5 subtests (keys up to 16 bytes): positive a plain ASCII key, negative (R1b) the 0x01-0x7F sweep with leading/trailing spaces; judge's trailing-space-strip break reds both MD5 negative subtests, positive green. Revert records observed red. The incomplete-block refusal is untagged now (Ze's own rule, D-15).

RFC5880-6.7.2-3

The currently selected password and Key ID for the session MUST be stored in the Authentication Section of each outgoing BFD Control packet. (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (phase 8: the Keyed SHA1 key-id units moved to RFC5880-6.7.4-10, row cites 6.7.2 only). Positive TestRFC5880SimplePasswordSectionCarriesPasswordAndKeyID asserts the selected password and Key ID on the signed wire. Negatives TestRFC5880SimplePasswordOtherThanSelectedPairDiscarded (key id 4/6/255 with the right password, password changed in first/middle/last byte, ErrPasswordMismatch each, selected pair accepted) and TestRFC5880SimplePasswordSignerNeedsPassword (nil/empty password refused at NewSigner). Units unchanged; judgement unchanged.

RFC5880-6.7.3-8

The Sequence Number field MUST be set to bfd.XmitAuthSeq. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (phase 8: row cites 6.7.3 only; the Keyed SHA1 session units moved to RFC5880-6.7.4-11). Positive TestRFC5880MD5SequenceFieldIsXmitAuthSeq (new): both MD5 types through Machine.Sign, field = 0x11223344 and then the advanced value. Negative (R1b, forced input) TestRFC5880SequenceFieldIsXmitAuthSeqAcrossTheCounterRange: XmitAuthSeq forced to 0, 1, 0x7FFFFFFF, 0x80000000, 0xFFFFFFFE, 0xFFFFFFFF and across the wrap, field equal after every Sign, all four keyed types; an earlier judge break (seq masked to 31 bits) reds it.

RFC5880-6.7.2-4

If the received BFD Control packet does not contain an Authentication Section, or the Auth Type is not 1 (Simple Password), then the received packet MUST be discarded. (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (phase 8: row cites 6.7.2 only; the SHA1 type units moved to RFC5880-6.7.4-14, the MD5 clause is RFC5880-6.7.3-16). Positive accepts Auth Type 1 sections for 1/8/16-byte passwords; negative TestRFC5880SimplePasswordMissingSectionOrOtherTypeDiscarded refuses an A-clear Length-24 packet (ErrShortAuthBody) and types 0,2,3,4,5,6,255 with every other field valid, isolated because Simple Password has no digest. Stack-level no-section discard is Receive's A-bit gate (RFC5880-6.8.6-10).

RFC5880-6.7.2-5

If the Auth Key ID field does not match the ID of a configured password, the received packet MUST be discarded. (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (phase 8: row cites 6.7.2 only; the SHA1 key-id units moved to RFC5880-6.7.4-15). Negative TestRFC5880SimplePasswordWrongKeyIDDiscarded signs key 7 with the right password against a verifier for key 8 and requires ErrPasswordMismatch (only the key id differs, isolated); positive TestRFC5880SimplePasswordMatchingKeyIDAccepted accepts key 7.

RFC5880-6.7.2-6

If the Auth Len field is not equal to the length of the password selected by the key ID, plus three, the packet MUST be discarded. (§6.7.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (phase 8: row cites 6.7.2 only; the SHA1 Auth Len units moved to RFC5880-6.7.4-16). Positive accepts Auth Len = password+3 for 1/8/16 bytes; negative changes only the Auth Len byte (0, n+2, n+4, 255) with Control Length, type, key id and password valid and requires ErrPasswordMismatch; removing the byte check in simpleVerifier.Verify accepts them.

RFC5880-6.7.3-16

If the received BFD Control packet does not contain an Authentication Section, or the Auth Type is not correct (2 for Keyed MD5 or 3 for Meticulous Keyed MD5), then the received packet MUST be discarded. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880MD5AuthTypeCorrectAccepted (types 2 and 3). Negative TestRFC5880KeyedMissingSectionOrWrongTypeDiscarded: A-clear Length-24 packet -> ErrShortAuthBody, and types 0,1,2..6,255 relabelled on an authentic packet -> discard with the replay floor unset. Judge break removing the Auth Type check in digestVerifier.Verify reds it (the floor assertion isolates it from the digest). The no-section clause at stack level is enforced by Receive's A-bit gate (session/fsm.go, proven under RFC5880-6.8.6-10, loop.go skips Verify for A=0); this unit proves the verifier refuses it too.

RFC5880-6.7.3-17

If the Auth Key ID field does not match the ID of a configured authentication key, the received packet MUST be discarded. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880MD5ConfiguredKeyIDAccepted; negative TestRFC5880MD5UnconfiguredKeyIDDiscarded (ids 2/4/255 vs 3, both MD5 types, floor unset). Judge break removing the key-id check in digestVerifier.Verify reds the negative (floor seeded), so it is isolated from the digest.

RFC5880-6.7.3-18

If the Auth Len field is not equal to 24, the packet MUST be discarded. (§6.7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880MD5AuthLen24Accepted (byte 24, Length 48); negative TestRFC5880MD5AuthLenNot24Discarded (byte 0/23/25/28 with floor unset, Length 47 ErrShortAuthBody, 49 refused). Judge break removing the Auth Len byte check in digestVerifier.Verify reds the negative through the floor assertion.

RFC5880-6.7.4-14

If the received BFD Control packet does not contain an Authentication Section, or the Auth Type is not correct (4 for Keyed SHA1 or 5 for Meticulous Keyed SHA1), then the received packet MUST be discarded. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880AuthTypeMatchAccepted (type 5). Negative TestRFC5880KeyedMissingSectionOrWrongTypeDiscarded covers types 4 and 5 (no section; types 0,1,2,3,6,255 and the other SHA1 variant) with the floor unset, and the judge break removing the Auth Type check reds it. The moved negative TestRFC5880AuthTypeMismatchDiscarded stayed GREEN under that break: it asserts only err != nil and the relabelled byte also breaks the hash, so it is digest-confounded and proves nothing alone. No-section clause at stack level: RFC5880-6.8.6-10.

RFC5880-6.7.4-15

If the Auth Key ID field does not match the ID of a configured authentication key, the received packet MUST be discarded. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (phase 8). Positive TestRFC5880AuthKeyIDMatchAccepted (key 3); negative TestRFC5880AuthKeyIDMismatchDiscarded (key 4 vs 3, ErrDigestMismatch, floor unset). Judge break removing the key-id check reds the negative through the floor assertion. Ze configures one key per session, so 'a configured key' is that key.

RFC5880-6.7.4-16

If the Auth Len field is not equal to 28, the packet MUST be discarded. (§6.7.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge rejudge 2026-09-30 (last five). Earlier weak finding closed: new negative auth/rfc5880_sha1_authlen_test.go::TestRFC5880SHA1AuthLenByteDiscardedWithAuthenticDigest hashes the digest over the forged Auth Len byte (0/20/24/27/29/255) for Keyed SHA1 and Meticulous Keyed SHA1, keeps Control Length and the other section fields authentic, and asserts ErrDigestMismatch plus bfd.RcvAuthSeq unseeded, so only the Auth Len check can refuse it. Judge break (int(data[off+1]) != v.bodyLen -> if false && ..., sha1.go Verify, go overlay): new negative RED ('type 4: Auth Len 0 with an authentic digest: got <nil>'), new positive and the old pair green. Positive TestRFC5880SHA1AuthLen28HandBuiltAccepted shows the same builder at 28 is accepted (isolation). Old TestRFC5880AuthLenMismatchDiscarded keeps its tag but does not discriminate the Auth Len byte (digest refuses it); supplementary only. Records: Verify revert, observed red, all four units.