A checker that compares Lean and TLA+ formal proofs with the current Zig code and rebuilds them when needed. Lean and TLA+ are tools for writing and checking mathematical descriptions of program behaviour.

Use it after changing security, locking, tool, or agent-protocol code, and before releases. It checks selected counts and declarations, identifies stale Lean files, rebuilds Lean proofs, and can rerun TLA+ models when specifications change.

It helps detect when security-related code has changed but its proofs or models have not been updated. This reduces the risk of relying on verification that no longer matches the implementation.

How joelreymont/pz configures Claude Code

Reuse

Borrowing it

Nothing to install: this file belongs to joelreymont/pz. Take a copy, put it at the same path in your own repository, and replace the rules that are about this project with yours.

Copy the file

curl -O https://raw.githubusercontent.com/joelreymont/pz/main/.claude/skills/sync-proofs/SKILL.md

Clone the repo

git clone --depth 1 https://github.com/joelreymont/pz

Made for: Claude Code.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

README.md

[![agentmods](https://agentmods.dev/badge/skills/joelreymont/pz/sync-proofs/github.svg)](https://agentmods.dev/skills/joelreymont/pz/sync-proofs)

Your own site

<a href="https://agentmods.dev/skills/joelreymont/pz/sync-proofs"><img src="https://agentmods.dev/badge/skills/joelreymont/pz/sync-proofs/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

Your own site · 80×15

<a href="https://agentmods.dev/skills/joelreymont/pz/sync-proofs"><img src="https://agentmods.dev/badge/skills/joelreymont/pz/sync-proofs.svg" alt="Reviewed on agentmods" width="80" height="20"></a>

Per session 33 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.

When invoked 358 The whole file, excluding the scripts and references it only reads on demand.

Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe.

Origin original No closer match found in the catalogue.

Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

Model	Per session	Once invoked
Fable 5.1	$0.00033	$0.00358
Opus 5.5	$0.00013	$0.00143
Sonnet 5.5	$0.00007	$0.00072
Haiku 4.5	$0.00003	$0.00036

Measured 2mo ago against content hash 45a2b0c6126d, method: parsed. Prices are Anthropic first-party input rates as of 2026-10-07, from the pricing page.

Security

Grade A, and why

sync-proofs scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 2mo ago.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

.claude/skills/sync-proofs/SKILL.md · 37 lines

What it actually says

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

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

2mo ago First seen · 37 lines · 33 tokens per session scan A 45a2b0c6126d

Subscribe to this mod's changes

sync-proofs is a skill published in the GitHub repository joelreymont/pz (100 stars, last pushed 7mo ago), licensed MIT. It adds 33 tokens to every session and 358 once invoked, about $0.0001 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.

Scientific

sync-proofs next to 6 skills from other repositories
Mod	Type	Stars	Last push	Licence	Scan	Tokens	Works with
sync-proofsjoelreymont/pz	Skill	100	7mo ago	MIT	A	33	Claude Code
instrument-data-to-allotropeanthropics/knowledge-work-plugins	Skill	35k	2d ago	Apache-2.0	A	123	Claude Code
exploratory-data-analysisK-Dense-AI/scientific-agent-skills	Skill	56k	4d ago	MIT	A	83	Claude Code
matlabK-Dense-AI/scientific-agent-skills	Skill	56k	4d ago	MIT	A	44	Claude Code
phylogeneticsK-Dense-AI/scientific-agent-skills	Skill	56k	4d ago	MIT	A	71	Claude Code, Codex
research-engineerdavila7/claude-code-templates	Skill	33k	yesterday	MIT	A	43	Claude Code, Codex
mapping-to-snomedmaziyarpanahi/openmed	Skill	5.8k	yesterday	Apache-2.0	A	205	Claude Code

pz: Skill for Claude Code