# Joelreymont Pz Pz

> Sync Proofs

- Skill: `tomevault-io/joelreymont-pz-pz` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/joelreymont-pz-pz`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/joelreymont-pz-pz/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/joelreymont-pz-pz

---


# Sync Proofs

Verify Lean/TLA+ proofs match current Zig code, rebuild if stale.

## Steps

1. Run sync check: `cd $(git rev-parse --show-toplevel) && bash proofs/sync_check.sh`
2. If stale: identify which proofs need updating from the output
3. Update stale Lean files in `proofs/lean/PzProofs/`
4. Rebuild: `cd proofs/lean && ~/.elan/bin/lake build`
5. Re-run TLA+ if specs changed: `cd proofs/tla && /opt/homebrew/opt/openjdk/bin/java -XX:+UseParallelGC -cp ~/tools/tla2tools.jar tlc2.TLC <spec>.tla -config <spec>.cfg -workers auto`

## When to Run

- After modifying security-critical code (policy, tools, agent, signing, audit, sandbox, path_guard)
- After adding new tool kinds or mask bits
- After changing Lock struct fields
- After modifying agent RPC protocol messages or states
- Before releases

## Sync Check Details

The script checks:
- Mask bit count matches Kind enum variant count
- Lock field count matches between Zig and Lean
- Tool filter presence in evaluate model
- ctEql function exists
- Agent RPC state/message counts

If `.lake/` is missing: `ln -s /tmp/pz-lake proofs/lean/.lake` then `cd proofs/lean && ~/.elan/bin/lake update && lake build`

---
> Source: [joelreymont/pz](https://github.com/joelreymont/pz) — distributed by [TomeVault](https://tomevault.io).
<!-- tomevault:4.0:skill_md:2026-07-01 -->