P4-Based Automated Reasoning - Steffen Smolka, Google#

Steffen Smolka, Staff Software Engineer, Google (leads the P4-Based Automated Reasoning group)

• Why: Using P4 not to program the pipeline but as a vendor-agnostic, machine-readable specification that switches are automatically validated against is a genuinely different use of P4 — it addresses switch qualification and multi-vendor SDN interoperability, two chronic pains for anyone operating heterogeneous fabrics.
• What: Google's practice of writing P4 specs for switch pipelines (programmable or not) and building tools that (1) run high-coverage automated validation of switch behavior against the spec, and (2) let the SDN controller hold switches from different vendors accountable to the same unambiguous spec, with reported gains in reliability and development velocity. (from abstract only)
• How: The P4 program becomes the contract; automated reasoning tools check conformance of actual switch forwarding behavior, and the controller's interaction with each vendor's silicon is mediated by the shared machine-readable spec.
• Where applicable: Any multi-vendor switch fleet with an SDN controller — hyperscaler-flavored, but the spec-as-contract technique is broadly adoptable and independent of particular silicon. Attested as running at Google, but the talk abstract does not quantify coverage or results.