In a recent paper, we show how to formally verify P4 code using the interactive theorem prover (ITP) HOL4. The method creates an end-to-end proof entirely inside the logic of the ITP, and is applicable to real P4 programs by using the import tool of HOL4P4. To gain efficiency when symbolically executing large programs, multiple types of semantics are used, with proofs of soundness with respect to the standard semantics enabling the composition of their results.
This tool can be used by SEMLA in the future to formally verify that P4 code generated by LLMs respects certain program specifications.
Authors: Didrik Lundberg, Roberto Guanciale, Mads Dam.