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.
git clone --depth 1 https://github.com/briangmilnes/APAS-VERUSWrote 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.
[](https://agentmods.dev/rules/briangmilnes/apas-verus/float-axiom-fixes)<a href="https://agentmods.dev/rules/briangmilnes/apas-verus/float-axiom-fixes"><img src="https://agentmods.dev/badge/rules/briangmilnes/apas-verus/float-axiom-fixes.svg" alt="Measured on agentmods" height="20"></a>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.00570 | $0.00570 |
| Opus 5 | $0.00285 | $0.00285 |
| Sonnet 5 | $0.00114 | $0.00114 |
| Haiku 4.5 | $0.00057 | $0.00057 |
Grade A, and why
float-axiom-fixes 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 7d 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.
What it actually says
Float Axiom Fixes
Context
Chap56-59 have duplicated Float/I64 file pairs for graph algorithms (SSSP results, Dijkstra,
Bellman-Ford, Johnson). The Float files are entirely external_body or outside verus! — no
verification at all. The I64 files are partly or fully verified.
vstdplus/float.rs Provides
FloatTotalOrdertrait for f64/f32: reflexive, antisymmetric, transitive, totalityfloat_wf(x)=is_finite_spec()(excludes NaN and infinity)le(self, other)via uninterpretedle_ensures- Exec
float_cmpreturningOrdering - Broadcast group
group_float_finite_total_order
What It Does NOT Provide
- No arithmetic axioms (no
a + breasoning for f64) - No axioms for
OrderedFloat<f64>(external crate wrapper)
Strategy: Easiest First
- SSSPResultStEphFloat.rs — No float arithmetic, just stores/retrieves OrderedF64 values.
The I64 version is already verified. Main challenge: bridging
OrderedFloat<f64>to f64 axioms. - SSSPResultStPerFloat.rs — Same pattern, persistent variant.
- AllPairsResult*Float.rs — Same pattern, matrix of distances.
- DijkstraStEphFloat.rs — Needs float addition axioms (dist + weight).
- BellmanFordStEphFloat.rs — Needs float addition axioms.
- Johnson*Float.rs — Depends on Dijkstra + BellmanFord.
Key Challenge: OrderedFloat
The Float files use OrderedFloat<f64> from the ordered_float crate for Eq + Ord + Hash.
Options to bridge to Verus:
- (a) Switch stored type to raw
f64, useFloatTotalOrder::float_cmpfor comparisons - (b) Write
#[verifier::external_type_specification]forOrderedFloat<f64>
Algorithm Files Need New Axioms
Dijkstra, Bellman-Ford, Johnson all do dist.0 + weight.0 — float addition.
This requires axioms not yet in vstdplus/float.rs:
- Finite + finite = finite (when no overflow)
- Monotonicity: a <= b ==> a + c <= b + c (for finite values)
- Identity: a + 0.0 = a
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.
- 7d ago First seen · 51 lines · 570 tokens per session scan A 061bce9795a5
float-axiom-fixes is a cursor rule published in the GitHub repository briangmilnes/APAS-VERUS (10 stars, last pushed 1mo ago), licensed MIT. It adds 570 tokens to every session, about $0.0029 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.
Other cursor rules, from other repositories
core
Core STT/TTS abstraction layer documentation.
rust-module-refactor
Use when splitting Rust modules, moving tests, tightening visibility, or preserving facades during refactors.
rust-architect
PoolAI — Rust Architect workflow: runtime stack, MSYS2, target/ disk, pre-push checks, docs sync.
rust-development-standards
Rust development standards: idioms, style, anti-patterns (Rust 2021 edition, 2024 where applicable).
cube-engine
Use when changing Rust puzzle state, moves, notation, scrambles, or validation.
ivolgaql-project
General development rules for ИволгаQL, an early-stage Rust project with a command-line and TCP server interface. They define the project structure, Russian user experience, coding conventions, testing, builds, and commit-message format.