Coq BPF interpreter

This is a BPF interpreter written in the Coq proof assistant. It also has tactic machinery to construct proven-equivalent Gallina programs for BPF programs.

This is not an official Google product.