What is when-to-write-ptts?

A guideline for deciding when to write Proof Time Tests, or PTTs—tests that check formal specifications and proofs rather than only program output.

Use it to choose between PTTs and runtime tests for iterators, reused modules, non-obvious specifications, simple functions, and self-contained algorithms.

It avoids the maintenance cost of tests that add little value while protecting fragile iterator proofs, shared building blocks, and specifications that have previously been wrong.

when-to-write-ptts — Cursor rule for Cursor by briangmilnes

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.

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.

README.md

[![agentmods](https://agentmods.dev/badge/rules/briangmilnes/apas-verus/when-to-write-ptts.svg)](https://agentmods.dev/rules/briangmilnes/apas-verus/when-to-write-ptts)

Your own site

<a href="https://agentmods.dev/rules/briangmilnes/apas-verus/when-to-write-ptts"><img src="https://agentmods.dev/badge/rules/briangmilnes/apas-verus/when-to-write-ptts.svg" alt="Measured on agentmods" height="20"></a>

Per session 0 Nothing until a file matches its globs; then the whole rule loads.

When invoked 359 The whole file, excluding the scripts and references it only reads on demand.

Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe.

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.

Model	Per session	Once invoked
Fable 5.1	$0.00000	$0.00359
Opus 5	$0.00000	$0.00179
Sonnet 5	$0.00000	$0.00072
Haiku 4.5	$0.00000	$0.00036

Measured 8d ago against content hash 4c8bb2264731, method: parsed. Prices are Anthropic first-party input rates as of 2026-09-07, from the pricing page.

Security

Grade A, and why

when-to-write-ptts 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 8d 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/when-to-write-ptts.mdc · 37 lines

What it actually says

When to Write Proof-Time Tests

PTTs (rust_verify_test/tests/) are expensive to write and maintain. Only create them when there is a real risk that specs are wrong and a downstream module will suffer.

Write a PTT when

The module exposes iterators. Iteration is the most fragile Verus proof pattern. A PTT should exercise every supported loop form (loop-match, for-iter, for-consuming) to catch invariant regressions.
The module is a building block for later chapters. If Chap18 depends on Chap05's SetStEph, a PTT on SetStEph catches spec errors before they propagate. Leaf modules used by no one else are lower priority.
The spec is non-obvious or has been wrong before. If a function's ensures was corrected during review, a PTT locks in the fix.

Do NOT write a PTT when

The module is self-contained and not imported by other modules.
The module is purely algorithmic with no iteration (e.g., recursive Fibonacci).
The module's specs are trivial (accessors, constructors, delegating calls).
A runtime test already exercises the same code path — RTTs catch exec bugs, PTTs catch spec bugs. If the spec is simple and correct, an RTT suffices.

Priority order

Iterable types used by other chapters (highest risk).
ADT modules with complex specs imported by algorithm chapters.
Everything else (skip unless a specific concern arises).

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.

8d ago First seen · 37 lines · 0 tokens per session scan A 4c8bb2264731

Subscribe to this mod's changes

when-to-write-ptts is a cursor rule published in the GitHub repository briangmilnes/APAS-VERUS (10 stars, last pushed 1mo ago), licensed MIT. It costs nothing until one of its globs matches a file; then it loads 359 tokens. 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.

Testing

when-to-write-ptts

Getting it into your agent

Wrote this? Show the measurements

What it costs to keep this loaded

Grade A, and why

Nothing flagged

What it actually says

When to Write Proof-Time Tests

Write a PTT when

Do NOT write a PTT when

Priority order

What this file has done since we first saw it

Other cursor rules, from other repositories

20-testing-generated-and-structure

fuzzing

testing-and-quality

smoke-monkey-tester

STAGE_S5_TEST_POINTS

testing