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

Not rated yet. A safety box score grades what a skill and its scripts can reach on the machine of whoever installs it, across eight categories from shell execution to secrets access. Anyone can request one from this page; it is saved for everyone. How the score works.

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

Related skills

• crypto-protocol-diagram — spthy) models and generates Mermaid sequenceDiagrams with cryptographic annotations.
• vector-forge — Mutation-driven test vector generation.
• testing-handbook-generator — md files with the structure each skill type requires. guide. Not for answering security testing questions — the generated skills cover those.
• 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.