OrCa property discoverer
Overview
Draft code-grounded English properties before writing [V] specs.
Required reference
Read ../references/specs-and-counterexamples.md.
Sub-agent use
Use sub-agents for source-heavy property discovery. Split by subsystem, target contract group, or property category when possible, and ask each agent to return only English properties, observables, rationale, source references, and [V] feasibility notes. The main campaign context does not need the full code-reading trail once the English properties and caveats are captured in orca_config/specs/properties.md.
Workflow
- Inspect target contracts, tests, docs, deployment scripts, and prior findings.
- Identify protocol assets, accounting units, actors, trust boundaries, and lifecycle states.
- Draft English properties that express intended behavior through observable API effects where possible.
- Group properties by accounting, access control, solvency, standards compliance, oracle assumptions, lifecycle, and emergency behavior.
- Mark properties that may need helper contracts, ghost variables, approximations, or weaker/stronger [V] variants.
- Write or update
orca_config/specs/properties.md when asked to store artifacts.
Output
For each property include title, English statement, contracts/functions involved, observables, rationale, likely [V] feasibility, and caveats.
Do not mirror implementation internals as the property itself; use code review to infer intended behavior, then express the intended protocol rule.
1---2name: audithub-orca-property-discoverer3description: Discover English-language protocol properties for OrCa fuzzing. Use when a user wants real specifications after setup tuning, asks what invariants or temporal properties should hold, needs code/tests/docs reviewed for OrCa properties, or wants a properties.md handoff before [V] translation.4---56# OrCa property discoverer78## Overview910Draft code-grounded English properties before writing [V] specs.1112## Required reference1314Read `../references/specs-and-counterexamples.md`.1516## Sub-agent use1718Use sub-agents for source-heavy property discovery. Split by subsystem, target contract group, or property category when possible, and ask each agent to return only English properties, observables, rationale, source references, and [V] feasibility notes. The main campaign context does not need the full code-reading trail once the English properties and caveats are captured in `orca_config/specs/properties.md`.1920## Workflow21221. Inspect target contracts, tests, docs, deployment scripts, and prior findings.232. Identify protocol assets, accounting units, actors, trust boundaries, and lifecycle states.243. Draft English properties that express intended behavior through observable API effects where possible.254. Group properties by accounting, access control, solvency, standards compliance, oracle assumptions, lifecycle, and emergency behavior.265. Mark properties that may need helper contracts, ghost variables, approximations, or weaker/stronger [V] variants.276. Write or update `orca_config/specs/properties.md` when asked to store artifacts.2829## Output3031For each property include title, English statement, contracts/functions involved, observables, rationale, likely [V] feasibility, and caveats.3233Do not mirror implementation internals as the property itself; use code review to infer intended behavior, then express the intended protocol rule.
Veridise