# Kani Harness Gen

> >

- **Type:** Skill
- **Install:** `agentstack add skill-yue-zhou1-zkcrypto-audit-kani-harness-gen`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [Yue-Zhou1](https://agentstack.voostack.com/s/yue-zhou1)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [Yue-Zhou1](https://github.com/Yue-Zhou1)
- **Source:** https://github.com/Yue-Zhou1/zkcrypto-audit/tree/main/plugins/evidence-and-tooling/skills/kani-harness-gen

## Install

```sh
agentstack add skill-yue-zhou1-zkcrypto-audit-kani-harness-gen
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# kani-harness-gen

Generate `#[kani::proof]` harnesses for formal verification of Rust cryptographic code.

**This skill is user-triggered only.** It must never be auto-invoked by the
audit router or any other skill. It consumes significant computation resources
(default timeout: 5 minutes per harness via `KANI_TIMEOUT_SECONDS`).

## When to Use

- User explicitly requests Kani verification
- User invokes this skill by name
- A Phase 2 finding needs stronger formal proof beyond the standard compilable PoC test

## When NOT to Use

- Never auto-trigger from audit flow
- Never run without explicit user request
- Code is not Rust
- cargo-kani is not installed (detect and warn)

## Prerequisites

Before generating harnesses, verify cargo-kani is available:

```bash
cargo kani --version 2>/dev/null || echo "ERROR: cargo-kani not installed. Install from https://github.com/model-checking/kani"
```

If not installed, inform the user and stop.

## Core Harness Categories

1. **Field arithmetic** — `a * inverse(a) == 1` for all non-zero `a`
2. **No-panic** — function does not panic for any input within type bounds
3. **Serialization roundtrip** — `deserialize(serialize(x)) == x`
4. **Constraint soundness** — satisfying witness implies valid statement
5. **State invariants** — API pre/post-conditions and rejection behavior over bounded inputs

## Limits

- Kani does not prove constant-time behavior or model timing/microarchitectural side channels.
- `kani::assume` constrains input space; it does not provide timing-side-channel guarantees.
- For timing analysis, route to `side-channel-auditor` (and supporting tools like `dudect`/`ctgrind`).

## Budget and Fallback Controls

- Override harness timeout with `KANI_TIMEOUT_SECONDS` (default `300`)
- Keep unwind bounds explicit in harness code so run cost remains predictable
- Use optional `PROPTEST_CASES` for lightweight `proptest` fallback checks when Kani is unavailable or too expensive

## Workflow

### Phase 1: Identify verification targets

- Read the code under audit
- Identify functions with formal-verification-worthy properties
- Read `references/kani-checklist.md` for pre-generation checks

### Phase 2: Generate harnesses

- Read `references/harness-patterns.md` for templates
- Generate `#[kani::proof]` functions tailored to the target code
- Set appropriate `#[kani::unwind(N)]` bounds
- Write harnesses to a test file in the target project

### Phase 3: Execute and interpret

- Run `cargo kani --harness {name}` with `KANI_TIMEOUT_SECONDS` (default 300 seconds)
- If verification succeeds: property holds for all inputs within bounds
- If counterexample found: extract the failing input as PoC evidence
- If Kani is unavailable, run targeted `proptest` checks (bounded by `PROPTEST_CASES`) and clearly label evidence type
- Report results for use by `crypto-fp-check`

## Output Contract

Produce Kani verification results that include:

- The harness code generated
- The property being verified
- PASS (property holds) or FAIL (counterexample found)
- If FAIL: the counterexample input values for PoC evidence
- The kani::unwind bound used and its coverage implications

## Reference Index

- [references/kani-checklist.md](references/kani-checklist.md)
- [references/harness-patterns.md](references/harness-patterns.md)

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [Yue-Zhou1](https://github.com/Yue-Zhou1)
- **Source:** [Yue-Zhou1/zkcrypto-audit](https://github.com/Yue-Zhou1/zkcrypto-audit)
- **License:** MIT

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-yue-zhou1-zkcrypto-audit-kani-harness-gen
- Seller: https://agentstack.voostack.com/s/yue-zhou1
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.