a positive test proves Ze does what the requirement demands and a negative one proves it refuses what the requirement forbids
Partial
RFC 7854 - BGP Monitoring Protocol (BMP)
Every requirement this repository extracted from RFC 7854, the tests bound to it, and what a reader has verified about them. This summary is enrolled and gated by ./le rfc check.
Overview
Positive
what Ze has
the requirement admits no counter-case, so one polarity plus a recorded reason is the whole proof available for it
one direction is tested, the other is neither tested nor excused, and nothing states which
scoped tests exist; the remaining obligation is unmet or unproven, with zero whole-requirement credit
no test carries the requirement id, whether or not a gap states why
a red was observed once under a recorded procedure, and the unit, the claim and the producer it rested on still hash to what was recorded. The break is not re-run. A test pair is not a proof until one has been observed
0 weak, wrong or unimplemented, 0 no longer current. Each is named below under its own requirement id
Neutral
measures that are neither good news nor bad
MUST-level requirements the gate HOLDS. A population, not a result: the shares beside it are what says how Ze stands
an obligation that does not bind Ze. A {not-applicable} annotation says it never bound; a {feature-declined} annotation says its condition is an optional feature Ze does not offer, and quotes the RFC sentence that makes it optional. Scope, not coverage: it stays in the denominator every share on this page is taken over
a {not-applicable} annotation says the obligation does not bind Ze, so no test is owed for it. It stays in the denominator every share here is taken over
a {lower-layer} annotation says a layer under Ze performs the behavior, on state Ze installs into that layer, and names the producer that installs it. The obligation binds Ze and is met; Ze proves none of it, because its own boundary carries no value the behavior reads
a {feature-declined} annotation says the obligation is conditional on a feature the RFC makes optional and Ze does not offer, and it quotes the sentence that makes it optional. The condition is false, so nothing is owed and nothing is missing. It stays in the denominator every share here is taken over
The 8 shares marked as a part above are the whole of the 39 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.
How to read the colors
A color names what the measure MEANS, not how well Ze scores on it. Green is a good outcome at any value, red is a bad one, and neither a population nor a scope count is an outcome, so both take no color. The number under the label is what says how far Ze has got.
| Card | Tone here | Why that color |
|---|---|---|
| Gated MUSTs | neutral | no color: a population is a scale, and a larger one is neither good news nor bad. It is the accounting total |
| Out of scope | neutral | no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim |
| Tested both ways | ok | green at every value: a test pair is the outcome this gate exists to produce, and the share under the label is what says how far Ze has got |
| One polarity plus reason | ok | green at every value: where no counter-case exists, one polarity IS the complete answer, and a recorded reason is what the gate demands beside it |
| One polarity, unexcused | ok | green at zero, RED above it: half a proof with no reason for the other half |
| Partial proof; remaining gap | ok | green at zero, RED above it: a tested clause cannot prove the whole requirement |
| No test at all | ok | green at zero, RED above it: a binding obligation nothing exercises is a claim with nothing behind it, whether or not a reason is stated |
| Not applicable | neutral | no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim |
| Met below Ze | neutral | no color: an obligation met below Ze is neither a test Ze wrote nor work Ze owes, and the two green shares above are what says how much Ze proves itself |
| Optional feature declined | neutral | no color: an obligation whose condition Ze never meets is neither an achievement nor a failure. The absent FEATURE is disclosed on the RFC's own status row, as an implementation gap a later scope decision can revisit |
| Proven by a recorded break | ok | green at every value: an observed break is the outcome the discrimination gate exists to produce. The denominator is TAGGED UNITS, not obligations, so this share is not one of the parts above |
| Audit verdicts | ok | RED on the first weak, wrong or unimplemented verdict, amber while a verdict is no longer current or a gated MUST is unjudged, green when every one is judged sound and current |
At a glance
| Field | Value |
|---|---|
| Public status | Partial |
| Enrolment | Enrolled |
| Requirements | 48 |
| Gated MUST-level | 39 |
| Not applicable, so out of scope | 0 |
| Declared gaps | 0 |
| Declared gaps a test demonstrates | 0 |
| Gated with no test | 0 |
| Nightly-only evidence | 0 |
| Test tags | 99 |
| Tagged units | 99 |
| Recorded audit verdicts | 43 |
| Discrimination records | 53 |
| Summary | rfc/short/rfc7854.md |
| Requirement shard | rfc/requirements/rfc7854.md |
| RFC text | rfc/full/rfc7854.txt |
Enrolment
Enrolled: Ze implements the BMP sender and receiver under internal/component/bgp/plugins/bmp. Wire-message and session carriers cover the common and per-peer headers, OPEN exchange, current per-peer replay and completion, identity, ordered information, termination and statistics. Requirement coverage and discrimination remain subject to the current gate result.
What the public ledger says
Status: Partial
What the ledger says is covered
- BMP receiver and sender, peer lifecycle, current per-NLRI replay with per-family End-of-RIB, received and sent route monitoring, CLI and configuration. Initiation carries the administrative system identity
- receiver information strings retain order and duplicates. Sender shutdown carries Reason 0 and closes
- bounded transmit queues reset stalled sessions.
What the ledger says remains
Focused execution, producer discrimination and third-party pmacct acceptance of the current changes remain unrun. Loc-RIB monitoring is defined under RFC 9069 and Adj-RIB-Out under RFC 8671. Post-policy Adj-RIB-In monitoring, the optional view with the L flag set on received routes, is not offered: the route-monitoring-policy post-policy choice streams the Adj-RIB-Out.Coverage
| Bucket | Count | What it counts |
|---|---|---|
| Positive and negative tests | 31 | one part of the gated population |
| Annotated (including scoped evidence) | 8 | one part of the gated population |
| One polarity only | 0 | one part of the gated population |
| No test and no annotation | 0 | one part of the gated population |
| Partial proof; remaining gap (subset of annotated; zero whole-requirement credit) | 0 | an overlay: each of these is also counted by the part it falls in |
| Evidence that runs nightly only | 0 | an overlay: each of these is also counted by the part it falls in |
| Derived from other rows | 0 | outside the gated population: each asserts nothing and derives its state from the rows it names, which the parts above already count |
| Gated MUST-level requirements | 39 | every gated MUST falls in exactly one bucket above |
Positive and negative tests (31): RFC7854-x-1, RFC7854-x-2, RFC7854-x-3, RFC7854-x-5, RFC7854-x-8, RFC7854-4.9-1, RFC7854-4.5-2, RFC7854-x-18, RFC7854-3.2-1, RFC7854-3.2-2, RFC7854-3.3-1, RFC7854-4.1-1, RFC7854-4.2-1, RFC7854-4.3-2, RFC7854-4.4-1, RFC7854-4.4-2, RFC7854-4.4-3, RFC7854-4.5-1, RFC7854-4.5-3, RFC7854-4.5-4, RFC7854-4.7-1, RFC7854-4.7-2, RFC7854-4.7-3, RFC7854-4.8-1, RFC7854-4.8-2, RFC7854-4.8-3, RFC7854-4.10-1, RFC7854-5-1, RFC7854-5-2, RFC7854-5-4, RFC7854-8.2-1
Annotated (including scoped evidence) (8): RFC7854-x-4, RFC7854-x-6, RFC7854-x-7, RFC7854-x-9, RFC7854-x-10, RFC7854-x-12, RFC7854-4.5-5, RFC7854-5-6
Requirements
| Requirement | Level | Section | Tests |
|---|---|---|---|
RFC7854-x-1 | This is set to '3' for all messages defined in this specification. (§4.1, Common Header) | ||
| MUST | 4.1 | ||
RFC7854-x-2 | Version (1 byte): Indicates the BMP version. This is set to '3' for all messages defined in this specification. ('1' and '2' were used by draft versions of this document.) Version 0 is reserved and MUST NOT be sent. o Message Length (4 bytes): Length of the message in bytes (including headers, data, and encapsulated messages, if any). o Message Type (1 byte): This identifies the type of the BMP message. (§4.1, Common Header) | ||
| MUST | 4.1 | ||
RFC7854-x-3 | The per-peer header follows the common header for most BMP messages. (§4.2, Per-Peer Header) | ||
| MUST | 4.2 | ||
RFC7854-x-4 | If a 16-bit AS number is stored in this field [RFC6793], it should be padded with zeroes in the 16 most significant bits. (§4.2, Per-Peer Header) | ||
| MUST | 4.2 | negative
no testno negative test{single-polarity}: the Peer AS is unconditionally a 4-octet field on every encode and decode, so there is no shorter-AS variant to reject and no negative case to construct |
|
RFC7854-x-5 | It is 4 bytes long if an IPv4 address is carried in this field (with the 12 most significant bytes zero-filled) and 16 bytes long if an IPv6 address is carried in this field. (§4.2, Per-Peer Header) | ||
| MUST | 4.2 | ||
RFC7854-x-6 | An initiation message MUST be sent as the first message after the TCP session comes up. (§4.3, Initiation Message) | ||
| MUST | 4.3 | negative
no testno negative test{single-polarity}: the sender always emits Initiation as the first message on a fresh connection, so there is no valid session in which another message precedes it to reject |
|
RFC7854-x-7 | The sysDescr and sysName Information TLVs MUST be sent, any others are optional. (§4.3, Initiation Message) | ||
| MUST | 4.3 | negative
no testno negative test{single-polarity}: the Initiation the sender builds always includes the sysName TLV, so there is no valid Initiation omitting it to assert against |
|
RFC7854-x-8 | Sent OPEN Message: The full OPEN message transmitted by the monitored router to its peer. o Received OPEN Message: The full OPEN message received by the monitored router from its peer. (§4.10, Peer Up Notification) | ||
| MUST | 4.10 | ||
RFC7854-x-9 | Following the common BMP header and per-peer header is a BGP Update PDU. (§4.6, Route Monitoring) | ||
| MUST | 4.6 | negative
no testno negative test{single-polarity}: Route Monitoring is only ever constructed around a complete BGP UPDATE PDU, so there is no valid Route Monitoring lacking one to reject |
|
RFC7854-x-10 | Reason indicates why the session was closed. (§4.9, Peer Down Notification) | ||
| MUST | 4.9 | negative
no testno negative test{single-polarity}: Peer Down is always written with a reason byte, so there is no valid Peer Down without one to assert against |
|
RFC7854-x-11 | The router MAY send a Termination message prior to closing the session. (§3.3, Lifecycle of a BMP Session) | ||
| MAY | 3.3 | negative
no testno negative test{single-polarity}: Termination is produced unconditionally when the session is torn down, so there is no valid shutdown that omits it to reject |
|
RFC7854-x-12 | No BMP message is ever sent from the monitoring station to the monitored router. (§3.2, Connection Establishment and Termination) | ||
| MUST | 3.2 | negative
no testno negative test{single-polarity}: the receiver loop (internal/component/bgp/plugins/bmp/bmp.go:441-492) issues only reads and the sender hold-loop (sender.go:207-237) reads only to detect close, so neither role writes toward the monitored router on a valid session and there is no reject case to construct |
|
RFC7854-4.9-1 | Reason 1: The local system closed the session. Following the Reason is a BGP PDU containing a BGP NOTIFICATION message that would have been sent to the peer. o Reason 2: The local system closed the session. No notification message was sent. Following the reason code is a 2-byte field containing the code corresponding to the Finite State Machine (FSM) Event that caused the system to close the session (see Section 8.1 of [RFC4271]). Two bytes both set to 0 are used to indicate that no relevant Event code is defined. o Reason 3: The remote system closed the session with a notification message. Following the Reason is a BGP PDU containing the BGP NOTIFICATION message as received from the peer. (§4.9, Peer Down Notification) | ||
| MUST | 4.9 | ||
RFC7854-4.5-2 | Likewise, the monitoring station MUST close the TCP session after receiving a termination message. (§4.5, Termination Message) | ||
| MUST | 4.5 | ||
RFC7854-x-13 | Exponential backoff with a default initial backoff of 30 seconds and a maximum of 720 seconds is suggested. (§3.2, Connection Establishment and Termination) | ||
| SHOULD | 3.2 | positive
no testno positive testnegative
no testno negative test |
|
RFC7854-x-14 | Exponential backoff with a default initial backoff of 30 seconds and a maximum of 720 seconds is suggested. (§3.2, Connection Establishment and Termination) | ||
| SHOULD | 3.2 | positive
no testno positive testnegative
no testno negative test |
|
RFC7854-x-15 | It MAY periodically send Stats Reports or even new Initiation messages, according to configuration. (§3.3, Lifecycle of a BMP Session) | ||
| MAY | 3.3 | ||
RFC7854-x-16 | It subsequently sends a Peer Up message over the BMP session for each of its monitored BGP peers that is in the Established state. (§3.3, Lifecycle of a BMP Session) | ||
| SHOULD | 3.3 | ||
RFC7854-x-17 | It subsequently sends a Peer Up message over the BMP session for each of its monitored BGP peers that is in the Established state. It follows by sending the contents of its Adj- RIBs-In (pre-policy, post-policy, or both, see Section 5) encapsulated in Route Monitoring messages. (§3.3, Lifecycle of a BMP Session) | ||
| SHOULD | 3.3 | ||
RFC7854-x-18 | The sysDescr and sysName Information TLVs MUST be sent, any others are optional. (§4.3, Initiation Message) | ||
| MUST | 4.3 | ||
RFC7854-x-19 | Information: Information about the peer, using the Information TLV (Section 4.4) format. Only the string type is defined in this context; it may be repeated. Inclusion of the Information field is OPTIONAL. (§4.10, Peer Up Notification) | ||
| MAY | 4.10 | positive
no testno positive testnegative
no testno negative test |
|
RFC7854-x-20 | Route Mirroring messages are used for verbatim duplication of messages as received. A possible use for mirroring is exact mirroring of one or more monitored BGP sessions, without state compression. (§4.7, Route Mirroring) | ||
| MAY | 4.7 | positive
no testno positive testnegative
no testno negative test |
|
RFC7854-3.2-1 | Retries MUST be subject to some variety of backoff. (§3.2, Connection Establishment and Termination) | ||
| MUST | 3.2 | ||
RFC7854-3.2-2 | The router MUST also restrict the rate at which sessions may be established. (§3.2, Connection Establishment and Termination) | ||
| MUST | 3.2 | ||
RFC7854-3.3-1 | Once it has sent all the routes for a given peer, it MUST send an End-of-RIB message for that peer (§3.3, Lifecycle of a BMP Session, and restated in the Route Monitoring section) | ||
| MUST | 3.3 | ||
RFC7854-4.1-1 | A BMP implementation MUST ignore unrecognized message types upon receipt. (§4.1, Common Header) | ||
| MUST | 4.1 | ||
RFC7854-4.2-1 | The remaining bits are reserved for future use. They MUST be transmitted as 0 and their values MUST be ignored on receipt. (§4.2, Per-Peer Header) | ||
| MUST | 4.2 | ||
RFC7854-4.3-1 | The string TLV MAY be included multiple times. (§4.3, Initiation Message) | ||
| MAY | 4.3 | positive
no testno positive testnegative
no testno negative test |
|
RFC7854-4.3-2 | The initiation message consists of the common BMP header followed by two or more Information TLVs (Section 4.4) containing information about the monitored router. (§4.3, Initiation Message) | ||
| MUST | 4.3 | ||
RFC7854-4.4-1 | If multiple strings are included, their ordering MUST be preserved when they are reported. (§4.4, Information TLV) | ||
| MUST | 4.4 | ||
RFC7854-4.4-2 | Type = 1: sysDescr. The Information field contains an ASCII string whose value MUST be set to be equal to the value of the sysDescr MIB-II [RFC1213] object. (§4.4, Information TLV) | ||
| MUST | 4.4 | ||
RFC7854-4.4-3 | Type = 2: sysName. The Information field contains an ASCII string whose value MUST be set to be equal to the value of the sysName MIB-II [RFC1213] object. (§4.4, Information TLV) | ||
| MUST | 4.4 | ||
RFC7854-4.5-1 | Once the router has sent a termination message, it MUST close the TCP session without sending any further messages. (§4.5, Termination Message) | ||
| MUST | 4.5 | ||
RFC7854-4.5-3 | Type = 1: Reason. The Information field contains a 2-byte code indicating the reason that the connection was terminated. Some reasons may have further TLVs associated with them. Inclusion of this TLV is REQUIRED. (§4.5, Termination Message) | ||
| MUST | 4.5 | ||
RFC7854-4.5-4 | The termination message consists of the common BMP header followed by one or more TLVs containing information about the reason for the termination (§4.5, Termination Message) | ||
| MUST | 4.5 | ||
RFC7854-4.5-5 | Although use of this message is RECOMMENDED, a monitoring station must always be prepared for the session to terminate with no message. (§4.5, Termination Message) | ||
| MUST | 4.5 | negative
no testno negative test{single-polarity}: a router that closes with no Termination message sends no non-compliant input, because the sentence permits exactly that close, so the station has nothing to refuse. TestBMPReceiverEndsTheSessionWhenTheRouterLeavesWithoutTermination proves the station clause and TestSenderStopSendsTerminationToCollector proves the RECOMMENDED clause on the router side |
|
RFC7854-4.7-1 | If the BGP Message TLV occurs in the Route Mirroring message, it MUST occur last in the list of TLVs. (§4.7, Route Mirroring) | ||
| MUST | 4.7 | ||
RFC7854-4.7-2 | Code = 0: Errored PDU. The contained message was found to have some error that made it unusable, causing it to be treated-as- withdraw [RFC7606]. A BGP Message TLV MUST also occur in the TLV list. (§4.7, Route Mirroring) | ||
| MUST | 4.7 | ||
RFC7854-4.7-3 | Following the common BMP header and per-peer header is a set of TLVs that contain information about a message or set of messages. (§4.7, Route Mirroring) | ||
| MUST | 4.7 | ||
RFC7854-4.8-1 | A BMP implementation MUST ignore unrecognized stat types on receipt, and likewise MUST ignore unexpected data in the Stat Data field. (§4.8, Stats Reports) | ||
| MUST | 4.8 | ||
RFC7854-4.8-2 | However, if an SR message is transmitted, at least one statistic MUST be carried in it. (§4.8, Stats Reports) | ||
| MUST | 4.8 | ||
RFC7854-4.8-3 | Following the common BMP header and per-peer header is a 4-byte field that indicates the number of counters in the stats message where each counter is encoded as a TLV. (§4.8, Stats Reports) | ||
| MUST | 4.8 | ||
RFC7854-4.10-1 | Following the common BMP header and per-peer header is the following (§4.10, Peer Up Notification) | ||
| MUST | 4.10 | ||
RFC7854-5-1 | Pre-policy routes MUST have their L flag clear in the BMP header (see Section 4), post-policy routes MUST have their L flag set. (§5, Route Monitoring) | ||
| MUST | 5 | ||
RFC7854-5-2 | If the implementation is able to provide information about when routes were received, it MAY provide such information in the BMP Timestamp field. Otherwise, the BMP Timestamp field MUST be set to 0, indicating that time is not available. (§5, Route Monitoring) | ||
| MUST | 5 | ||
RFC7854-5-4 | The withdraw MUST have its L flag set to correspond to that of any previous announcement (§5, Route Monitoring) | ||
| MUST | 5 | ||
RFC7854-5-6 | When a change occurs to a route, such as an attribute change, the router must update the monitoring station with the new attribute. (§5, Route Monitoring) | ||
| MUST | 5 | negative
no testno negative test{single-polarity}: every received UPDATE that changes a route is compliant input to the router, so the sender holds no refusal path. TestRFC7854ChangedAttributesCanReturnToEarlierValue asserts one Route Monitoring message for each ORIGIN change, including the return to an earlier value |
|
RFC7854-8.2-1 | Since in this case no transport session actually exists, the Local and Remote Port fields of the Peer Up message MUST be set to 0. (§8.2, Peer Up Notification) | ||
| MUST | 8.2 | ||
Gaps and untested MUSTs
RFC 7854 declares no gap, and every gated MUST it carries has a test bound to it.
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.
RFC7854-x-1
This is set to '3' for all messages defined in this specification. (§4.1, Common Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. rfc7854_wire_header_test.go::TestRFC7854EveryTransmittedMessageCarriesVersion3AndItsTotalLength builds all seven types through the writers the sender calls (writeRouteMonitoring, writeStatisticsReport, writePeerDown, writePeerUp, writeInitiation, writeTermination, writeRouteMirroring) into a 0xA5-patterned buffer and requires octet 0 == 3 on each, so a writer that emits another version or leaves the octet unset goes red. The sentence binds the sender and no input can make it send another version; the negatives (header_test decode table #2, session_test TestBMPMalformedHeaderDrops) are the receiver refusing a version-2 header, the same rule read at the other end. The old decode-table positive stays tagged and proves only decode.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestBMPCommonHeaderDecode |
unit/verify | unproven |
| negative | TestBMPMalformedHeaderDrops |
unit/verify | unproven |
| positive | TestBMPCommonHeaderDecode |
unit/verify | unproven |
| positive | TestRFC7854EveryTransmittedMessageCarriesVersion3AndItsTotalLength |
unit/verify | revert, verified |
RFC7854-x-2
Version (1 byte): Indicates the BMP version. This is set to '3' for all messages defined in this specification. ('1' and '2' were used by draft versions of this document.) Version 0 is reserved and MUST NOT be sent. o Message Length (4 bytes): Length of the message in bytes (including headers, data, and encapsulated messages, if any). o Message Type (1 byte): This identifies the type of the BMP message. (§4.1, Common Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. TestRFC7854EveryTransmittedMessageCarriesVersion3AndItsTotalLength reads the transmitted octets of all seven types: octet 0 == 3 (so never the reserved 0), octets 1-4 == the whole message computed independently from the case's own inputs (common header + per-peer header where present + data) and equal to the octets the writer produced, and octet 5 == the type. Each clause of the quoted definition is asserted on a sent message. The tagged negative (header_test, a 3-octet buffer refused) is thin, but the clauses are sender field definitions with no input to refuse; the positive discriminates every one.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestBMPCommonHeaderDecode |
unit/verify | unproven |
| positive | TestBMPCommonHeaderEncode |
unit/verify | unproven |
| positive | TestRFC7854EveryTransmittedMessageCarriesVersion3AndItsTotalLength |
unit/verify | revert, verified |
RFC7854-x-3
The per-peer header follows the common header for most BMP messages. (§4.2, Per-Peer Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. rfc7854_wire_header_test.go::TestRFC7854PerPeerHeaderFollowsTheCommonHeader writes all seven types and decodes a per-peer header at octet 6 of Route Monitoring, Statistics Report, Peer Down, Peer Up and Route Mirroring, requiring it to equal the header the writer was given (4-octet AS 4200000001); for Initiation and Termination it requires the first TLV (type 1, length 2) at octet 6 and a message too short to hold a per-peer header, which is the 'most' of the sentence. The older TestHasPeerHeader tags stay: hasPeerHeader has no non-test caller, so those two tags prove a helper table only.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestHasPeerHeader |
unit/verify | unproven |
| negative | TestRFC7854PerPeerHeaderFollowsTheCommonHeader |
unit/verify | revert, verified |
| positive | TestHasPeerHeader |
unit/verify | unproven |
| positive | TestRFC7854PerPeerHeaderFollowsTheCommonHeader |
unit/verify | revert, verified |
RFC7854-x-4
If a 16-bit AS number is stored in this field [RFC6793], it should be padded with zeroes in the 16 most significant bits. (§4.2, Per-Peer Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. rfc7854_wire_header_test.go::TestRFC7854PeerASIsFourOctetsWithTheShortASZeroPadded writes a Peer Down (writePeerHeader) into a patterned buffer and reads per-peer octets 26-29 raw: 65001 must be 00 00 FD E9 (the 16 most significant bits zero) and 4200000001 must be FA 56 EA 01, so a 2-octet field, a lost padding or a misplaced AS goes red. {single-polarity: positive} holds: the field is a fixed 4-octet encode with no shorter variant to refuse.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestBMPPeerHeaderDecode |
unit/verify | unproven |
| positive | TestBMPPeerHeaderEncode |
unit/verify | unproven |
| positive | TestRFC7854PeerASIsFourOctetsWithTheShortASZeroPadded |
unit/verify | revert, verified |
RFC7854-x-5
It is 4 bytes long if an IPv4 address is carried in this field (with the 12 most significant bytes zero-filled) and 16 bytes long if an IPv6 address is carried in this field. (§4.2, Per-Peer Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. IPv4 lands in octets 12..15 with 0..11 zero; the IPv6 negative keeps its full address
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestParseIPIntoIPv6 |
unit/verify | unproven |
| positive | TestParseIPIntoIPv4 |
unit/verify | unproven |
RFC7854-x-6
An initiation message MUST be sent as the first message after the TCP session comes up. (§4.3, Initiation Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. collector reads the first message off a live TCP connection and asserts type Initiation; single-polarity marker
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestBMPSenderConnects |
unit/verify | unproven |
RFC7854-x-7
The sysDescr and sysName Information TLVs MUST be sent, any others are optional. (§4.3, Initiation Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. live Initiation carries sysName equal to the system identity and a sysDescr; single-polarity marker
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestBMPSenderInitiation |
unit/verify | unproven |
RFC7854-x-8
Sent OPEN Message: The full OPEN message transmitted by the monitored router to its peer. o Received OPEN Message: The full OPEN message received by the monitored router from its peer. (§4.10, Peer Up Notification)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-13 after the RFC 7854 Section 3.3 guard (no Peer Down for a peer never reported up). Positives unchanged: TestHandleSenderStatePeerUp and TestBMPSenderPeerUp echo both cached OPENs byte for byte. Negative TestPeerUpOnCacheMissNeverReachesTheCollector: up event with no OPEN cached, down event, then a Route Monitoring sentinel on the same FIFO queue; the first message read must be the sentinel, and a Peer Up is a named failure. Owner-approved marker change (sentinel replaces the Peer Down, which Section 3.3 no longer owes). Reviewer observed red with the guard removed (first message became the Peer Down), so the test still sees the whole queue head; a Peer Up emitted without both OPENs would be read first and fail.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestPeerUpOnCacheMissNeverReachesTheCollector |
unit/verify | unproven |
| positive | TestHandleSenderStatePeerUp |
unit/verify | unproven |
| positive | TestBMPSenderPeerUp |
unit/verify | unproven |
RFC7854-x-9
Following the common BMP header and per-peer header is a BGP Update PDU. (§4.6, Route Monitoring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Route Monitoring wraps the body in a full RFC 4271 header of type UPDATE; single-polarity marker
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestBMPSenderRouteMonitoring |
unit/verify | unproven |
RFC7854-x-10
Reason indicates why the session was closed. (§4.9, Peer Down Notification)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-18 (independent auditor, after 4ef90497c6). Section 4.9: "Reason indicates why the session was closed." The earlier finding (no unit tied a Reason to the cause, and peerDownFor never emitted reason 4) is fixed and now proven at both decision points. Reactor: TestPeerCloseNamesTheTransportLoss drops TCP under a running Peer and asserts rpc.ReasonTCPFailure with Event 18; TestPeerCloseNamesTheCongestionTeardownLocal drives congestionTeardownPeer and asserts rpc.ReasonLocalClose with Event 18, so ze closing the transport itself is not reported as the remote doing it. BMP: TestRFC7854PeerDownTransportLossIsReason4 asserts Reason 4 ("This includes any unexpected termination of the transport session") with no Data for rpc.ReasonTCPFailure. TestHandleSenderStatePeerDown (reason 2 for a NOTIFICATION close with no cached PDU) and TestBMPSenderPeerDown (round-trips a chosen byte) remain weak on their own. Seam not covered by a tagged unit: apiStateObserver.OnPeerClosed and server/events.go copying the reason and CloseFSMEvent into the StructuredEvent. Single-polarity annotation holds: every Peer Down is written with a reason byte.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestHandleSenderStatePeerDown |
unit/verify | unproven |
| positive | TestRFC7854PeerDownTransportLossIsReason4 |
unit/verify | revert, verified |
| positive | TestBMPSenderPeerDown |
unit/verify | unproven |
| positive | TestPeerCloseNamesTheCongestionTeardownLocal |
unit/verify | revert, verified |
| positive | TestPeerCloseNamesTheTransportLoss |
unit/verify | revert, verified |
RFC7854-x-11
The router MAY send a Termination message prior to closing the session. (§3.3, Lifecycle of a BMP Session)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29: the stale unit TestSenderStopSendsTerminationToCollector changed only by an added RFC7854-4.5-5 tag comment; body unchanged. It still requires the collector to read a Termination through stop() racing holdConnection, and the writeTerminationLocked break recorded under RFC7854-4.5-5 on this same unit was observed red. sender_test.go::TestBMPSenderTermination covers the encoder, no record. {single-polarity: positive} holds for a MAY that ze always exercises.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestSenderStopSendsTerminationToCollector |
unit/verify | unproven |
| positive | TestBMPSenderTermination |
unit/verify | unproven |
RFC7854-x-12
No BMP message is ever sent from the monitoring station to the monitored router. (§3.2, Connection Establishment and Termination)
Audit verdict: enforced (the tests do what the requirement demands), fresh. receiver loop driven with Initiation and Termination writes zero bytes toward the router end; single-polarity marker
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestBMPReceiverUnidirectional |
unit/verify | unproven |
RFC7854-4.9-1
Reason 1: The local system closed the session. Following the Reason is a BGP PDU containing a BGP NOTIFICATION message that would have been sent to the peer. o Reason 2: The local system closed the session. No notification message was sent. Following the reason code is a 2-byte field containing the code corresponding to the Finite State Machine (FSM) Event that caused the system to close the session (see Section 8.1 of [RFC4271]). Two bytes both set to 0 are used to indicate that no relevant Event code is defined. o Reason 3: The remote system closed the session with a notification message. Following the Reason is a BGP PDU containing the BGP NOTIFICATION message as received from the peer. (§4.9, Peer Down Notification)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-18 (independent auditor, after ecba2d9147). Section 4.9: "Reason 2: The local system closed the session. No notification message was sent. Following the reason code is a 2-byte field containing the code corresponding to the Finite State Machine (FSM) Event that caused the system to close the session", and the figure gives "Data (present if Reason = 1, 2 or 3)". The two data units now feed the close reasons the reactor sends: TestRFC7854PeerDownCarriesTheDataItsReasonRequires feeds rpc.ReasonNotification with a sent and a received NOTIFICATION and asserts reasons 1 and 3 with Data equal to the exact NOTIFICATION PDU, and rpc.ReasonLocalClose on FSMEvent 18 and asserts reason 2 with Data 0012, red if peerDownFor (bmp_events.go) writes constant zero octets or drops the event. TestRFC7854PeerDownOmitsDataWhereTheReasonHasNone asserts reason 5 for rpc.ReasonPeerRemoved and reason 4 for rpc.ReasonTCPFailure on event 18, each with no Data, so an encoder that always appends the event code goes red; its tag claim names reason 5 only and the body proves more. TestRFC7854PeerDownLocalCloseCarriesTheFSMEvent is unchanged. Residual seam as before: which event closed the session is the reactor's answer (sessionCloseFor), and the copy of CloseFSMEvent into StructuredEvent.FSMEvent (server/events.go) has no unit; these units set FSMEvent directly.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854PeerDownOmitsDataWhereTheReasonHasNone |
unit/verify | revert, verified |
| positive | TestRFC7854PeerDownLocalCloseCarriesTheFSMEvent |
unit/verify | revert, verified |
| positive | TestRFC7854PeerDownCarriesTheDataItsReasonRequires |
unit/verify | revert, verified |
RFC7854-4.5-2
Likewise, the monitoring station MUST close the TCP session after receiving a termination message. (§4.5, Termination Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. receiver closes after reading a Termination with the router end held open (well under the read deadline) and drops the router; without a Termination two valid messages leave the session open
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestBMPReceiverKeepsSessionWithoutTermination |
unit/verify | unproven |
| positive | TestBMPReceiverClosesAfterTermination |
unit/verify | unproven |
RFC7854-x-15
It MAY periodically send Stats Reports or even new Initiation messages, according to configuration. (§3.3, Lifecycle of a BMP Session)
Audit verdict: enforced (the tests do what the requirement demands), fresh. statistics-timeout 1 through the reload rail yields two reports about one interval apart; statistics-timeout 0 yields none
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854StatisticsTimeoutZeroSendsNoReport |
unit/verify | revert, verified |
| positive | TestRFC7854StatisticsTimeoutSendsPeriodicReports |
unit/verify | revert, verified |
RFC7854-x-16
It subsequently sends a Peer Up message over the BMP session for each of its monitored BGP peers that is in the Established state. (§3.3, Lifecycle of a BMP Session)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. The wrong tags on TestConcurrentDumpsStayAddressedToTheirOwnCollector are gone. rfc7854_session_opening_test.go::TestRFC7854SessionPeerUpOnlyForEstablishedPeers primes a new collector (primeSender) over one Established peer and one peer that exchanged OPENs and sent an UPDATE but never reported Up; it counts Peer Ups per address on the collector's bytes: exactly 1 for the Established peer, 0 for the other, and the first message is the Peer Up. A producer that announced every peer with cached OPENs, or none, goes red.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854SessionPeerUpOnlyForEstablishedPeers |
unit/verify | revert, verified |
| positive | TestRFC7854SessionPeerUpOnlyForEstablishedPeers |
unit/verify | revert, verified |
RFC7854-x-17
It subsequently sends a Peer Up message over the BMP session for each of its monitored BGP peers that is in the Established state. It follows by sending the contents of its Adj- RIBs-In (pre-policy, post-policy, or both, see Section 5) encapsulated in Route Monitoring messages. (§3.3, Lifecycle of a BMP Session)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. rfc7854_session_opening_test.go::TestRFC7854SessionDumpsAdjRIBInAfterThePeerUp reads the same two-peer session in order: no Route Monitoring before the Peer Up, the Established peer's received route (exact UPDATE body announceBody(1)) arrives as a pre-policy Route Monitoring (L clear, the default pre-policy selection), and nothing is dumped for the peer that never reached Established. Order, content and scope of the Adj-RIB-In dump are each asserted.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854SessionDumpsAdjRIBInAfterThePeerUp |
unit/verify | revert, verified |
| positive | TestRFC7854SessionDumpsAdjRIBInAfterThePeerUp |
unit/verify | revert, verified |
RFC7854-x-18
The sysDescr and sysName Information TLVs MUST be sent, any others are optional. (§4.3, Initiation Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29. Both clauses now hold both polarities. Sender: rfc7854_test.go TestRFC7854InitiationCarriesSysDescr and the new rfc7854_session_opening_test.go::TestRFC7854InitiationCarriesSysName decode the Initiation sendInitiation writes and require exactly one sysName (type 2) and a sysDescr (type 1). Receiver: TestRFC7854InitiationMissingSysDescrEndsSession and TestBMPInitiationMissingSysNameEndsSession (tag added) each send an Initiation missing one TLV and require the session closed (decodeInitiation checks each independently); TestRFC7854InitiationEmptyIdentityValuesAccepted keeps presence, not length, as the test.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestBMPInitiationMissingSysNameEndsSession |
unit/verify | revert, verified |
| negative | TestRFC7854InitiationMissingSysDescrEndsSession |
unit/verify | unproven |
| positive | TestRFC7854InitiationEmptyIdentityValuesAccepted |
unit/verify | unproven |
| positive | TestRFC7854InitiationCarriesSysName |
unit/verify | revert, verified |
| positive | TestRFC7854InitiationCarriesSysDescr |
unit/verify | revert, verified |
RFC7854-3.2-1
Retries MUST be subject to some variety of backoff. (§3.2, Connection Establishment and Termination)
Audit verdict: enforced (the tests do what the requirement demands), fresh. nextReconnectWait doubles and caps at reconnectMax; a refused dial is not retried before the base wait even when the port reopens early
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854RetryNotBeforeBackoff |
unit/verify | revert, verified |
| positive | TestRFC7854RetryBackoffDoubles |
unit/verify | revert, verified |
RFC7854-3.2-2
The router MUST also restrict the rate at which sessions may be established. (§3.2, Connection Establishment and Termination)
Audit verdict: enforced (the tests do what the requirement demands), fresh. after the collector closes a session the sender reconnects, and not before the base wait since the first session
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854SessionEstablishmentRateLimited |
unit/verify | revert, verified |
| positive | TestRFC7854SessionEstablishmentRateLimited |
unit/verify | revert, verified |
RFC7854-3.3-1
Once it has sent all the routes for a given peer, it MUST send an End-of-RIB message for that peer (§3.3, Lifecycle of a BMP Session, and restated in the Route Monitoring section)
Audit verdict: enforced (the tests do what the requirement demands), fresh. after reconnect Peer Up precedes the surviving route and each family gets EOR after its routes; an incremental UPDATE and another collector's reconnect produce no EOR, and an incomplete snapshot never emits EOR
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854AdjReplayCompletionIsSessionScoped |
unit/verify | unproven |
| negative | TestRFC7854IncompleteAdjReplayCannotClaimCompletion |
unit/verify | unproven |
| positive | TestRFC7854AdjReplayEndsEachFamily |
unit/verify | unproven |
RFC7854-4.1-1
A BMP implementation MUST ignore unrecognized message types upon receipt. (§4.1, Common Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. type 200 is skipped and the following Termination is consumed; a malformed Peer Up still ends the session
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854MalformedKnownTypeStillEndsSession |
unit/verify | revert, verified |
| positive | TestRFC7854UnrecognizedMessageTypeIgnored |
unit/verify | revert, verified |
RFC7854-4.2-1
The remaining bits are reserved for future use. They MUST be transmitted as 0 and their values MUST be ignored on receipt. (§4.2, Per-Peer Header)
Audit verdict: enforced (the tests do what the requirement demands), fresh. transmitted Route Monitoring on both directions has reserved bits 0; a Peer Up with every reserved bit set is accepted and its defined flags decode unchanged
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854ReservedFlagsIgnoredOnReceipt |
unit/verify | revert, verified |
| positive | TestRFC7854ReservedFlagsTransmittedAsZero |
unit/verify | revert, verified |
RFC7854-4.3-2
The initiation message consists of the common BMP header followed by two or more Information TLVs (Section 4.4) containing information about the monitored router. (§4.3, Initiation Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29. Positive rfc7854_message_layout_test.go::TestRFC7854InitiationIsTheCommonHeaderThenTwoOrMoreTLVs reads the octets sender.go::sendInitiation writes off a pipe, checks type 4 and walks TLVs by hand from octet 6 to exactly the end, requiring >= 2. Negative (R1(a)) ::TestRFC7854InitiationWithFewerThanTwoTLVsIsRefused: a one-TLV Initiation is refused by the receiver. The refusal comes from decodeInitiation's sysName-presence check (RFC7854-x-18), not a count check, but every one-TLV Initiation lacks sysName or sysDescr, so no one-TLV input is accepted; the buffer is otherwise valid.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854InitiationWithFewerThanTwoTLVsIsRefused |
unit/verify | revert, verified |
| positive | TestRFC7854InitiationIsTheCommonHeaderThenTwoOrMoreTLVs |
unit/verify | revert, verified |
RFC7854-4.4-1
If multiple strings are included, their ordering MUST be preserved when they are reported. (§4.4, Information TLV)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Initiation and Peer Up strings reach the command output in transmitted order, with duplicates kept
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854InitiationStringsKeepDuplicates |
unit/verify | unproven |
| negative | TestRFC7854PeerUpStringsKeepDuplicates |
unit/verify | unproven |
| positive | TestRFC7854InitiationStringsReportedInOrder |
unit/verify | unproven |
| positive | TestRFC7854PeerUpStringsReportedInOrder |
unit/verify | unproven |
RFC7854-4.4-2
Type = 1: sysDescr. The Information field contains an ASCII string whose value MUST be set to be equal to the value of the sysDescr MIB-II [RFC1213] object. (§4.4, Information TLV)
Audit verdict: enforced (the tests do what the requirement demands), fresh. sysDescr carries the running build and uname sysname, release and machine, the MIB-II sysDescr content; it changes when the build identity changes
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854InitiationDescriptionChangesWithBuild |
unit/verify | unproven |
| positive | TestRFC7854InitiationDescribesRunningSystem |
unit/verify | unproven |
RFC7854-4.4-3
Type = 2: sysName. The Information field contains an ASCII string whose value MUST be set to be equal to the value of the sysName MIB-II [RFC1213] object. (§4.4, Information TLV)
Audit verdict: enforced (the tests do what the requirement demands), fresh. sysName is the configured host.domain FQDN, the MIB-II sysName convention, survives rollback, and follows a configuration change
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854InitiationSystemNameChanges |
unit/verify | unproven |
| positive | TestRFC7854InitiationUsesConfiguredSystemName |
unit/verify | unproven |
RFC7854-4.5-1
Once the router has sent a termination message, it MUST close the TCP session without sending any further messages. (§4.5, Termination Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. after stop() the collector reads the Termination then EOF; a Peer Up afterwards is refused with errNotConnected
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854TerminationThenCloseAndSilence |
unit/verify | revert, verified |
| positive | TestRFC7854TerminationThenCloseAndSilence |
unit/verify | revert, verified |
RFC7854-4.5-3
Type = 1: Reason. The Information field contains a 2-byte code indicating the reason that the connection was terminated. Some reasons may have further TLVs associated with them. Inclusion of this TLV is REQUIRED. (§4.5, Termination Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. live shutdown Termination carries exactly one two-octet Reason; absent, empty, short and long Reason TLVs fail decode and end the session
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854TerminationRequiresTwoByteReason |
unit/verify | unproven |
| positive | TestRFC7854SenderTerminationCarriesReason |
unit/verify | unproven |
RFC7854-4.5-4
The termination message consists of the common BMP header followed by one or more TLVs containing information about the reason for the termination (§4.5, Termination Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29. Positive rfc7854_message_layout_test.go::TestRFC7854TerminationIsTheCommonHeaderThenTLVs reads the octets the sender's Termination path writes, walks TLVs from octet 6 to exactly the end, requires at least one and exactly one Reason TLV. Negative ::TestRFC7854TerminationWithNoTLVIsRefused: a 6-octet header-only Termination is refused (decodeTermination's missing-Reason branch, which any zero-TLV body reaches).
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854TerminationWithNoTLVIsRefused |
unit/verify | revert, verified |
| positive | TestRFC7854TerminationIsTheCommonHeaderThenTLVs |
unit/verify | revert, verified |
RFC7854-4.5-5
Although use of this message is RECOMMENDED, a monitoring station must always be prepared for the session to terminate with no message. (§4.5, Termination Message)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Station clause: termination_absent_test.go::TestBMPReceiverEndsTheSessionWhenTheRouterLeavesWithoutTermination sends Initiation + Peer Up, confirms one router and one peer held, closes the pipe with no Termination, and requires handleSession to return with zero routers and zero peers (record: removeRouter break observed red). RECOMMENDED clause: sender_queue_test.go::TestSenderStopSendsTerminationToCollector reads a Termination on the collector side through stop() racing holdConnection (record: writeTerminationLocked break observed red). {single-polarity: positive} holds: the sentence permits the no-message close, so no non-compliant router input exists for the station to refuse.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestSenderStopSendsTerminationToCollector |
unit/verify | revert, verified |
| positive | TestBMPReceiverEndsTheSessionWhenTheRouterLeavesWithoutTermination |
unit/verify | revert, verified |
RFC7854-4.7-1
If the BGP Message TLV occurs in the Route Mirroring message, it MUST occur last in the list of TLVs. (§4.7, Route Mirroring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. transmitted Route Mirroring ends with the BGP Message TLV; Information then BGP Message is accepted, BGP Message then Information ends the session
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854MirrorBGPMessageNotLastEndsSession |
unit/verify | unproven |
| positive | TestRFC7854ErroredMirrorWithPDUAccepted |
unit/verify | unproven |
| positive | TestRFC7854RouteMirroringBGPMessageTLVLast |
unit/verify | revert, verified |
RFC7854-4.7-2
Code = 0: Errored PDU. The contained message was found to have some error that made it unusable, causing it to be treated-as- withdraw [RFC7606]. A BGP Message TLV MUST also occur in the TLV list. (§4.7, Route Mirroring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Errored PDU with a BGP Message TLV is accepted; Errored PDU without one ends the session
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854ErroredMirrorWithoutPDUEndsSession |
unit/verify | unproven |
| positive | TestRFC7854ErroredMirrorWithPDUAccepted |
unit/verify | unproven |
RFC7854-4.7-3
Following the common BMP header and per-peer header is a set of TLVs that contain information about a message or set of messages. (§4.7, Route Mirroring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29. Positive rfc7854_message_layout_test.go::TestRFC7854RouteMirroringIsThePerPeerHeaderThenTLVs: writeRouteMirroring output decodes a per-peer header equal to the input at octet 6, then TLVs walked by hand from octet 48 to exactly the end, same types and values in order. Negative ::TestRFC7854RouteMirroringWhoseBodyIsNotTLVsIsRefused: the valid message is first accepted, then a 3-octet tail that is no TLV (length fixed up) is refused, so only the not-TLVs body differs.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854RouteMirroringWhoseBodyIsNotTLVsIsRefused |
unit/verify | revert, verified |
| positive | TestRFC7854RouteMirroringIsThePerPeerHeaderThenTLVs |
unit/verify | revert, verified |
RFC7854-4.8-1
A BMP implementation MUST ignore unrecognized stat types on receipt, and likewise MUST ignore unexpected data in the Stat Data field. (§4.8, Stats Reports)
Audit verdict: enforced (the tests do what the requirement demands), fresh. unknown stat type 60000 and a 3-octet counter are consumed and the session survives; a stat length past the report end still ends it
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854TruncatedStatEndsSession |
unit/verify | revert, verified |
| positive | TestRFC7854UnrecognizedStatTypeIgnored |
unit/verify | revert, verified |
RFC7854-4.8-2
However, if an SR message is transmitted, at least one statistic MUST be carried in it. (§4.8, Stats Reports)
Audit verdict: enforced (the tests do what the requirement demands), fresh. a transmitted report carries one statistic; an empty report is refused before it reaches the collector
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854SenderRefusesEmptyStatistics |
unit/verify | unproven |
| positive | TestRFC7854StatsReportCarriesAStatistic |
unit/verify | revert, verified |
RFC7854-4.8-3
Following the common BMP header and per-peer header is a 4-byte field that indicates the number of counters in the stats message where each counter is encoded as a TLV. (§4.8, Stats Reports)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29. Positive rfc7854_message_layout_test.go::TestRFC7854StatsReportCountNamesTheCountersThatFollow: the 4-octet count at octet 48 equals 3 and exactly three counter TLVs, walked by hand, run to the end with the input types and values. Negative ::TestRFC7854StatsReportCountDisagreeingWithItsCountersIsRefused: the valid report is first accepted, then count+1 (truncated entry) and count-1 (trailing data) are each refused by decodeStatisticsReport.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854StatsReportCountDisagreeingWithItsCountersIsRefused |
unit/verify | revert, verified |
| positive | TestRFC7854StatsReportCountNamesTheCountersThatFollow |
unit/verify | revert, verified |
RFC7854-4.10-1
Following the common BMP header and per-peer header is the following (§4.10, Peer Up Notification)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29. The row's sentence is the lead-in to the §4.10 figure, the only statement of the Peer Up layout, so the obligation judged is that figure: Local Address (16), Local Port, Remote Port, Sent OPEN, Received OPEN after the per-peer header (Information TLVs are RFC7854-x-19, the OPEN contents RFC7854-x-8). Positive rfc7854_message_layout_test.go::TestRFC7854PeerUpIsThePerPeerHeaderThenTheFixedFieldsAndBothOPENs reads each field raw at its offset from writePeerUp output and the exact total length. Negative ::TestRFC7854PeerUpShorterThanItsFixedFieldsIsRefused: a valid Peer Up is accepted, the same cut 10 octets into the fixed fields is refused (decodePeerUp short check).
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854PeerUpShorterThanItsFixedFieldsIsRefused |
unit/verify | revert, verified |
| positive | TestRFC7854PeerUpIsThePerPeerHeaderThenTheFixedFieldsAndBothOPENs |
unit/verify | revert, verified |
RFC7854-5-1
Pre-policy routes MUST have their L flag clear in the BMP header (see Section 4), post-policy routes MUST have their L flag set. (§5, Route Monitoring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29 (the negative unit gained the RFC7854-5-4 tag line only; assertions unchanged). rfc7854_test.go::TestRFC7854LFlagFollowsPolicy: received announce and withdraw leave with L clear, sent with L set. ::TestRFC7854LFlagNotDecidedByBody: one body streamed on both sides leaves L clear received and L set sent, so the flag follows the direction (policy stage) and not the message. Ze sends no post-policy Adj-RIB-In; its L-set stream is the RFC 8671 Adj-RIB-Out (O and L set, peerHeaderFromEvent).
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854LFlagNotDecidedByBody |
unit/verify | revert, verified |
| positive | TestRFC7854LFlagFollowsPolicy |
unit/verify | revert, verified |
RFC7854-5-2
If the implementation is able to provide information about when routes were received, it MAY provide such information in the BMP Timestamp field. Otherwise, the BMP Timestamp field MUST be set to 0, indicating that time is not available. (§5, Route Monitoring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. replayed routes and EORs with unknown receipt time carry 0.0; a known receipt time survives replay exactly
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854KnownRouteTimeSurvivesReplay |
unit/verify | unproven |
| positive | TestRFC7854UnknownRouteTimeIsZero |
unit/verify | unproven |
RFC7854-5-4
The withdraw MUST have its L flag set to correspond to that of any previous announcement (§5, Route Monitoring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. First verdict 2026-09-29 (first clause of the §5 sentence; the twice-sent-withdraw clause left with retired RFC7854-5-3). Producer peerHeaderFromEvent sets L only on the sent direction, so a route's announcement and its withdraw take their L from the same direction. Positive rfc7854_test.go::TestRFC7854LFlagFollowsPolicy: a received withdraw carries L clear like a received announce, a sent withdraw L set like a sent announce. Negative ::TestRFC7854LFlagNotDecidedByBody: the same withdraw body on both sides gets L clear and L set, so a withdraw cannot carry the other side's flag. Both observed red under the peerHeaderFromEvent break. The test does not pair one announce with its own withdraw by prefix; the direction is the only input L reads, so no pairing can diverge.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854LFlagNotDecidedByBody |
unit/verify | revert, verified |
| positive | TestRFC7854LFlagFollowsPolicy |
unit/verify | revert, verified |
RFC7854-5-6
When a change occurs to a route, such as an attribute change, the router must update the monitoring station with the new attribute. (§5, Route Monitoring)
Audit verdict: enforced (the tests do what the requirement demands), fresh. rfc7854_replay_test.go::TestRFC7854ChangedAttributesCanReturnToEarlierValue receives one prefix three times with ORIGIN IGP, INCOMPLETE, IGP and requires exactly three Route Monitoring messages, each body byte-equal to the UPDATE carrying that ORIGIN, so a sender that suppresses or dedupes the return to an earlier value fails (record: handleSenderUpdate break observed red). One attribute (ORIGIN) samples 'such as an attribute change'. {single-polarity: positive} holds: every route change is compliant input to the router, which has no refusal path.
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| positive | TestRFC7854ChangedAttributesCanReturnToEarlierValue |
unit/verify | revert, verified |
RFC7854-8.2-1
Since in this case no transport session actually exists, the Local and Remote Port fields of the Peer Up message MUST be set to 0. (§8.2, Peer Up Notification)
Audit verdict: enforced (the tests do what the requirement demands), fresh. Loc-RIB instance Peer Up carries ports 0/0; a BGP peer's Peer Up carries its real 179/40000
| Polarity | Test | Kind and tier | Proof state |
|---|---|---|---|
| negative | TestRFC7854BGPPeerUpCarriesTransportPorts |
unit/verify | revert, verified |
| positive | TestRFC7854LocRIBPeerUpPortsZero |
unit/verify | revert, verified |
Extraction sign-off
| Field | Value |
|---|---|
| Reviewer | claude |
| Signed off | 2026-09-29 |
| Register | prose |
| Source | rfc/full/rfc7854.txt |
| Source fingerprint | b32c6bf7d6b5d67a |
| Record | rfc/extraction/rfc7854.json |
| Mapped sentences | 24 |
| Declined as scope | 15 |
| Relocated to a spec, which Ze OWES | 0 |
| Unclassified | 0 |
Sections
| Section | Name | Sites | Disposition | Reason |
|---|---|---|---|---|
front |
not stated | 1 | walked | not stated |
1 |
not stated | 0 | walked | not stated |
1.1 |
not stated | 0 | walked | not stated |
2 |
not stated | 0 | walked | not stated |
3 |
not stated | 0 | walked | not stated |
3.1 |
not stated | 0 | walked | not stated |
3.2 |
not stated | 2 | walked | not stated |
3.3 |
not stated | 2 | walked | not stated |
4 |
not stated | 0 | walked | not stated |
4.1 |
not stated | 2 | walked | not stated |
4.2 |
not stated | 1 | walked | not stated |
4.3 |
not stated | 2 | walked | not stated |
4.4 |
not stated | 3 | walked | not stated |
4.5 |
not stated | 4 | walked | not stated |
4.6 |
not stated | 0 | walked | not stated |
4.7 |
not stated | 2 | walked | not stated |
4.8 |
not stated | 3 | walked | not stated |
4.9 |
not stated | 0 | walked | not stated |
4.10 |
not stated | 0 | walked | not stated |
5 |
not stated | 6 | walked | not stated |
6 |
not stated | 0 | walked | not stated |
7 |
not stated | 0 | walked | not stated |
8 |
not stated | 0 | walked | not stated |
8.1 |
not stated | 0 | walked | not stated |
8.2 |
not stated | 2 | walked | not stated |
9 |
not stated | 0 | walked | not stated |
10 |
not stated | 0 | walked | not stated |
10.1 |
not stated | 1 | walked | not stated |
10.2 |
not stated | 1 | walked | not stated |
10.3 |
not stated | 0 | walked | not stated |
10.4 |
not stated | 1 | walked | not stated |
10.5 |
not stated | 1 | walked | not stated |
10.6 |
not stated | 1 | walked | not stated |
10.7 |
not stated | 1 | walked | not stated |
10.8 |
not stated | 1 | walked | not stated |
10.9 |
not stated | 1 | walked | not stated |
10.10 |
not stated | 1 | walked | not stated |
11 |
not stated | 0 | walked | not stated |
12 |
not stated | 0 | walked | not stated |
12.1 |
not stated | 0 | walked | not stated |
12.2 |
not stated | 0 | walked | not stated |
Excluded sentences
| Site | Excluded kind | Reason | Quote |
|---|---|---|---|
front:1 |
not-a-requirementnever bound Ze the sentence states a fact or describes another document, and directs no implementation |
Front-matter boilerplate the extractor did not strip: the IETF Trust Legal Provisions notice binds whoever extracts Code Components from the RFC document, not a BMP router or monitoring station. The lowercase must is the license condition of the copyright notice. | Code Components extracted from this document must include Simplified BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Simplified BSD License. |
3.3:1 |
duplicate-ofnever bound Ze the same obligation is already captured under another requirement id |
Restates the obligation section 4.3 states at the site this walk maps to RFC7854-x-6: 'An initiation message MUST be sent as the first message after the TCP session comes up.' Section 3.3 states it as the first step of the session lifecycle; section 4.3 states it as the rule of the message itself. | It MUST begin by sending an Initiation message. |
4.8:2 |
cross-documentnever bound Ze the obligation belongs to another document that this one only cites |
The sentence is the 64-bit Gauge definition that section 4.8 adopts from Section 4 of RFC 2856 (the section says the stats types are defined after the examples in Section 3.2.3.3 of RFC 1155 and Section 4 of RFC 2856). The lowercase shall describes the semantics of that data type as RFC 2856 defines it; section 4.8 states its own obligations on stats reports at the sites this walk maps to RFC7854-4.8-1 and RFC7854-4.8-2. | 64-bit Gauge: A non-negative integer that may increase or decrease, but shall never exceed a maximum value, nor fall below a minimum one. |
5:1 |
duplicate-ofnever bound Ze the same obligation is already captured under another requirement id |
Restates the per-peer End-of-RIB obligation section 3.3 states at the site this walk maps to RFC7854-3.3-1: 'Once it has sent all the routes for a given peer, it MUST send an End-of-RIB message for that peer'. Section 5 adds only where the marker is defined (Section 2 of RFC 4724) and that it carries the BMP encapsulation header. | When the initial dump is completed for a given peer, this MUST be indicated by sending an End-of-RIB marker for that peer (as specified in Section 2 of [RFC4724], plus the BMP encapsulation header). |
5:6 |
not-a-requirementnever bound Ze the sentence states a fact or describes another document, and directs no implementation |
The prose scanner matched the ordinary English required in (Route mirroring (Section 6) is provided if this is required.), which describes when an operator uses Route Mirroring, and the lowercase should attempt to generate updates promptly, which the same paragraph relaxes: it is acceptable that the router generate the final state of that prefix. Neither states an obligation on the router; RFC 7854 invokes RFC 2119 for the capitalized keywords only. | (Route mirroring (Section 6) is provided if this is required.) While the router should attempt to generate updates promptly, there is a finite time that could elapse between reception of an update, the generation an RM message, and its transmission to the monitoring station. |
8.2:1 |
not-a-requirementnever bound Ze the sentence states a fact or describes another document, and directs no implementation |
The prose scanner matched the ordinary English Some consideration is required, which introduces section 8.2 and states no obligation. The section obligation on locally originated routes is the next site, mapped to RFC7854-8.2-1. | Some consideration is required for routes originated into BGP by the local router, whether as a result of redistribution from another protocol or for some other reason. |
10.1:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Type values 0 through 127 MUST be assigned using the "Standards Action" policy, and values 128 through 250 using the "Specification Required" policy defined in [RFC5226]. |
10.2:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Peer Type values 0 through 127 MUST be assigned using the "Standards Action" policy, and values 128 through 250 using the "Specification Required" policy, defined in [RFC5226]. |
10.4:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Stat Type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.5:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.6:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.7:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.8:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.9:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
10.10:1 |
binds-another-rolenever bound Ze the obligation is addressed to a role Ze never acts as Presumed wrong until justified: Ze rarely implements one side of a protocol, so the reason beside this row must name the role, show Ze never acts as it, and cite the producer that would. |
Binds IANA, the registry the section addresses: the sentence sets the allocation policy ('Standards Action', 'Specification Required' under RFC 5226) IANA applies when it assigns a value from this registry. Ze holds no code that acts as IANA and could hold none: the role is the registry itself, not a party on the BMP wire. Ze's BMP encoder and decoder (internal/component/bgp/plugins/bmp) read and write the values the registry already holds; nothing in the repository allocates one. | Information type values 0 through 32767 MUST be assigned using the "Standards Action" policy, and values 32768 through 65530 using the "Specification Required" policy, defined in [RFC5226]. |
Superseded
No document obsoletes RFC 7854, so its obligations are stated where they were written.