mermaid-to-proverif

An agent skill by trailofbits, from trailofbits/skills. Tags: crypto, documentation, formal-verification, generative.

What it does

Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files). Use when generating a ProVerif model, formally verifying a protocol, converting a Mermaid diagram to ProVerif, verifying protocol security properties (secrecy, authentication, forward secrecy), checking for replay attacks, or producing a .pv file from a sequence diagram.

Install

With the skills CLI, which installs into Claude Code, Codex, Cursor and other agents:

npx skills add trailofbits/skills --skill mermaid-to-proverif

Or copy the skill folder into Claude Code's skills directory by hand (~/.claude/skills for every project, or .claude/skills inside one):

git clone --depth 1 https://github.com/trailofbits/skills
cp -r skills/plugins/trailmark/skills/mermaid-to-proverif ~/.claude/skills/mermaid-to-proverif

Safety box score

Grade A, minimal risk: 7 of 100 risk points, rated 2026-10-19. The grade rates what the skill and its scripts can reach on the machine of whoever installs it, across eight categories from shell execution to secrets access. How the score works.

This skill is a documentation-and-model-generation helper for ProVerif: it reads Mermaid sequence diagrams and writes `.pv` verification models. The main exposure is limited local file writes and a small test harness that can invoke the local `proverif` binary; there is no network, secret, or privilege-seeking behavior in the shipped files.

Category levels, from 0 (none) to 3 (high)
Category	Level	Why
Code & shell execution	1 (low)	The shipped test script shells out to a local verifier with `subprocess.run([proverif, str(SAMPLE)], ...)`, but it only runs the bundled sample model and does not execute arbitrary downloaded code.
Network access	0 (none)	No file downloads, uploads, API calls, or remote hosts are referenced; the files only describe local reads/writes and local verifier execution.
Filesystem reach	1 (low)	The skill’s purpose is to create `.pv` files — `SKILL.md` says it “produces a ProVerif model (`.pv` file)” and “Write the model to a `.pv` file,” but nothing points outside the working tree.
Secrets & credentials	0 (none)	There is no handling of tokens, passwords, `.env` files, keychains, or CLI logins in the skill or shipped scripts.
Privilege & persistence	0 (none)	No `sudo`, global installs, services, scheduled tasks, shell startup edits, or OS setting changes appear in the shipped files.
Instruction hijack surface	0 (none)	The docs are prescriptive but do not tell the agent to ignore higher-priority instructions, hide content, or follow remote/fetched instructions.
Irreversible actions	0 (none)	The skill generates formal verification artifacts and summaries only; it does not send messages, publish, deploy, pay, or delete anything.
Transparency	0 (none)	All shipped assets are human-readable Markdown/YAML/Python/SVG; there are no binaries, minified blobs, or opaque installers.

Before installing

Read `tests/test_guidance.py`; it will execute the `proverif` binary found on PATH during tests.
Use a scratch workspace first so generated `.pv` files cannot overwrite important models.
If you plan to run the tests, pin a trusted ProVerif installation before enabling the skill.

Rated 2026-10-19 by an automated review of 8 files from the skill's repository.

Source

Repository: trailofbits/skills (all skills from this repository)
Path: plugins/trailmark/skills/mermaid-to-proverif/SKILL.md
Branch: main
Collection: trailmark
Updated: 2026-09-19

crypto-protocol-diagram — Extracts protocol message flow from source code, RFCs, academic papers, pseudocode, informal prose, ProVerif (.pv).
vector-forge — Mutation-driven test vector generation.
testing-handbook-generator — Generates Claude Code skills from the Trail of Bits Testing Handbook (appsec.guide).
writing-lean-proofs — Writes and reviews structured Lean 4 proofs and designs Lean libraries following Mathlib conventions.
cli-demo-generator — Generates professional animated CLI demos as GIFs using VHS terminal recordings.
prompt-engineer — Writes, refactors, and evaluates prompts for LLMs — generating optimized prompt templates, structured output schemas, evaluation rubrics, and test suites.