How do I install the Lean Security Formalization skill?

Run npx skillmds@latest add r-irbe/lean-security-formalization in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Lean Security Formalization safe to use?

This skill has not completed SkillMD's automated safety review yet. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Lean Security Formalization?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Lean Security Formalization free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Lean Security Formalization?

r-irbe (@r-irbe) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Lean Security Formalization by r-irbe

Name: Lean Security Formalization
Author: r-irbe

Lean Security Formalization

USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties. DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.

r-irbe d576adf 3.3 KB Updated Sep 17, 2026

File contents

Lean 4 Security & Privacy Formalization

Guide to formalizing security properties, access control, information flow, and privacy in Lean 4.

Routing

USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties.
DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization).
TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.

Workflow

Identify the security property class: information flow, access control, cryptographic, or privacy.
Pick the matching encoding from the body (non-interference, BLP-Lean, IND-CPA-Lean, k-anonymity-Lean).
Produce the Lean statement + proof skeleton; verify Mathlib primitives at the pin.
Hand off: to @lean-proof-review for review, to @lean-enforcement for CI, to @applied-data-information-security if the model is wrong.

Recovery & STOP

STOP if the question is about policy design — delegate to @applied-data-information-security.
STOP if Mathlib lacks the cryptographic primitive — escalate to @lean-research.
STOP if the property has not been formally stated — delegate to @lean-specification.

Handoffs

Predecessors: agent:gateway, skill:lean-research.
Successors: skill:lean-proof-review, skill:lean-enforcement, skill:lean-zettelkasten.

Detailed reference

Full content for lean-security-formalization lives in references/lean-security-formalization-handbook.md. Load that file when the skill is convened; the SKILL.md only carries the dispatch contract and the parts index.

Section	Topic
Part 1	Security Properties
Part 2	Access Control Models
Part 3	Information Flow
Part 4	Privacy and Data Protection
Part 5	Cryptographic Properties
Part 6	Trust Models
Part 7	Research Council Integration

---name: lean-security-formalizationdescription: USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties. DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.---# Lean 4 Security & Privacy FormalizationGuide to formalizing security properties, access control, information flow, and privacy in Lean 4.---## Routing- **USE FOR:** Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties.- **DO NOT USE FOR:** security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization).- **TRIGGERS:** security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.## Workflow1. Identify the security property class: information flow, access control, cryptographic, or privacy.2. Pick the matching encoding from the body (non-interference, BLP-Lean, IND-CPA-Lean, k-anonymity-Lean).3. Produce the Lean statement + proof skeleton; verify Mathlib primitives at the pin.4. Hand off: to `@lean-proof-review` for review, to `@lean-enforcement` for CI, to `@applied-data-information-security` if the model is wrong.## Recovery & STOP- STOP if the question is about policy design — delegate to `@applied-data-information-security`.- STOP if Mathlib lacks the cryptographic primitive — escalate to `@lean-research`.- STOP if the property has not been formally stated — delegate to `@lean-specification`.## Handoffs- **Predecessors:** `agent:gateway`, `skill:lean-research`.- **Successors:** `skill:lean-proof-review`, `skill:lean-enforcement`, `skill:lean-zettelkasten`.---## Detailed referenceFull content for `lean-security-formalization` lives in[`references/lean-security-formalization-handbook.md`](../../references/lean-security-formalization-handbook.md).Load that file when the skill is convened; the SKILL.md only carriesthe dispatch contract and the parts index.| Section | Topic ||---|---|| Part 1 | Security Properties || Part 2 | Access Control Models || Part 3 | Information Flow || Part 4 | Privacy and Data Protection || Part 5 | Cryptographic Properties || Part 6 | Trust Models || Part 7 | Research Council Integration |---## See also- [`../../references/lean-security-formalization-handbook.md`](../../references/lean-security-formalization-handbook.md) — Full handbook (extracted from this skill)- [`../lean-proof-review/SKILL.md`](../lean-proof-review/SKILL.md) — Successor- [`../lean-enforcement/SKILL.md`](../lean-enforcement/SKILL.md) — Successor- [`../lean-zettelkasten/SKILL.md`](../lean-zettelkasten/SKILL.md) — Successor

Frequently asked questions