# \[ANN\] New package: P4-SpecTec

**URL:** https://discuss.ocaml.org/t/ann-new-package-p4-spectec/18434
**Category:** Community
**Tags:** announce
**Created:** [August 10, 2026, 1:11am UTC](https://discuss.ocaml.org/t/ann-new-package-p4-spectec/18434 "2026-08-10T01:11:59Z")
**Posts on this page:** 1
**Showing post:** 1

<div class="post-metadata">

### Author: ![pacokwon](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/pacokwon/32/6634_2.png) [@pacokwon](https://discuss.ocaml.org/u/pacokwon)
#### Post date: [August 10, 2026, 1:12am UTC](https://discuss.ocaml.org/t/ann-new-package-p4-spectec/18434/1 "2026-08-10T01:12:00Z")

</div>

Hi!

We are happy to announce the first public release of `p4spectec`, a framework for mechanizing the P4 language specification. It provides a domain-specific language for writing formal specifications in the form of _algorithmic inference rules_ [(Lee et al., 2026)](https://arxiv.org/abs/2608.00639).

A specification written in P4-SpecTec is **executable**. By writing typing rules with P4-SpecTec, you get a reference type checker. By writing dynamic semantics rules, you get a reference interpreter. The _prose backend_ also generates human-readable documentation from the mechanized specification.

> **[opam - p4spectec](https://opam.ocaml.org/packages/p4spectec/)**
>
> The homepage of opam, a package manager for OCaml

For detailed instructions, source code and the mechanized P4 specification, check out the GitHub repository linked to the package.

---

_[View the full topic](https://discuss.ocaml.org/t/ann-new-package-p4-spectec/18434)._