# Kani Harness Gen

> Generate Kani proof harnesses for Rust crypto code. User-triggered only — never auto-invoked by the audit flow. Produces formal verification evidence for crypto-fp-check.

- Skill: `yue-zhou1/kani-harness-gen` (Agent Skill)
- Install (CLI): `npx skillmds@latest add yue-zhou1/kani-harness-gen`
- Raw SKILL.md: https://api.skillmd.com/api/skills/yue-zhou1/kani-harness-gen/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Security
- Author: Yue-Zhou1 (https://skillmd.com/u/yue-zhou1)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/yue-zhou1/kani-harness-gen

---


This file is a Codex skill discovery stub.

Canonical skill source:
`plugins/evidence-and-tooling/skills/kani-harness-gen/SKILL.md`

When this skill is selected, follow the canonical source file above.