Sync Proofs
SkillDev toolsCheck proof-code sync and rebuild proofs. Triggers: "sync proofs", "check proofs sync", "are proofs stale", "proof sync".
Available today. Use it from your connected AI after setup.
No other account needed.
Connect ahel once, and every AI you use reads what you have installed.
Then ask your AI: use the Sync Proofs skill
What this skill tells your AI
The instructions your AI receives, as published by joelreymont/pz in .claude/skills/sync-proofs/SKILL.md and read by ahel’s review.
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
Signals
- GitHub stars
- 95
- Forks
- 8
- Last commit
- Apr 2026
Advanced
- Catalog kind
- skill
- Gateway key
sync-proofs- Source
- github.com/joelreymont/pz