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.
npx skills add plurigrid/asi --skill formal-verification-aigit clone --depth 1 https://github.com/plurigrid/asiWrote 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/skills/plurigrid/asi/formal-verification-ai)<a href="https://agentmods.dev/skills/plurigrid/asi/formal-verification-ai"><img src="https://agentmods.dev/badge/skills/plurigrid/asi/formal-verification-ai/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/plurigrid/asi/formal-verification-ai"><img src="https://agentmods.dev/badge/skills/plurigrid/asi/formal-verification-ai.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
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.00608 |
| Opus 5 | $0.00000 | $0.00304 |
| Sonnet 5 | $0.00000 | $0.00122 |
| Haiku 4.5 | $0.00000 | $0.00061 |
Grade A, and why
formal-verification-ai 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 6d 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.
How it starts
The opening of the file, as written. The whole thing — 80 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Formal Verification AI
Category: Phase 3 Core - Correctness Guarantees
Status: Skeleton Implementation
Dependencies: categorical-composition (correctness as functoriality)
Overview
Integrates formal verification methods with AI systems: theorem proving for correctness guarantees, interval arithmetic for certified bounds, and categorical proofs for compositional correctness.
Capabilities
- Theorem Proving: Automated verification of AI properties
- Interval Arithmetic: Certified bounds on network outputs
- Categorical Correctness: Functorial preservation guarantees
- Adversarial Robustness: Verified defense certificates
Core Components
-
Theorem Prover Interface (
theorem_proving.jl)- Integration with Z3, Lean, or Coq
- Encode neural networks as logical formulas
- Automated proof search
-
Interval Arithmetic (
interval_arithmetic.jl)- Interval propagation through networks
- Certified bounds on outputs
- Robustness verification
-
Categorical Proofs (
categorical_correctness.jl)- Verify functor laws for compositional networks
- Natural transformation diagrams
- Commutativity checking
-
Verification Examples (
verification_examples.jl)- Adversarial robustness proofs
- Fairness guarantees
- Safety-critical system verification
Integration Points
- Input from: All Phase 3 skills (provides verification layer)
- Output to:
categorical-composition(verified transformations) - Coordinates with:
oriented-simplicial-networks(topological invariants)
Usage
using FormalVerificationAI
# Define neural network
network = SimpleNN([Dense(10, 20, relu), Dense(20, 2)])
# Verify robustness using interval arithmetic
input_interval = Interval([0.0, 0.0], [1.0, 1.0])
output_bounds = propagate_intervals(network, input_interval)
# Prove categorical correctness
F = network_to_functor(network)
@assert verify_functor_laws(F)
# Automated theorem proving
property = "∀x. ||x - x'|| < ε ⟹ ||f(x) - f(x')|| < δ"
proof = prove_property(network, property, timeout=60)
What ships with it
1 file beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
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.
- 6d ago First seen · 80 lines · 0 tokens per session scan A 1b00fe1ee656
formal-verification-ai is a skill published in the GitHub repository plurigrid/asi (62 stars, last pushed 2mo ago), licensed MIT. It costs nothing until one of its globs matches a file; then it loads 608 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-09-03.
Other skills, from other repositories
research-engineer
An uncompromising Academic Research Engineer. Operates with absolute scientific rigor, objective criticism, and zero flair. Focuses on theoretical correctness, formal verification, and optimal implementation across any required technology.
tika-eval-compare
Compare extracts from two Tika builds over a corpus to detect regressions in content, encoding, exceptions, and embedded-document handling. Use for "compare before/after extracts", "eval this change against the corpus".
neuron-evaluation-engineer
Create and run AI evaluations with datasets, assertions, and output drivers in Neuron AI. Use this skill whenever the user mentions evaluation, testing AI systems, creating evaluators, dataset-driven testing, assertion-based validation, or wants to measure AI system performance. Also trigger for tasks involving…
jetson-validate-image
Use after jetson-flash-image to run static BSP checks, on-target smoke/regression tests on a flashed DUT, or both. Not for build or flash steps. Triggers: validate bsp, on-target validation.
atmos-validation
Validate Atmos projects, components, arbitrary JSON Schema inputs, EditorConfig, and GitHub Actions; use affected-file selection and native CI annotations.
skill-benchmark
Benchmark AI skill effectiveness by measuring implementation quality against legacy constraints.