# Verify Rust Proofs and SMT Queries with Sail

Repeated Verus checks and SMT queries can slow proof development and complicate evidence tracking. This skill guides Sail workflows for cached verification, repair validation, and accurate result interpretation.

## Install

```bash
npx skillstore add chelis-lang/sail-verification
```

## Metadata

- Status: approved
- Slug: chelis-lang-sail-verification
- Version: 1.0.0
- Author version: 1.0.0
- Skillstore revision: r2
- Version status: not\_bumped
- Tree hash: 8b4e53c3b21769cd387ceecab8c0de47fe298490c12efae20d24247e46b2e8f6
- Author: chelis-lang
- GitHub username: chelis-lang
- License: MIT
- Repository: https://github.com/chelis-lang/sail/tree/d8e6c3407d8194a6c39f25353364fe0eba52ea7e/skills/sail-verification
- Ref: 1560e56cb7d29b28375339f36876381de0b278b2
- Supported tools: Claude, Codex, Claude Code
- Audit status: complete
- Agent install advisory: allowed
- Manual install advisory: allowed
- Artifact signature: available
- Audit attestation: unavailable
- Human verification: not\_verified
- Risk factors: external\_commands, network
- Quality score: 77
- Quality tier: bronze
- Public page: https://skillstore.pages.dev/skills/chelis-lang-sail-verification
- Manifest: https://skillstore.pages.dev/api/skills/chelis-lang-sail-verification/manifest

## Capabilities

- Guide Cargo project verification with Sail and interpret failure diagnostics.
- Explain proof-repair checks that require a full-target verification result.
- Guide complete SMT-LIB requests through bundled Z3 with cached decided results.
- Distinguish verification freshness, result scope, and proof success.
- Describe CLI and MCP workflows for background verification jobs.
- Explain release-dependent standalone verification and cache management.

## Use Cases

- Iterate on Rust contracts: Use Sail diagnostics and reusable solver work while developing Verus proofs without weakening intended contracts.
- Validate automated proof repairs: Check candidate repairs, inspect completed jobs, and require current full-target success before accepting changes.
- Repeat constraint checks: Submit complete SMT-LIB transcripts, inspect models or unsat cores, and reuse matching decided results.

## Prompt Templates

### Verify an existing project

```
Use Sail to verify this Cargo/Verus project. Report the verdict, checked scope, freshness, and failure diagnostics.
```

### Run an SMT query

```
Check Sail runtime capabilities, then run my SMT-LIB transcript. Report each satisfiability result, requested model or core, and cache reuse.
```

### Check a candidate proof repair

```
Validate my candidate repair for [package] and [function] with Sail. Preserve the contract and require current full-target success before accepting it.
```

### Track background verification

```
Use the configured Sail MCP server to submit background verification for [project]. Inspect installed schemas, read the completed result, and report scope and freshness.
```

## Limitations

- Requires an installed Sail runtime on Linux x86-64 or Apple-silicon macOS.
- Standalone verification and cache budget commands depend on the installed Sail release.
- Proof-repair validation requires the interactive engine; the agent must write the candidate repair.
- SMT answers apply only to submitted formulas; partial or historical verification does not establish a current full-target proof.

## Best Practices

- Check installed help, MCP schemas, and release compatibility before choosing a workflow.
- Require the correct scope, a successful verdict, and Current evidence before accepting verification.
- Keep logs and transcripts outside watched inputs, and preserve intended contracts during repairs.

## Anti Patterns

- Accepting a focused function pass as proof that the entire target verifies.
- Treating runtime readiness, Unknown results, or timeouts as successful solver evidence.
- Weakening contracts to hide implementation failures.

## Security Audit

- Audited at: 2026-11-04T17:01:29.165\+00:00
- Summary: All nine static findings are false positives: seven match Markdown backticks, and two identify documentation links without data transmission instructions. No evidence found of prompt injection, credential collection, or exfiltration in the reviewed skill files. The documented commands support local verification and solver workflows, but the external Sail implementation was not audited.

## Stats

- Views: 0
- Downloads: 2
- Favorites: 0
- Popularity score: 0