verusification-table

verusification-table is a cursor rule for Cursor from briangmilnes/APAS-VERUS. It costs 518 tokens per session, scanned A, original, MIT.

A required report format for reviewing how much of an algorithms chapter has been implemented and formally verified. Verusification means checking program correctness with the Verus verification tool.

In plain words
What is it for?
Use it to map textbook sections to source files, inspect each file’s verification structure, and classify every public function’s specification and proof status.
Why use it?
It makes missing algorithms, weak specifications, unfinished proofs, and unverified function bodies visible in one structured review.

Cursor rule for Cursor

Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

agentmods
npx agentmods add rules/briangmilnes/apas-verus/verusification-table
Clone the repo
git clone --depth 1 https://github.com/briangmilnes/APAS-VERUS

Made for: Cursor.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

agentmods badge for verusification-table

README.md
[![agentmods](https://agentmods.dev/badge/rules/briangmilnes/apas-verus/verusification-table.svg)](https://agentmods.dev/rules/briangmilnes/apas-verus/verusification-table)
Your own site
<a href="https://agentmods.dev/rules/briangmilnes/apas-verus/verusification-table"><img src="https://agentmods.dev/badge/rules/briangmilnes/apas-verus/verusification-table.svg" alt="Measured on agentmods" height="20"></a>
Per session 518 This file is loaded in full into every session.
When invoked 518 The same file — it is already loaded in full.
Security scan A 0 findings. Scan, not verified.
Origin original No closer match found in the catalogue.
Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

ModelPer sessionOnce invoked
Fable 5 $0.00518 $0.00518
Opus 5 $0.00259 $0.00259
Sonnet 5 $0.00104 $0.00104
Haiku 4.5 $0.00052 $0.00052

Measured 4d ago against content hash ba96fe1d28d3, method: parsed. Prices are Anthropic first-party input rates as of 2026-08-30, from the pricing page.

Security

Grade A, and why

verusification-table scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 4d ago.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

.cursor/rules/apas-verus/verusification-table.mdc · 55 lines

What it actually says

Verusification Status Table

When the user asks for a "verusification table" or "verusification status" for a chapter, produce a structured review with the following sections.

1. Prose Coverage

Map each prose section/algorithm to implementation files. Flag missing algorithms.

# Prose Section Description File(s) Status
1 §N Algorithm Name Brief description File.rs Implemented / Missing

2. Per-File Verusification Status

For each source file, report structural verusification:

# File verus! block Spec fns Trait specs Impl bodies Proof holes
1 File.rs Yes/No count count with ensures verified / external_body count × type

3. Spec Strength Assessment

Classify every public function's spec strength and proof hole status:

# Function File Spec Strength Holes Notes
1 fn_name File.rs Brief spec summary strong/partial/weak/none verified / external_body / assume(N) / admit Gap description

The Holes column reports the verification status of the function body:

  • verified — body fully verified, no holes
  • external_body — body not checked by Verus
  • assume(N) — N assume(...) statements in body
  • admit — contains admit()
  • A function may have multiple hole types (e.g., external_body on one arm, assume on another)

Use the standard classification from classify-spec-strengths.mdc.

4. Summary

Metric Value
Strong specs N
Partial specs N
Weak / None specs N
Fully verified bodies N
external_body holes N
assume holes N
Prose algorithms missing N

When to Produce

  • When the user says "verusification table", "verusification status", or "verus status"
  • At the start of work on a new chapter (combined with review-against-prose)
  • Before claiming a chapter is complete
Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

  1. 4d ago First seen · 55 lines · 518 tokens per session scan A ba96fe1d28d3

Subscribe to this mod's changes

verusification-table is a cursor rule published in the GitHub repository briangmilnes/APAS-VERUS (10 stars, last pushed 1mo ago), licensed MIT. It adds 518 tokens to every session, about $0.0026 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.