sync-proofs

star 89

Check proof-code sync and rebuild proofs. Triggers: "sync proofs", "check proofs sync", "are proofs stale", "proof sync".

joelreymont By joelreymont schedule Updated 3/15/2026
play_arrow Run Skill in Manus View GitHub

name: sync-proofs description: 'Check proof-code sync and rebuild proofs. Triggers: "sync proofs", "check proofs sync", "are proofs stale", "proof sync".' user_invocable: true

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

Install via CLI
npx skills add https://github.com/joelreymont/pz --skill sync-proofs
Repository Details
star Stars 89
call_split Forks 8
navigation Branch main
article Path SKILL.md
Occupations
Computer And Information Research Scientists 151221
More from Creator
joelreymont
joelreymont Explore all skills →