File contents Sync Proofs
Verify Lean/TLA+ proofs match current Zig code, rebuild if stale.
Steps
Run sync check: cd $(git rev-parse --show-toplevel) && bash proofs/sync_check.sh
If stale: identify which proofs need updating from the output
Update stale Lean files in proofs/lean/PzProofs/
Rebuild: cd proofs/lean && ~/.elan/bin/lake build
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 — distributed by TomeVault .
1 --- 2 name: joelreymont-pz-pz 3 description: Sync Proofs 4 --- 5 6 # Sync Proofs 7 8 Verify Lean/TLA+ proofs match current Zig code, rebuild if stale. 9 10 ## Steps 11 12 1. Run sync check: `cd $(git rev-parse --show-toplevel) && bash proofs/sync_check.sh` 13 2. If stale: identify which proofs need updating from the output 14 3. Update stale Lean files in `proofs/lean/PzProofs/` 15 4. Rebuild: `cd proofs/lean && ~/.elan/bin/lake build` 16 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` 17 18 ## When to Run 19 20 - After modifying security-critical code (policy, tools, agent, signing, audit, sandbox, path_guard) 21 - After adding new tool kinds or mask bits 22 - After changing Lock struct fields 23 - After modifying agent RPC protocol messages or states 24 - Before releases 25 26 ## Sync Check Details 27 28 The script checks: 29 - Mask bit count matches Kind enum variant count 30 - Lock field count matches between Zig and Lean 31 - Tool filter presence in evaluate model 32 - ctEql function exists 33 - Agent RPC state/message counts 34 35 If `.lake/` is missing: `ln -s /tmp/pz-lake proofs/lean/.lake` then `cd proofs/lean && ~/.elan/bin/lake update && lake build` 36 37 --- 38 > Source: [joelreymont/pz](https://github.com/joelreymont/pz) — distributed by [TomeVault](https://tomevault.io). 39 <!-- tomevault:4.0:skill_md:2026-07-01 -->
commit bf8952d17d
Frequently asked questions How do I install the Joelreymont Pz Pz skill? Run npx skillmds@latest add tomevault-io/joelreymont-pz-pz in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.
What does the Joelreymont Pz Pz skill do? Sync Proofs It is listed under Coding & Dev Tools on SkillMD.
Is Joelreymont Pz Pz safe to use? This skill has not completed SkillMD's automated safety review yet. Independent scanners report: SkillSpector: PASS, Skill Scanner: PASS. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.
Which AI agents work with Joelreymont Pz Pz? This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.
Is Joelreymont Pz Pz free to use? Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.
Who published Joelreymont Pz Pz? tomevault-io (@tomevault-io) published this skill. Their other Agent Skills are listed on their SkillMD profile.
tomevault-io