[ THE COMPLETE FIELD MANUAL ]
Know what is running.
Usage, configuration, evidence and recovery. Plain text with clickable links, shipped with the software.
[ download + install ] / [ stack YAML ] / [ launch AWS stack ]
Katarina manual
# Katarina manual
For Solidity, start with the [end-to-end review guide] and [complete starter configuration]. They distinguish default analysis from optional research, tools, proof execution and simulation. This manual describes the current source tree; older binaries/configurations do not acquire new capabilities automatically.
New workflows: [dependency and binary audits], [interactive MCP/JSON tools], [investigation memory, progress and preflight].
Katarina coordinates security reviews of Solidity, Java, Rust, C/C++ and other backend repositories. It scouts for potential issues, records independent reviews, and prepares tests and evidence for human assessment. This manual covers configuration, running and resuming reviews, and preparing reports for an audit. Use the reports to prioritize investigation and document design decisions; completed coverage does not establish that a repository is free of vulnerabilities.
## First review
1. [Download and install the prebuilt executable], or build with `make build` and put `bin/katarina` on your PATH. See [development] for build requirements.
2. Run `katarina init` in your working directory. This writes an example `katarina.yaml` without overwriting an existing file.
3. Provide `DEEPSEEK_API_KEY` for the example configuration, or configure different providers and agent models. The API key stays out of CLI arguments and reports.
4. Run `katarina doctor` to check configuration, linked pi support and installed optional tools.
5. Run `katarina index ./project > inventory.json` to inspect included files and explicit exclusions.
6. Run `katarina start --tui ./project` for the [terminal dashboard]. Omit `--tui` for normal logs or CI. Flags must appear before the path.
7. Review `PROJECT/.katarina/sessions/SESSION/audit-handoff.md`, `report.md` and the corresponding JSON. State defaults to `PROJECT/.katarina`; the CLI prints the exact resume command and report directory.
A fresh init has `tests.runner: none` and an empty `tests.commands` map: it does not generate runnable proof plans until you configure a permitted command. With a command and runner `none`, requested plans are saved without execution. Select `local`, `ssh` or `ec2` only after preparing the execution environment.
Concurrency defaults to 16 model workers; use `--max-agents` to adjust it. Set `--token-budget deepseek=100M` to cap that family's token reservations at 100 million. YAML and CLI caps accept `K`, `M`, `B` and `T` suffixes, including amounts such as `1.5B`. Family labels are configured per agent; flags precede the repository path. The printed resume command retains these overrides. See [budgets and concurrency].
## Continue interrupted work
Use the session ID printed at startup:
```sh
katarina sessions --state ./project/.katarina
katarina resume --config katarina.yaml --state ./project/.katarina SESSION
katarina report --state ./project/.katarina SESSION
```
A completed job is reused, including context-request responses and assessor decisions. A call interrupted before its durable result may be retried and billed again. Billing reservations are retained. An interrupted test is marked indeterminate and is not silently repeated.
Resume requires the same repository root, included file contents, inventory and effective configuration. If code, models, budgets or policies change, begin a new session. Credential values can change without invalidating a session. A process lock prevents two controllers writing the same state directory simultaneously.
## Typical Solidity setup
Use the [Solidity workflow] for the full sequence, readiness checks and outputs. This optional execution fragment assumes a prepared Foundry project; edit existing YAML keys rather than appending duplicate blocks.
```yaml
tests:
runner: local
allowed_paths: ["test/Katarina*.t.sol"]
commands:
foundry: [forge, test, --offline, --match-path, "test/Katarina*.t.sol", -vvv]
design_notes: [docs/invariants.md, docs/trust-model.md]
```
The example excludes `lib/**`; remove that exclusion if you want vendored Solidity dependencies included and copied to test workspaces. Explain economic invariants, roles, upgradeability, accepted oracle assumptions, token behavior and off-chain dependencies in design notes. The assessor must cite evidence before labeling an issue “by design.”
## Typical Java setup
```yaml
language_servers:
- name: java
command: [jdtls, -data, "{workspace}"]
extensions: [.java]
language_id: java
timeout_seconds: 120
tests:
runner: local
allowed_paths: ["src/test/java/**"]
commands:
maven: [mvn, -B, -Dtest=KatarinaSecurityTest, test]
```
Use a JDK compatible with the chosen JDT LS release and your project. Supply dependency resolution through an operator-controlled command or prepared toolchain. The clean test environment does not inherit credentials or your usual HOME. Read [navigation] and [testing] for the practical implications.
## Choose what to read next
| Task | Guide |
|---|---|
| Download, verify and install; macOS Gatekeeper | [Installation] |
| Current product scope, defaults, contracts and limitations | [Product specification] |
| Terminology, numbered requirements and failure cases | [Behavior and definitions] |
| Providers, models, credentials and spend limits | [Configuration] |
| Components, diagrams, data flow, FFI and recovery | [Architecture] |
| Competitive position, implemented differentiators and fair comparisons | [Competitive analysis and research design] |
| Start testing: readiness, baselines and outcome scorecard | [Security benchmark assessment] |
| Measure detection, false alarms, evidence and review cost | [Benchmark] |
| Shared security knowledge, specific questions, evidence and grouping | [Security analysis] |
| Shannon's code-analysis workflow and design influences | [Shannon design review] |
| Solidity from first run through findings, proofs and audit handoff | [Solidity workflow] |
| Solidity economic mechanisms, incentives and game theory | [Economics] |
| Reusable simulation campaigns and user-provided SSH machines | [Simulation execution] |
| Chaos Labs lessons and generated economic simulation design | [Economic simulation methodology] |
| EVMBench tasks, scoring limits and integration sequence | [EVMBench assessment] |
| Java/Solidity/Rust/C/C++ navigation and analyzer adapters | [Navigation] |
| Generated tests and execution boundaries | [Testing] |
| Create and use temporary EC2 infrastructure | [AWS] |
| Report schemas and recovering evidence | [Reports] |
| Build, test, package and evaluate Katarina | [Development] |
[Audit methodology] covers operational mistakes, proof quality, related-defect follow-ups, candidate lineage and evidence-backed practice comparisons.
[Investigation ledger] explains guided-agent cooperation, work claims, failure handoffs and enforced unhinted isolation.
[Capability composition] describes post-discovery chain analysis, external authority boundaries, scoped tests and controlled evaluation.
Terminal dashboard
# Terminal dashboard Use `--tui` to follow a review in the terminal: ```sh katarina start --config katarina.yaml --state ./review-state --tui ./project katarina resume --config katarina.yaml --state ./review-state --tui SESSION ``` Flags precede the repository path or session ID. Keep any engine, worker or budget overrides from the printed resume command and add `--tui` before the session ID. Without `--tui`, or when stderr is redirected, Katarina prints ordinary event lines. The dashboard does not change scheduling, prompts, budgets or permissions. ## Reading the map A wide terminal shows the route beside active work. Narrow terminals stack the panels; very short terminals show the current stage. For example, during guided discovery: ```text AUDIT ROUTE LIVE WORK / role, model, task +-> [-] Configured tools investigator / configured-model / 12s |-> [x] Unhinted discovery exploration:2 |-> [>] Guided research context_read: source evidence |-> [ ] Architecture + planning |-> [ ] Source review + investigations |-> [ ] Challenge / defend / judge |-> [ ] Follow-ups + synthesis |-> [ ] Proofs + verification ``` This is an illustrative layout, not a security result. The live map follows controller events. Unhinted discovery finishes before guided discovery begins. The follow-up stage includes enabled related-path investigations, capability composition, practice comparisons and grouping; those investigations can conduct further candidate assessments. Agents may request tools or experiments during discovery, before the final proof stage. | Marker | Meaning | | --- | --- | | `[ ]` | Stage has not been reached in this invocation. | | `[>]` | Controller is currently in this stage. | | `[x]` | Controller finished this stage, including any reused checkpoints or eligibility checks. | | `[-]` | Stage is disabled, has zero configured work, or has no selected candidates, as described by its event. | | `[!]` | The active stage stopped with an incomplete run. | A completed stage does not establish coverage, confirm a vulnerability or prove safety. Optional work inside a combined stage may be disabled or have no eligible candidates. Read the reports for exact coverage, deferred work and evidence limitations. No overall completion percentage is shown: follow-up work and proof revisions depend on what agents find. ## Counters, budgets and activity - **Model calls active** counts currently running model requests against the configured worker cap. Live work identifies roles, configured models, task IDs and available activity. Tool/test executions appear separately and are not constrained by this model-worker count. The display limits visible work rows and indicates overflow. - **Jobs done, pending and failed** come from saved job records, including context turns and preflight jobs. They are not counts of audited files or failed attempts. A successful retry replaces a failed job status; reservations remain. Pending counts only jobs already created, not all future work. - **Candidate decisions** counts distinct candidates with a recorded decision, including ignored or unresolved candidates. It is not a confirmed-vulnerability count. - **Calls, USD reserved and tokens reserved** use durable session accounting, including earlier invocations. Reservations are conservative and are not actual billing. `uncapped` means that particular cap is unset, not that all limits are absent. The first two model families are shown in sorted order; an overflow notice points to the report for additional families. - **Elapsed** measures this invocation. Time since the last event helps distinguish quiet calls from ongoing activity; it is not a provider heartbeat or a diagnosis of a stalled process. - **Dispatch blocked** remains visible after the event scrolls away. An unresolved-proof notice records a recent evidence limitation. These are not an exhaustive issue list; consult the report. The display refreshes four times per second and reads saved counters about once per second. Short jobs can finish between refreshes; their events and durable totals remain. Counters and the event stream can briefly differ while work is being saved. If a snapshot cannot be read, the dashboard retains its last values and labels them stale. Resizing is detected on refresh. Terminal controls are filtered; non-ASCII text is escaped to preserve layout. ## Stopping, resuming and reports Ctrl-C interrupts work. Katarina preserves committed results and exports partial reports when possible. On exit, it restores the terminal and prints the session outcome, job/decision counts and report directory. Use the startup resume command with `--tui` added to continue. A resumed map traverses the stages again as the engine reuses checkpoints; saved counts and reservations do not reset. In-flight calls may have been billed even if their results were lost. This is a read-only dashboard: it does not capture keyboard input, approve actions or provide a shell. The existing Ctrl-C handler remains responsible for cancellation. After analysis, the status changes to report export. See [reports] for evidence and [configuration] for execution controls. With runner `none`, requested proof plans can be saved but are not executed. To try the interface from a source checkout without paid model calls: ```sh katarina start --config examples/demo.yaml --state /tmp/katarina-tui-demo --tui examples/solidity ``` Demo mode is explicitly labeled synthetic and performs no security analysis. Its short runtime may show only the initial and final frames.
Reviewing a Solidity codebase with Katarina
# Reviewing a Solidity codebase with Katarina
This guide describes the current source tree, checked against the implementation on 16 October 2026. Start here for an end-to-end review; use the linked reference guides for individual features. Existing configurations are not automatically upgraded, and an older packaged executable may not include newer commands. Check `katarina help`, `katarina version` and the package's `BUILD.json`; build the current source when testing the latest additions.
Katarina combines independent discovery, guided security/economic investigation, adversarial review and optional execution. A completed run is an evidence package for developers and auditors. It is not a certificate, exhaustive attack search or demonstrated reduction in audit cost.
## What happens with a fresh init configuration
These are the settings written by `katarina init`, not the behavior of every older YAML file. The effective configuration is saved with each session.
| Stage | What Katarina does | What the result establishes |
|---|---|---|
| Inventory | Hashes included text, splits it into numbered chunks and records excluded files/directories. Includes off-chain code in the selected root if it passes the same inclusion rules. | Which source was supplied and what was omitted; not deployed bytecode equivalence. |
| Independent discovery | Runs **two of six** scenario investigators first. They choose hypotheses, reads, searches and permitted experiments without supplied attack families, peer findings or analyzer hints. | An opportunity for discovery outside our catalog; not independence from model training or biases. |
| Guided scenario review | Runs the other four investigators with all **20 economic/security families** assigned across them. Each family needs a cited investigation, justified inapplicability or an unresolved next step. | Accounted-for review obligations; not a guarantee that each family produced an executable test. |
| Architecture and further discovery | Builds source-cited system knowledge; plans up to eight additional investigations; scouts every included chunk twice, with an extra deeper scout on a deterministic 10% sample. | Source coverage and additional cross-file hypotheses within context and budget limits. The deeper sample is separate from the fully unhinted slots. |
| Candidate review | Independently challenges and defends each candidate, obtains a rebuttal, and assesses reachability, guards, impact, feasibility and deployment assumptions. | A reasoned `log`, `ignore` or `test` decision. Ignores remain reviewable; model agreement is not ground truth. |
| Expansion and comparison | Searches for related defects from up to four retained candidates; performs bounded capability-chain investigation; attempts up to four established-practice comparisons. | Additional candidates and explicit unfinished work. Practice research is unavailable until public research is enabled. |
| Proof and handoff | Groups suitable findings, generates permitted proof files when a command exists, optionally executes/reviews/revises them, and exports reports and an audit handoff. | The actual evidence and remaining gaps. A fresh init has **no test commands**, so it does not generate runnable proofs out of the box. |
The six scenario investigators are scheduled before shared architecture and ordinary scouting. Independent investigators finish before guided ones start. Guided agents can use the investigation ledger to share attempts, blockers and discoveries; independent investigations, deep scouts and blind reviews cannot read it. Own-task memory and repetition notices help agents avoid repeating unchanged work. These protections are enforced by the controller, but do not eliminate semantic duplication.
All stages share budgets. Fresh init allows 16 concurrent model workers and 1,000 model calls; it has no USD or per-family token cap until configured. A cap can interrupt later stages. Counts are limits or scheduled work, not promises of findings, executed tests or total model independence.
## What security questions it can pursue
Ordinary Solidity review includes authorization, state transitions, reentrancy/callbacks, arithmetic, upgradeability and cross-contract assumptions. Guided economic review additionally covers:
| Concern | Example experiment or obligation |
|---|---|
| Oracles, keepers and sequencers | Delay or stop observations and execution; test freshness, recovery windows, fallback assumptions and whether liquidation remains feasible. |
| On-chain/off-chain races | Check health at state S0, perform a valid intervening withdrawal/borrow/price change, and consume the original approval at S1. |
| Solvency and loss allocation | Combine price/depth shocks, withdrawals and delayed loss recognition; reconcile collateral, liabilities, insurance and socialized losses. |
| ADL, funding and market incentives | Test priority/account splitting, repeated or partial settlement, funding accrual and who bears losses when backstops run out. |
| Accounting and contribution | Cycle rounding, donations, shares, token transfers and rewards; track actual receipts and net profit across controlled accounts. |
| Roles and editable values | Follow privileged writers to consumers; test wrong units, extreme/coupled values, stale queued changes, lost authority and recovery. |
| Composed and external risks | Connect individually permitted actions across contracts/services; report code exposure to dependency failure even without a malicious actor. |
| Dependencies and deployed artifacts | Establish exact versions/forks, compiler settings, proxy implementation and runtime-code identity; keep missing facts unresolved. |
See the full [20-family catalog and coverage semantics], [operational/proof methodology] and [capability composition]. The catalog does not constrain what independent agents may investigate. Intentional governance power, accepted loss sharing or profitable ordinary trading is not automatically a defect; the finding must establish a violated property and concrete harm under stated assumptions.
## Prepare a usable first run
Use [the complete Solidity starter configuration], or run `katarina init` and edit its existing fields. Do not append duplicate YAML blocks. The starter keeps the current analysis stages, supplies a Foundry command for **generated-only** proofs, uses four workers, a 300-call cap and a 10M-token `deepseek` family cap. These are editable bounds for a first run, not a sizing estimate; a large project may exhaust them before completion. Model IDs are copied from the current init example; select models available to your account and set current rates before using a USD cap.
1. Choose the source root and exact revision. Include relevant contracts, tests, build files, remappings, keeper/backend code and integration documentation. If an external service is absent, record that boundary rather than assuming it behaves correctly.
2. Check compiler/toolchain and dependencies. Fresh init excludes `lib/**`; the starter includes `lib/` so Foundry dependencies can be copied, at the cost of additional scouting. Inspect the result before spending. `node_modules` and other built-in dependency directories still need explicit `scan.dependency_paths`; an explicit exclusion wins over that selection. No dependencies are downloaded automatically.
3. Put questions and assumptions in source-controlled design documents and list existing included paths in `design_notes`. Useful facts include intended loss allocation, supported tokens, privileged roles, upgrade policy, oracle guarantees and emergency recovery. Put targeted hypotheses in `analysis.questions`. Reserve `scan.task_instructions` for universal scope boundaries: it reaches independent agents too, so attack hints there would compromise their neutrality.
4. Keep generated reports, prior audits and known-answer material outside the review root when assessing independent discovery. Not attaching them as hints does not prevent agents from reading them as ordinary included files. Supply public research only when that is an intended evaluation condition.
5. Configure credentials, review budgets and inspect the inventory before starting.
From a working directory **outside** the source root, save your edited configuration as `solidity-review.yaml`, then run:
```sh
katarina doctor --config solidity-review.yaml
katarina index --config solidity-review.yaml /path/to/project > inventory.json
katarina start --config solidity-review.yaml --state ./review-state --tui /path/to/project
```
Inspect `inventory.json` for missing `.sol` files, build inputs and unintended prior reports. Katarina does not automatically apply `.gitignore`. `doctor` reports configuration validity, credentials/pi status and a fixed list of optional executables on the controller. Its exit zero does not establish valid API credentials, successful Foundry compilation, SSH availability, remote toolchains or adequate coverage. Review its printed statuses and prepare the selected environment separately.
The starter's named test command allows the assessor to request proof generation. With `runner: none`, those plans are saved but not executed. Only switch the runner after preparing its toolchain and understanding the execution boundary.
## Enable capabilities deliberately
| Capability | Required configuration/setup | Default from fresh init |
|---|---|---|
| Bundled incident leads | `research.incidents: true`; investigators choose a hypothesis and lookup. The index is a discovery aid, not an exhaustive verified exploit corpus. | Enabled; disable for blind benchmark runs. |
| Web research and practice comparisons | `research.public: true`; add `research.search_url` for agent-chosen searches. Direct fetch works without search. | Public access disabled; practice comparisons therefore unavailable. |
| Git history / chain observations | `research.history: true` and/or operator-captured, SHA-256-pinned `research.chain_snapshots`. | Disabled/empty; no automatic RPC queries or mainnet fork. |
| Agent-selected static analysis | Prepared `tools` entries with `mode: agent`, plus positive `analysis.tool_requests`; optional version and project preflight commands. | No tools; request budget zero. |
| Mandatory analyzer pass | A configured preflight-mode tool runs before model discovery. Its output is withheld from initial unhinted context. | No tools. |
| Interactive MCP/JSON tools | Prepared adapter/server plus explicitly allowed read-only operations and schemas. | Not configured. |
| Semantic Solidity navigation | Configured, installed Solidity language server with a compatible project. | Not configured; built-in outlines and bounded text navigation remain available. |
| Dependency/advisory review | `analysis.dependency_audit`, resolved SBOM/advisory tools and selected dependency source as appropriate. | Specialized dependency guidance/tools disabled. Included dependency source still receives ordinary review. |
| Generated proof execution | Nonempty `tests.commands`, permitted new-file paths, prepared `local`, `ssh` or `ec2` runner. | Runner `none`, commands empty. |
| Generated simulation campaigns | A prepared campaign command named by `tests.simulation_command`; agent-generated project adapter/manifest. | Not configured. |
| Distributed architecture coverage | `analysis.distributed_systems: true`; existing six-slot allocation can cover 20 economic plus 12 distributed families. | Disabled. |
| EVMBench evaluation | Separate `katarina evmbench detect` workflow and prepared upstream sandbox. | Never part of a normal project audit. |
Tools are generic. Agents can research and propose a missing tool when public research is enabled, but proposals do not install it or authorize execution. Configure the chosen tool and start a new session. Ghidra adapters concern native binary dependencies; they do not automatically analyze EVM bytecode. See [tools], [interactive adapters], [dependencies] and [navigation].
For an existing Foundry project, the starter includes this generated-test contract:
```yaml
tests:
runner: none
max_iterations: 2
timeout_seconds: 180
max_output_bytes: 65536
allowed_paths: ["test/Katarina*.t.sol"]
commands:
foundry: [forge, test, --offline, --match-path, "test/Katarina*.t.sol", -vvv]
```
Adjust it to the project's real test layout and prepared Foundry version. The compiler and dependencies must already be available in the runner's clean environment; the normal user HOME/cache is not inherited. Confirm that generated tests will actually be discovered. A successful build or zero-test execution is not a proof. Generated files cannot overwrite the existing implementation or tests; prepare a test hook if the framework cannot discover added files.
`local` runs on the controller with its OS privileges. `ssh` runs tests on specified user-provided machines. `ec2` uses the prepared disposable AWS runner. **Selecting SSH/EC2 for tests does not move model workers, language servers or analyzer tools there.** Those remain controller-side unless their configured launcher supplies another execution environment. See [execution boundaries] and [SSH setup].
## What simulation adds today
The reusable runner executes explicit cases and seeds against a generated adapter. It records successful/reverted actions, assertion evidence, exact-decimal observations/estimates and ordered traces; separates property violations from failed execution; checks declared controls; and retains source bytes and inputs for replay. It supports local/SSH execution and serial trials per campaign. Independent investigators can invent their own scenarios using the same neutral interface.
It does not automatically construct a correct financial model from an ABI. The adapter must map actual project actions, initialization, external observations and accounting. Market prices/depth, oracle values and keeper delivery need distinct controls. LLMs propose strategies; simulation actors normally use explicit reproducible policies. No calibrated probabilities, automatic trace minimization, general production Solidity adapter or live market realism is claimed. The two shipped examples are synthetic economic/retry fixtures, not audited protocols. See [campaign setup and evidence].
Standalone campaign artifacts live in the chosen `--out` directory. During an audit, a nested campaign returns captured output through the existing experiment/proof record; arbitrary files in its temporary workspace are not automatically exported. Preserve the generated adapter/manifest, source revision and recorded evidence; run a standalone campaign when the full retained replay bundle is needed.
## Read the result and act on it
The CLI prints the session ID and exact report directory, for example `review-state/sessions/SESSION/`. Start with:
1. **`audit-handoff.md`:** retained candidates, suggested repairs, unresolved work and next evidence.
2. **`report.md` / `report.json`:** original findings, ignored candidates, debate, assumptions, external/operational exposure, practice comparisons and proof interpretations. Review important dismissals too.
3. **Coverage and `inventory.json`:** expected/completed jobs, excluded source, each family's review/execution status and incomplete/deferred work.
4. **Proof/observation artifacts:** generated files, actual command outcome, test discovery, assertion quality, healthy/repaired controls and remaining deployment assumptions. `report.sarif` supports code-scanning consumers; it is not uploaded automatically.
`log` retains a concern without selecting a final proof; `test` requests proof work; `ignore` records a reasoned dismissal. `passed` describes process exit, while `supports`, `refutes`, `inconclusive` or `revise` describes a separate model interpretation. A family marked `investigated`, a campaign marked `completed`, and an audit process exiting zero each mean something narrower than “secure.” Practice comparisons provide context without lowering severity simply because a design is common.
Give auditors the handoff, full reports, exact source/configuration, generated tests and unresolved assumptions. Verify the proposed defect and controls, implement repairs through your normal development process, and start a new session on the changed code. Katarina does not automatically patch production contracts or measure money saved. Keep old artifacts for comparison.
## Recover or resolve a blocked run
```sh
katarina sessions --state ./review-state
katarina resume --config solidity-review.yaml --state ./review-state SESSION
katarina report --state ./review-state SESSION
```
| Symptom | What to check / do |
|---|---|
| No generated tests | Configure a command and valid new-file paths; inspect whether any findings were selected for `test`. A `log`/`ignore` decision does not generate a final proof. |
| No executed scenarios | Check runner `none`, missing commands, action budgets and family execution labels. Assignment alone does not schedule a guaranteed test. |
| Compiler/dependency failure | Inspect the actual copied inputs, remappings, compiler version and clean runner HOME/cache. Prepare missing dependencies outside the audit, then use a new session if source/config changes. |
| No historical/public/SOTA evidence | Distinguish the enabled local incident index from disabled public access, absent search endpoint and exhausted request budgets. |
| Analyzer did not run | Check tool mode/request limits, discovery results, preflight outcome and cached/indeterminate state. Test-runner selection does not relocate tools. |
| No SSH connection or unknown outcome | Verify host/key/known-hosts paths and the remote binary/toolchain. Inspect the remote environment before manually starting a fresh attempt; the controller will not retry ambiguous execution. |
| Budget exhausted or partial report | Inspect completion and deferred work. Resume only with compatible source/config/budget; increasing limits requires a new session. |
| Updated code or configuration rejected on resume | Expected: source, effective configuration and policy identity are pinned. Start a new session for the changed inputs. |
| Hard-killed process left stale exports | Regenerate committed reports with `report`; missing in-flight execution results remain indeterminate. |
Public research can affect independence, generated code needs an appropriate execution environment, and optional toolchains need preparation. These are visible configuration choices, not hidden prerequisites for ordinary source review. The separate [EVMBench guide] explains Detect setup and scoring limits; no official score has been established.
Download and install
# Download and install The current download is **0.1.0-preview.1**, an unsigned development preview. The executable includes pi through FFI and embedded SQLite. Running Katarina itself needs no Go, Rust, Python or database server. Project compilers, test frameworks and optional analyzers/language servers are installed separately. Repository documentation may describe capabilities added after a preview was packaged. Check the package's `BUILD.json` and bundled documentation, plus `katarina help`, before following newer simulation/SSH/EVMBench examples. Build the current source to test changes that have not been repackaged. ## Choose a download | Download | Platform and contents | |---|---| | [Linux x86_64 binary archive] | Native pi-linked executable, manual, schemas, examples and dependency notices. Built on Linux x86_64 with glibc 2.35; use Ubuntu 22.04 or a compatible newer glibc distribution. | | [Source archive] | Source snapshot, locked dependency manifests, schemas and website sources. Compilers and dependency downloads are needed to build it. | | [SHA-256 checksums] | Checksums of the downloadable archives. | `amd64` means x86_64, including Intel and AMD processors. This Linux binary does not run on macOS or ARM Linux. On Windows, use an x86_64 Linux environment under WSL. Native macOS archives are not included in this upload; the macOS instructions below apply when a matching native archive is published or provided by the maintainer. See [building from source] for other platforms. These downloads are previews, not a claim that live model providers, AWS execution or security-detection quality have been validated. The source archive corresponds to the packaged source snapshot; its build manifest records the base Git revision, source digest and any working-tree changes. ## Verify and extract on Linux Download both files into a new directory: ```sh curl -fLO https://katarina.fyi/downloads/katarina-0.1.0-preview.1-linux-amd64.tar.gz curl -fLO https://katarina.fyi/downloads/SHA256SUMS sha256sum --check --ignore-missing SHA256SUMS tar -xzf katarina-0.1.0-preview.1-linux-amd64.tar.gz cd katarina-0.1.0-preview.1-linux-amd64 ./katarina version ``` Confirm the archive's checksum reports `OK` before extracting. A checksum detects a changed or incomplete download; an unsigned checksum from the same website does not independently authenticate the publisher. `version` should report `0.1.0-preview.1` and `pi FFI linked: true`. The archive preserves executable permissions; if they were lost during copying, use `chmod +x ./katarina`. Install without administrator privileges, keeping the rest of the extracted archive for its documentation and notices: ```sh mkdir -p "$HOME/.local/bin" cp ./katarina "$HOME/.local/bin/katarina" export PATH="$HOME/.local/bin:$PATH" katarina version ``` Add the PATH export to the startup file used by your shell, such as `~/.bashrc` or `~/.zshrc`, if it is not already present. An `Exec format error` usually means the archive targets the wrong OS or CPU. A `GLIBC_... not found` error requires a compatible Linux distribution or a build on your target system; do not replace the system C library to install Katarina. ## First review after installation From a directory where you want to keep the configuration: ```sh katarina init # Set DEEPSEEK_API_KEY in your environment, or configure credentials_file. katarina doctor katarina start --tui ./your-project ``` The default configuration selects DeepSeek models. Edit `katarina.yaml` to select other providers/models, configure family budgets, or enable test execution. Use a private credentials file or environment variables for keys. See [configuration] and [the first-review guide]. Test execution is off until an execution runner is selected; configured test commands are required even for generated-only test plans. ## macOS downloads and Gatekeeper A native macOS archive must match the Mac: `darwin-arm64` for Apple silicon, `darwin-amd64` for Intel. Check with `uname -m`. Verify the archive's SHA-256 with `shasum -a 256 ARCHIVE.tar.gz` and compare it with the matching entry in `SHA256SUMS`, then extract it and try `./katarina version`. No macOS signing or notarization is claimed for this preview. For a trusted, verified native download blocked as an unidentified developer, first attempt to open it, then use **System Settings → Privacy & Security → Open Anyway** and confirm. This grants an exception for that program. Apple describes the current process in [Safely open apps on your Mac]. For a command-line executable where the normal exception is unavailable, inspect the exact extracted file: ```sh xattr -l ./katarina ``` If it has `com.apple.quarantine`, and you have verified the source and download and deliberately accept running this unsigned executable, remove only that file's quarantine attribute: ```sh xattr -d com.apple.quarantine ./katarina ./katarina version ``` Do not disable Gatekeeper globally or recursively remove quarantine from the Downloads directory. An alert that the file contains malware, will damage the computer, or is damaged calls for investigation and a fresh verified download, not a quarantine workaround. On managed Macs, follow the organization's software policy. Install the verified executable in `~/.local/bin` using the commands above.
Katarina product specification
# Katarina product specification This document describes the implemented pre-release product as of 16 October 2026. It defines scope and observable behavior; it is not a claim of release readiness or measured security effectiveness. [Behavior and definitions] provides stable behavioral requirements, and [architecture] explains components, protocols and data flow. | Contract | Current value | |---|---| | Application version default | `0.1.0-dev`; release builds can override it | | Configuration version | `1` | | Report schema version | `1.12.0` | | SQLite storage version | `1`, with additive tables | | Review policy | `15-interactive-tools` | | Agent runtime | Statically linked `pi_agent_rust 0.3.0` through a Rust C ABI bridge | | Application implementation | Go controller, CLI, providers, workers, persistence, navigation, runners, TUI and reports | For a concrete user journey and a complete configuration, see the [Solidity workflow]. This describes the current checkout, not an assurance that an older downloadable preview contains every feature. Version values are defined in [the CLI], [configuration], [models], [store] and the [bridge package]. ## Purpose and scope Katarina reviews a local software repository, investigates security hypotheses with multiple model roles, records arguments and evidence, and optionally generates and executes tests. Its intended outcomes are better software security and less repetitive preparation and clarification during a human audit. Detection quality, comparison with other harnesses, and audit-cost savings require separate measurement. The review covers included UTF-8 text rather than a fixed extension allowlist. Solidity, Java and other backend code, Rust, and C/C++ have the following support: | Area | Implemented support | |---|---| | General source analysis | Numbered source chunks, repository outlines, bounded reads and literal search, optional analyzer output and design notes | | Solidity | Access/state/accounting review plus economic incentives, game theory, capital, payoff, MEV, oracle, liquidation, governance and griefing guidance | | Java/backend | Entry-point, tenant, authorization, data-flow, state and integration reasoning; optional language-server navigation | | Rust | Ownership, aliasing, lifetime, unsafe code, FFI and build-feature guidance; optional rust-analyzer | | C/C++ | Memory/lifetime, allocation units, arithmetic, ABI, build and concurrency guidance; optional clangd | | Test integration | Operator-configured commands for the repository's existing test framework, including Foundry, Go, JVM, Rust and native tests; local/SSH/EC2 execution | | Simulation | Generic seeded campaign runner, explicit project adapters, fresh trial workspaces, controls, observations and source/input replay; serial local/SSH trials | | Dependencies and tools | Resolved SBOM/advisory evidence, selected dependency source, pinned native-binary input and configured command/JSON/MCP adapters | | External evaluation | Separate EVMBench Detect/no-hint adapter and retained-finding exporter; upstream scoring validation remains pending | Go outlines use its parser. Other built-in outlines are heuristic. Optional language servers provide symbols, definitions and references; successful startup does not establish complete project indexing. Tools such as Slither, Semgrep, graph generators or search utilities can be configured as external commands. No particular optional analyzer or graph product is mandatory or automatically installed. Katarina does not implement live API/web pentesting, exploitation of deployed targets, autonomous production patches, formal whole-program verification, a game-theoretic equilibrium solver, live market feeds, or an auditor approval system. These are outside the current product contract. ## Distribution and execution modes The release build is one executable containing the Go application, embedded SQLite, the statically linked pi runtime, website/manual assets and CloudFormation template. It requires no database server, model-agent daemon, separate pi executable or Node/Python runtime for ordinary controller operation. Provider access, OS facilities and any selected project tools remain external dependencies. | Engine | Behavior | |---|---| | `pi` | Invokes pi through FFI inside each model worker; the Go provider adapter supplies the actual HTTP completion. Requires a pi-linked build. | | `direct` | Uses the same controller workflow and Go provider adapter without invoking pi. | | `demo` | Uses deterministic, explicitly synthetic fixture responses without paid model requests; it does not perform model security analysis. | Source builds need Go 1.24+, a C toolchain and the pinned Rust toolchain. Linux and macOS are intended host platforms; Windows controller locking is unsupported, so Windows usage requires a supported environment such as WSL. Platform builds and libc compatibility are separate release concerns. Optional compilers, test frameworks, analyzers and language servers are installed and configured by the operator. See [development]. ## Public interfaces Flags precede positional arguments. Successful commands return zero; reported command errors return nonzero. A review command does not use finding severity as a CI failure threshold: a completed review with high-severity findings can return zero. | Command | Observable purpose | |---|---| | `init` | Writes an annotated YAML configuration without overwriting an existing file; supports `--out`. | | `start PATH` | Loads configuration, inventories the repository, creates a session, runs the workflow and exports reports. | | `resume SESSION` | Reuses compatible committed work and retained budgets; refuses a different source inventory, effective configuration or review policy. | | `sessions` | Lists saved sessions in the selected state directory. | | `report SESSION` | Exports committed session data without performing new model analysis. | | `index PATH` | Emits the source inventory, including exclusions and chunk metadata. | | `search QUERY` | Searches included repository text using the built-in bounded literal search. | | `doctor` | Checks configuration, linked pi support, credential presence and optional executable availability; it is not a live-provider or project-indexing certification. | | `dependencies` | Reads a resolved CycloneDX/SPDX SBOM, reports graph/identity gaps and optionally queries OSV within explicit limits. | | `simulate run` / `simulate replay` | Executes a strict campaign manifest or replays a retained trial into a new evidence directory. | | `evmbench detect` / `evmbench export` | Runs the pinned Detect task in a prepared upstream environment or exports retained findings. Patch and Exploit are unsupported. | | `aws template` / `aws link` | Exports the stack YAML or creates a CloudFormation quick-create review URL; AWS requires a hosted S3 template endpoint. | | `aws cleanup SESSION` / `aws reap` | Performs explicit recovery cleanup or termination requests for expired tagged instances. | | `serve` | Serves the embedded static website and manual; defaults to `127.0.0.1:8787`. This is not a review-control API. | | `version` / `help` | Reports build/pi availability or command usage. | `worker` is an internal model subprocess entry point; `execution-worker` is a single-request execution protocol endpoint used over SSH. Neither is a public network service or ordinary interactive workflow. `start` defaults state to `PATH/.katarina`; saved-session commands default to `.katarina` in the current directory. The printed resume command preserves the selected state, configuration and limit overrides. `--tui` enables terminal progress when stderr is a terminal; otherwise progress is ordinary text. The [terminal dashboard] displays a controller-driven stage map, active model calls and execution tasks, saved job/decision counts, reserved budgets, elapsed time, blockers and recent events. Stage completion is not a security verdict. Counters refresh from durable state, including on resume. ## Configuration, credentials and limits Configuration is strict YAML: unknown fields, duplicate keys, multiple documents and invalid values are rejected. The controller loads it once. CLI `--engine`, `--max-agents` and repeatable `--token-budget FAMILY=AMOUNT` override the corresponding settings and are included in the effective session configuration. Providers are selected by configured name. Built-in transport kinds are `openrouter`, `anthropic`, `openai`, `deepseek` and `compatible`. Claude uses Messages; the others use text Chat Completions. `base_url` is an API root, with the appropriate completion path appended. HTTPS is required unless `allow_http: true`; redirects are refused. Arbitrary OAuth schemes, proprietary response shapes and every provider-specific parameter are not part of compatibility. Model credentials come from environment variables, a separate YAML credential file, or an inline provider key, in that precedence order. Credential-file keys are configured provider names; credential files require private permissions. AWS uses the AWS SDK credential chain independently. Only the provider key needed by a worker is sent over its anonymous protobuf pipe. API-key values are excluded from saved effective configuration and the configuration digest; known provider keys are redacted from recorded model/tool text. Redaction and filename exclusions are not general secret detection. New `init` files and omitted-field defaults differ deliberately for optional analysis: | Setting | New `init` configuration | When omitted from existing YAML | Bound / meaning | |---|---:|---:|---| | `scan.workers` | 16 | 16 | 1–64 concurrent model workers | | `scan.passes` | 2 | 2 | 1–8 baseline passes per included chunk | | `scan.scout_mode` | `specialized` | `specialized` | `specialized` or `focused` | | `scan.deep_percent` | 10 | 0 | 0–100 deterministic hash sample; explicit `deep_paths` also select chunks | | `analysis.shared_knowledge` | true | false | Architecture extraction before scouting | | `analysis.max_investigations` | 8 | 0 | 0–64 generated questions, additional to configured questions | | `analysis.evidence_checks` | true | false | Structured review, capability and applicability validation | | `analysis.grouping` | true | false | Conservative grouping after individual decisions | | `analysis.max_group_size` | 6 | 6 | 2–12 members per group | | `analysis.scenario_investigations` / `independent_percent` | 6 / 30 | 0 / 0 | Two independent slots first, then four guided slots in fresh init | | `analysis.scenario_coverage` | true | false | Accounts for 20 economic families when Solidity is included; 12 more with distributed review | | `analysis.experiment_requests` | 3 | 0 | Up to 16 per investigation, also bounded by context/action and global budgets | | `analysis.investigation_ledger` | true | false | Guided coordination; independent/deep/review roles cannot read peers | | `analysis.progress_monitor` / `working_memory` | true / true | false / false | Own-task repetition notices and bounded evidence memory | | `analysis.boundary_analysis` / `proof_quality` | true / true | false / false | Boundary reasoning and required proof-quality evidence | | `analysis.followup_investigations` / `practice_comparisons` | 4 / 4 | 0 / 0 | Bounded related searches and practice research; the latter needs public access | | `analysis.composition_investigations` / `composition_windows` | 4 / 4 | 0 / 0 | Post-discovery capability composition and extraction-window cap | | `analysis.tool_requests` | 0 | 0 | Agent-driven tools disabled until configured; preflight tools are separate | | `analysis.dependency_audit` / `distributed_systems` | false / false | false / false | Additional guided dependency and distributed-system review | | `research.incidents` / `research.public` | true / false | false / false | Local discovery index enabled by init; public retrieval opt-in | | `scan.task_instructions` | empty | empty | Up to 32 KiB of universal scope instructions, also visible to independent roles | | `scan.context_requests` | 3 | 3 | 0–12 extra navigation rounds for ordinary tasks | | `analysis.investigation_context_requests` | 8 | 8 | 0–64 extra rounds for additional questions | | `scan.max_calls` | 1,000 | 1,000 | Persisted session-wide model dispatch cap | | `scan.max_cost_usd` | 0 | 0 | Zero disables the USD reservation cap | | `scan.token_budgets` | empty | absent | Per-family caps; an absent family cap is unlimited under other limits | | `tests.runner` | `none` | `none` | `none`, `local`, `ssh` or `ec2` | | `tests.simulation_command` | empty | empty | Names a configured command; supplies the generic campaign schema to investigators/test writers | | `tests.max_iterations` | 2 | 2 | 1–5 plans/executions per finding or shared group | | `tests.commands` | empty | empty | No test disposition until a command is configured | Initial defaults also include 16,000-byte chunks, an 8 MiB file-size limit, 64,000-byte source/context budgets, 4,096 output tokens, 180-second model and test timeouts, two completion attempts per unfinished job per invocation, and 65,536 bytes of captured test output. Context budgets bound individual context collections; they are not a cap on total process memory or the complete prompt with instructions and all evidence blocks. The full accepted ranges and path defaults are specified by [configuration], [the generated example] and [validation code]. Family names are explicit `agents.ROLE.family` labels; without one, the exact model ID is its family. No provider-to-family inference is performed. YAML and CLI accept positive integer counts or decimal K/M/B/T suffixes, case-insensitively, including `100M`, `1B` and `1.5B`. Expansion must yield a whole token count in 1 through 2^60. Equivalent spellings normalize to the same persisted count and digest. Before each dispatch, including navigation and retries, SQLite atomically reserves a call, family tokens and the configured USD estimate. Token reservation is `system bytes + prompt bytes + 1024 + max_output_tokens`. Reservations are never refunded. USD limits require configured positive model rates; AWS and external-tool costs are separate. These limits control dispatch, not exact tokenization or provider invoices. Exhaustion stops new dependent work and leaves the session incomplete; the controller does not silently switch models or skip the failed stage. ## Source inventory and navigation Inventory traverses the local filesystem independently of Git. It records included/excluded paths, sizes, source hashes, line counts, outlines and reasons for exclusions. It does not automatically apply `.gitignore`. Built-in credential filenames, dependency/state/metadata directories, nonregular files and symlinks, non-UTF-8/binary content, configured exclusions, oversized files and files containing a line beyond the chunk limit are excluded. An excluded directory has one entry rather than entries for all descendants. Included text is partitioned into numbered chunks, with five-line overlap where possible. Every baseline pass schedules every included chunk. Primary chunk space is reserved before supplementary shared knowledge and design/tool context. That is a source-supply property, not a guarantee that the model understood every line. Cross-file context and question starting windows remain bounded. No reviewable chunks is a visible error. Agents request included-file line reads, literal searches and optional LSP symbols/definitions/references through typed YAML context requests. Each request allows at most 16 combined operations; a read spans at most 1,001 lines and a search returns at most 30 matches. Context requests cannot fetch URLs, install tools, invoke arbitrary shell commands or read outside the included inventory. Separate opt-in research/tool actions allow bounded public documentation retrieval, named operator-configured execution and non-executing setup proposals; see [agent-selected tools]. Configured tools and language servers run against disposable copies and may themselves have host or network effects. ## Analysis and decision workflow The following order describes a successful configured workflow. Optional stages are omitted only when disabled or when no eligible work exists; a stage failure is not converted into an empty successful result. 1. **Preparation:** validate configuration/budgets, lock state, inventory source, create/recover the session, initialize optional navigation, capture configured preflight analyzer output and load included design notes. 2. **Independent then guided exploration:** run the reserved neutral investigations first, then guided investigations. When coverage is enabled, assign all applicable catalog families and require cited accounting. Investigators may choose bounded research and experiments; recorded evidence survives into later review. Initial unhinted prompts exclude supplied taxonomy, shared findings and analyzer/design hints. 3. **Shared knowledge, when enabled:** one architect job per chunk extracts source-cited component, boundary, actor, asset, invariant or dependency claims. Claims are challengeable interpretations, bound to the source digest. 4. **Question planning:** an optional planner proposes up to the generated-question cap; up to 32 configured questions are additional. Target files and knowledge references are validated; unmatched or invalid targets fail visibly. 5. **Scouting and investigation:** baseline passes cover every included chunk; selected deeper scouts and additional question investigators share the bounded worker pool. Cheap scouts and planners do not gate ordinary coverage or the deeper sample. Deeper scouts receive no shared model claims or earlier scout findings, but are not the separate fully unhinted exploration slots. 6. **Candidate accounting:** collect exploratory, scout and question findings; assign fingerprints from path, start line, CWE and normalized title; attach recorded investigation evidence. This is deterministic deduplication, not exhaustive semantic matching. 7. **Debate and assessment:** independent challenger/defender answers precede the defender's rebuttal. The judge receives the candidate, source and arguments and chooses `log`, `ignore` or `test`, retaining rationale, severity, confidence, assumptions and applicable structured evidence. Ignores remain inspectable; `by_design` requires evidence. 8. **Related-defect searches:** when enabled, investigate bounded related instances from retained candidates and independently assess new candidates. This is one generation, not an unbounded follow-up swarm. 9. **Capability composition:** when enabled, extract and connect source-grounded prerequisites/capabilities after discovery. Investigate bounded proposed chains and assess new findings; record deferred extraction and chain work. 10. **Established-practice research:** compare eligible retained findings against fetched primary evidence when configured. Unavailable/unfinished comparisons remain visible; they do not lower severity or alter dispositions because a design is common. 11. **Grouping and proofs:** propose bounded groups while preserving individual decisions. Only members individually selected for `test` share a proof. Generate allowed new files, optionally execute, review actual evidence and permit bounded meaningful revisions. Early exploratory experiments can already have run in step 2. 12. **Export:** save completion and export committed findings, observations, lineage, collaboration, coverage, tests and the developer handoff. Handled errors/cancellation leave an incomplete session and attempt export; hard kills can leave exports stale. Models are independently configurable per role. Architect, investigator and capability mapper inherit the complete scout model/family/rate entry unless overridden; planner, grouper and chain planner inherit judge. Deeper scouting requires its own configured role when enabled. An optional `proof_reviewer` overrides the judge model for execution interpretation. Separate role names do not promise different underlying models or statistically independent judgments. ### Structured evidence and economic analysis With evidence checks enabled, challenge, defense, rebuttal and assessment must address reachability, control, guards, invariant, impact and feasibility. Findings with structured `economics` additionally require incentives and capital. Unknown checks require `next_evidence`; other outcomes require source citations. Invariant, impact, incentives and capital cannot be waived as inapplicable. The host checks cited paths, line ranges and exact quotation matches. A citation spans at most 41 lines and 4,096 quote bytes. It does not prove that the quote entails the claim. A supporting review cannot contain unknown or refuted checks; a refuting review needs a refuted check. A supported assessor verdict requires resolved checks, meaningful additional capability and applicable/conditional deployment. An ignore requires a refuted verdict supported by a refuted obligation or inapplicability, even when behavior is intended. Capability analysis separates existing authority from additional access, control, profit or harm, the crossed boundary/invariant and economic effects. Applicability records deployment/build/integration conditions. Permission to act does not establish that resulting economic harm is accepted. Solidity guidance asks for feasible strategies, incentives, capital, net payoffs, griefing costs and sensitivity to assumptions; economic findings need not have a CWE. These are model reasoning requirements with structural guards, not a formal economic proof. ## Test generation and execution The writer selects an operator-configured command key and creates new files matching allowed paths. It cannot supply new executable arguments, overwrite inventoried implementation/tests, traverse paths, create hidden/credential paths or exceed twelve files and 256 KiB of generated content. Plans are saved under `tests/FINDING_ID/attempt-N/` or `tests/GROUP_ID/attempt-N/`. Execution copies only included files, verifies their hashes, and applies the new files in a disposable workspace. `none` saves requested plans without execution or proof review; a command must be configured for the assessor to select a final test disposition. `local` runs the command with the operator's OS privileges, a private HOME, reduced environment, timeout, bounded output and process-group cleanup. This is not an OS sandbox. `ec2` uses an operator-prepared image, private S3 transfer and SSM to execute on a disposable host as an unprivileged test user in a separate network namespace. `ssh` transfers the validated source/test bundle to an operator-configured machine and runs a same-binary worker in a fresh workspace with strict host-key checks, bounded output and a remote deadline. SSH does not itself provide OS/network isolation. Selecting an execution runner authorizes configured tests without a per-test confirmation prompt. It does not move analyzer tools, LSP servers or model workers off the controller. Execution status and security interpretation are separate. `passed` means exit zero; `failed` may be an assertion or setup failure. `error`, `timeout`, `indeterminate` and truncated evidence cannot yield a definitive supports/refutes interpretation. A reviewer can request revision only after completed passed/failed execution, with a concrete request. Revisions cannot repeat any earlier plan's command and file contents, including A → B → A cycles. An indeterminate attempt is never automatically rerun. Shared plans must map every member to an assertion excerpt in a generated file. Shared proof reviews must interpret every member separately; a group may support one and leave another inconclusive. Overall supports/refutes requires all member interpretations to agree. Assertion presence is checked by the host; meaningful execution and semantic adequacy still require review. Production repairs and repaired-version negative controls are not automatically generated/executed by this workflow. Proof scopes execute sequentially in the current controller, even when multiple test candidates exist. The model-worker limit is a maximum, not a promise that every stage or test runs that many tasks at once. ## AWS and infrastructure The included CloudFormation template creates network resources, an encrypted private artifact bucket, instance permissions/profile and an operator role. The website also distributes the unchanged YAML. Quick-create links preload a template from its S3 HTTPS endpoint; a custom website URL alone is not a supported CloudFormation template source. They do not issue access keys in one click, supply an AMI or eliminate AWS IAM approval. The controller uses the AWS SDK; the prepared remote image supplies AWS CLI/SSM and test tools. Each remote attempt records a resource intent and idempotent EC2 client token before launch, uses ownership/expiry tags and an in-instance shutdown timer, and requests instance termination and source-object deletion on completion/error/cancellation. Ambiguous SSM submission is not automatically repeated. Cleanup/reap commands and resume cleanup handle recoverable leftovers. Cleanup errors remain visible. TTL and termination requests are safeguards, not guaranteed deletion during AWS outages or failed boot. Live AWS deployment validation remains pending. See [AWS setup and boundaries]. ## Persistence, reports and completion semantics SQLite in a private state directory is authoritative for sessions, jobs, reservations, findings, immutable analysis artifacts, test intents/results and cloud intents. It uses WAL, FULL synchronous writes, foreign keys and one database connection; an OS lock excludes concurrent controllers for that directory. No server-based database or worker-to-worker message bus is used. Accepted completed jobs are reused on compatible resume; unfinished jobs may be retried and billed again. Job records preserve the latest result/error, attempt count and accumulated usage, not every discarded retry response. Navigation completions have distinct persisted job IDs. Shared test evidence is checkpointed atomically for all members, and replaying earlier stages preserves later committed proof progress. A persisted test intent without a result remains indeterminate. Resume does not refund reservations or reset budgets. Reports are JSON, Markdown and SARIF 2.1.0, with inventory, event JSONL and conditional knowledge/question/group exports. JSON contracts use Draft 2020-12 schemas. Reports retain source/configuration identity, separate coverage counts, findings and ignores, evidence and assumptions, economic/capability analysis, groups, generated plans, test outcomes, model interpretations, usage/reservations, events and outstanding resources. SARIF preserves member findings and encodes locations as relative URIs; ignores are suppressions under review, not auditor approval. See [artifact contracts]. Each export file is written atomically; the complete set is not a single filesystem transaction. SQLite-backed report regeneration repairs stale exports after interruption. The inventory/configuration files provide the saved inputs needed by report export; SQLite alone is not a full copy of the source repository. Retain the exact source revision and session directory for audit handoff. Session `completed` means the scheduled workflow returned successfully, not that all security questions were resolved or all tests passed. It may include logged concerns, ignored findings, inconclusive proof reviews, unsuccessful test commands or an iteration limit. `incomplete` means orchestration stopped with an error or handled cancellation. A hard-killed process may leave `running` status until recovered; that status alone is not proof a controller is alive. ## Release boundaries and maintenance The static site uses monospace/ASCII-style presentation and a red high heel drawn with Unicode Braille characters. The embedded manual preserves text and diagram source with clickable links; Mermaid-capable Markdown viewers can render the architecture diagrams. No diagram-rendering service is required at runtime. Native preview downloads, the source snapshot and unsigned SHA-256 checksums are generated under the Git-ignored `web/downloads/` directory. Archives include documentation, schemas, source/build identity and dependency notices. The current prepared binary targets Linux x86_64; native macOS binary/signing validation is separate release work. Download archives are hosted externally and are not embedded inside the binary. Automated checks cover orchestration, budgets, exact amount parsing, evidence shapes/provenance, source coverage, recovery, protobuf/FFI boundaries, provider response handling, local runners, SARIF locations and mocked AWS lifecycles. They do not establish parity with Claude Code, MDASH or Shannon, live-provider reliability, live AWS correctness, complete language-server indexing, detection recall or audit savings. Detection recall, false alarms, evidence validity and audit savings are measured separately by [the benchmark], which ships in `benchmark/` as its own module and is not part of this product contract. The remaining evaluation/release work has a procedure in [development] and [research design]. Changes to observable workflow must update this specification, the relevant behavior IDs, architecture, configuration/examples and report contracts together. Changes to review semantics must also review the policy digest boundary; changing documentation alone does not change the policy. Behavior IDs are stable references for issues, tests and release notes. ## Simulation and evaluation boundaries [Simulation campaigns] are a separate reusable execution layer. A strict manifest selects explicit source/adapter files, seeded cases, expected control behavior and time/output limits. The adapter invokes real project code and returns structured actions, assertions, measurements and traces. The controller retains source/manifest/request identity and replay artifacts; missing meaningful actions, malformed output, truncation and execution failures remain inconclusive. A completed campaign means its planned trials were attempted, not that its properties held. Calibration, general production financial adapters and automatic trace minimization remain unimplemented. Nested audit campaigns retain generated files and captured output; standalone campaigns retain their full replay bundle. [EVMBench Detect] uses a distinct launcher with pinned task instructions and an incremental exporter that includes only `log`/`test` findings. It rejects external research and remote test execution for the supported source-only/no-hint track. The upstream sandbox and grader remain external prerequisites. Official scores, live SSH deployments and production economic-model accuracy have not been validated by the implementation tests. Patch and Exploit need separate workflows; simulation results are not added to an official Detect score.
Katarina behavior and definitions
# Katarina behavior and definitions This is the behavioral contract for the current product described in [the specification]. It defines terms, desired behaviors (`b01`, `b02`, …), and undesirable behaviors (`ub01`, `ub02`, …). Use these IDs in issues, tests, evaluation cases and release notes. IDs are stable: append new entries and retire obsolete ones explicitly rather than renumbering or reusing them. Each `ubNN` below is the failure counterpart of `bNN`. ## Interpretation and enforcement Desired behavior applies when the relevant feature is enabled and its documented prerequisites are met. An optional feature being disabled is not itself a defect. An undesirable behavior is something the implementation, model reasoning or product claims should avoid; listing it does not assert that every instance is mechanically detectable. | Label | Meaning | |---|---| | **Host** | Enforced by controller logic, data validation, operating-system/process boundaries or persistence rules. Tests can check the stated observable property. | | **Model** | Required by role instructions and assessed by review/evaluation. The controller may enforce structure and consistency without establishing semantic truth. | | **Operator** | Requires supplied scope, credentials, commands, dependencies, deployment assumptions, human judgment or infrastructure operation. | Several behaviors combine these labels. For example, exact quotation matching is Host-enforced; whether that quote proves an authorization bypass is a Model/Operator judgment. A valid schema, passing command, high confidence value or majority of agreeing agents is not independent vulnerability confirmation. ## Definitions | Term | Definition | |---|---| | Operator | The person or automation choosing the repository, configuration, providers, budget and permitted execution environment. | | Controller | The Go process that owns scheduling, scope, validation, budget reservations, authoritative state, runners and exports. | | Worker | A short-lived child invocation of the same executable, serving one protobuf request and one completion response. It does not own a database or peer message bus. | | Role | A review responsibility and model configuration, such as scout, challenger or judge. Two roles may use the same model. | | Task | A logical unit of work, potentially involving an initial completion and additional navigation completions. | | Job | A persisted completion slot identified within a session. Retries reuse the job ID; navigation rounds have their own job IDs. | | Attempt | Either a completion dispatch for an unfinished job or a numbered proof plan/execution. The two counters are separate. | | Session | A review bound to its root, inventory digest, effective configuration and review-policy digest, with durable results and reservations. | | Inventory | Included/excluded file metadata and included-source chunks. It records scope; it is not a call graph or a security verdict. | | Source snapshot | The source bytes represented by the inventory hashes. Source is held in memory for review and verified when copied for tools/tests; the saved inventory is not a complete source archive. | | Chunk | A bounded numbered source range used as a discovery seed. Adjacent chunks overlap where possible. | | Coverage | Counts of completed baseline, deeper, knowledge and planned-question jobs against their corresponding expected work. It measures workflow/source exposure, not defect recall. | | Independent review | Separate initial answers without access to the peer's answer. It does not imply different models or statistically independent errors. | | Shared knowledge | Session-scoped, source-cited model claims about components, actors, assets, boundaries, invariants and dependencies. Claims remain challengeable. | | Investigation | An additional configured or generated question with included starting files, selected shared claims, and a saved answer/unresolved obligations. | | Candidate / finding | A proposed defect with a location, claim, evidence, impact and other details. The term alone does not mean a confirmed vulnerability. | | Finding ID / fingerprint | A controller-derived identity based on location, CWE and normalized title. Exact fingerprint deduplication can coalesce discoveries; it is not complete root-cause classification. | | Assessed finding | A candidate with challenge, defense, rebuttal, disposition and optional structured assessment, group and proof history. | | Disposition | The judge's next action: retain the concern, retain a dismissal rationale, or request a test. It is distinct from a proof result. | | Citation | An included-file location and an exact source quotation. | | Provenance | Evidence that a quotation occurs in the claimed reviewed source range. Provenance does not establish semantic entailment or deployment truth. | | Evidence obligation / check | A question that must be addressed to support or defeat a claim, such as reachability, effective guards or economic feasibility. | | Invariant | A required safety, accounting, ownership, access or economic property. Comments and supplied design notes can describe it but are not automatically authoritative. | | Actor | A participant whose inputs, permissions, resources, incentives or timing matter to a claim. Economic actors need not act maliciously. | | Additional capability | Access, control, profit or imposed harm enabled by a mechanism beyond the actor's relevant existing authority. It includes economic effects, not only privilege escalation. | | Applicability | Whether a claim's build, deployment, integration and operating conditions hold, are conditional, are disproven or remain unknown. | | Economic risk | A harmful strategy, incentive failure, cost asymmetry or system response under stated capital, payoff, timing and operating assumptions, even if code follows its intended rules. | | By design | A model claim that behavior is intended, requiring explicit design evidence. It is not a synonym for safe, harmless or accepted by an auditor. | | Finding group | A proposal to validate multiple retained findings through common conditions and member-specific assertions. Group membership does not merge their verdicts. | | Test plan | A configured command key plus new generated files and an expected observation; a shared plan also identifies each member's assertion. | | Execution result | Recorded runner status, exit code, output, truncation, duration and runner type. | | Proof interpretation | A model's assessment of what a generated test and recorded execution establish about the claim. | | Proof of a defect | A scenario/assertion that succeeds in observing the defect and stops doing so after repair. It must exercise the real implementation and relevant trigger. | | Safety regression assertion | An assertion of the desired property: it should fail on the vulnerable implementation and pass after repair. | | Negative control | A repaired or deliberately non-triggering comparison demonstrating that the observed result depends on the claimed mechanism. Katarina does not automatically repair production code to create one. | | Model family | An explicit budget grouping shared across selected roles/models/providers; absent an explicit label, the exact model ID is used. | | Token budget | A cap on conservative input-plus-output reservations for a family in one session. `100M` means 100,000,000 reserved tokens. | | Reservation | Persisted dispatch allowance consumed before a request. It is not refunded after errors, unused output allowance or lost responses. | | Observed usage | Input/output token counts reported by a provider, or marked estimates when counts are unavailable. It is separate from reservations and invoices. | | Durable intent | A committed record made before a potentially externally effective operation such as test execution or instance launch. | | Indeterminate execution | An execution was recorded as started but has no committed outcome. It may have happened; automatically repeating it is unsafe. | | Complete workflow | Scheduled orchestration returned successfully. Findings, test failures, unresolved assumptions or inconclusive proofs can remain. | | Audit-ready evidence | Traceable source identity, scope, claims, arguments, assumptions and test artifacts suitable for human review. The label does not imply auditor acceptance or certification. | ## Status vocabularies These values belong to different objects and must not be substituted for one another. | Object | Values | Interpretation boundary | |---|---|---| | Session | `running`, `incomplete`, `completed` | A hard kill can leave `running`; completed is orchestration completion, not security approval. | | Job | `pending`, `running`, `failed`, `done` | Done means an accepted response is committed; it does not validate the model's conclusion as fact. | | Knowledge claim | `observed`, `inferred`, `unknown` | All are model-authored claims with source citations. | | Review position | `supports`, `refutes`, `uncertain` | The peer's position on the candidate. | | Evidence check | `established`, `refuted`, `unknown`, `not_applicable` | Established supports an obligation; refuted defeats it; unknown names next evidence. Inapplicability needs justification and is prohibited for core invariant/impact and economic incentive/capital checks. | | Evidence assessment | `supported`, `refuted`, `unresolved` | The assessor's structured evidence verdict, subject to consistency rules. | | Capability | `meaningful`, `exposure`, `equivalent`, `unknown` | Whether the mechanism adds relevant capability or harm; equivalence alone is insufficient to dismiss economic harm. | | Applicability | `applicable`, `conditional`, `not_applicable`, `unknown` | Whether the required operating conditions hold. | | Disposition | `log`, `ignore`, `test` | Log keeps a concern; ignore keeps a dismissal rationale; test requests a permitted plan. | | Severity | `critical`, `high`, `medium`, `low`, `info` | Model-assessed impact, distinct from evidence strength and probability. | | Execution | `passed`, `failed`, `error`, `timeout`, `indeterminate` | Command/runtime outcomes, not security verdicts. | | Proof interpretation | `supports`, `refutes`, `inconclusive`, `revise` | Revise requests another permitted, changed plan; it is not an instruction to repeat an unknown execution. | | Shared member interpretation | `supports`, `refutes`, `inconclusive` | One interpretation for each group member; revision is requested at the shared-plan level. | Confidence is a number from 0 to 1 supplied by a model. It is uncalibrated and is not an independently measured probability. ## Desired behavior | ID | Required behavior | Enforcement and observable acceptance | |---|---|---| | `b01` | Record the review scope explicitly, including exclusions and why content was omitted. Do not depend on a Git checkout or silently apply `.gitignore`. | **Host.** Inventory accounts for included files and exclusion entries; excluded directories may have one entry. | | `b02` | Supply every scheduled primary source chunk in full before allocating supplementary model/design/tool context. | **Host.** Complete numbered chunk text remains in the initial seed context even at supported tight context settings; coverage counts remain separate from understanding. | | `b03` | Run every baseline pass and the independently selected deeper sample regardless of whether cheap scouts return findings. | **Host.** A stronger scout can recover a case missed by ordinary scouts; the plan cannot reduce baseline expected jobs. | | `b04` | Honor context independence: deeper scouts receive no shared model claims or earlier scout conclusions; empty question knowledge references mean none. | **Host.** Prompt inspection verifies absence of unselected claims, including configured questions. Shared source/design notes are still permitted. | | `b05` | Preserve shared claims with source provenance and observed/inferred/unknown status; keep them challengeable. | **Host + Model.** Paths/ranges/quotes validate and host-assigned IDs persist; investigators must seek counterevidence rather than treat summaries as proof. | | `b06` | Run explicit/generated questions in addition to normal work, validate their included targets, and retain answers even when no finding results. | **Host.** Unmatched targets fail visibly; unresolved or unfinished questions are represented in saved answers/reports. | | `b07` | Bound navigation to included source and configured LSP operations, with explicit round/output limits and budget charges. | **Host.** Unavailable paths are not read; context exhaustion stops the task visibly; each completion consumes a reservation. | | `b08` | Obtain blind initial challenge and defense, then a rebuttal and an assessor decision using their arguments. | **Host + Model.** Initial peers cannot see one another's responses; reasoning should address the strongest alternative explanation. | | `b09` | When evidence checks are enabled, require complete obligations, cited resolved outcomes and specific next evidence for unknowns. | **Host + Model.** Unknown/refuted checks cannot produce support; refutation and ignores need the appropriate cited basis. Citation truth is assessed separately. | | `b10` | Include Solidity incentives, rational deviations, capital, net payoffs, cost asymmetry and operating assumptions. Preserve structured economic evidence when supplied. | **Model + Host.** Domain guidance reaches review stages; economic objects require their fields and additional incentive/capital checks. Economic adequacy requires evaluation. | | `b11` | Separate existing authority, additional capability/harm and deployment applicability from severity, confidence and disposition. | **Host + Model.** Structured assessment contains these fields; unknown conditions remain explicit and intended behavior alone does not justify dismissal. | | `b12` | Retain every distinct assessed finding and its disposition, including ignored findings and members of groups. | **Host.** Grouping does not delete findings or overwrite their individual severity/decision; exact fingerprint coalescing remains a separate discovery step. | | `b13` | Group only when a common scenario and assertions can address all members; reject unknown or overlapping membership. | **Host + Model.** IDs/size/citations validate; common mechanism and conditions require review. Uncertain or out-of-window matches remain separate. | | `b14` | Shared plans and proof reviews account for every member separately. Share execution only when every member was individually selected for testing. | **Host + Model.** Each plan maps an assertion excerpt to a generated file; each review has a member result. Overall support/refutation requires agreement. | | `b15` | Keep the reviewed implementation unchanged. Generate only permitted new test files and select only configured command keys. | **Host + Operator.** Reject traversal, forbidden/existing paths and new argv; run overlays in hash-checked disposable copies. Operators choose trusted commands. | | `b16` | Execute tests or create test instances only through an explicitly selected execution runner and configured commands. | **Host + Operator.** `runner: none` writes one plan and performs no test execution/review; `local`/`ssh`/`ec2` permits configured execution without a separate per-test prompt. | | `b17` | Distinguish command outcome from security evidence; inspect discovery, actual implementation reachability, assertion meaning and negative controls. | **Host + Model + Operator.** Incomplete/truncated execution cannot support/refute; semantic adequacy and repaired controls require independent review. | | `b18` | Bound revisions and reject a command/file-content plan already present in the same proof history. | **Host.** Description changes, file reordering and A → B → A cycles cannot authorize another identical execution. | | `b19` | Commit execution intent before launch and preserve unknown outcomes without automatic repetition. | **Host.** After interruption, a missing result becomes indeterminate and does not cause another dispatch for that attempt. | | `b20` | Reserve call, family-token and optional USD allowance atomically before each dispatch, including retries and navigation. Retain reservations across resume. | **Host.** Concurrent workers cannot race beyond the configured reservation caps; exhausted sessions stop rather than reset or silently skip work. | | `b21` | Parse token shorthand exactly, normalize equivalent amounts and keep family selection explicit. | **Host.** `100M`, `0.1B` and `100000000` have the same cap/digest; reject zero, overflow and fractional-token amounts. | | `b22` | Default to at most 16 simultaneous model workers, honor `--max-agents`/`scan.workers` within 1–64, and state what the limit covers. | **Host.** Worker peaks respect the cap; dependent/sequential stages may use fewer workers, and external compiler/LSP threads are separate. | | `b23` | Use the selected provider/model and documented optional-role inheritance, validate responses, and fail visibly on transport/refusal/truncation/schema errors. | **Host.** No automatic provider/model substitution occurs; completed responses use the configured API shape and role budget. | | `b24` | Keep keys out of argv and effective configuration, limit worker credentials to the selected provider, and redact known keys from recorded model/tool text. | **Host + Operator.** Credential precedence and private files work; reduced child environments do not inherit model/AWS secrets. Scope and embedded secret review remain operator duties. | | `b25` | Use the versioned protobuf child-pipe contract, bounded frames and matching job identity; keep workflow authority in the controller. | **Host.** Oversized/mismatched frames fail; model output does not select worker programs, database servers or a peer communication protocol. | | `b26` | Make committed SQLite state authoritative, retain accepted work and use atomic writes for exported files and shared member proof checkpoints. | **Host.** Reopening/replay preserves committed evidence; a stopped earlier stage cannot erase a later committed proof. Export files can be regenerated from saved session inputs/state. | | `b27` | Resume only with matching inventory, effective configuration and review policy; reuse completed jobs and allow key rotation. | **Host + Operator.** Source/model/budget/policy changes are rejected; equivalent budget notation and credential changes preserve compatible session identity. | | `b28` | Report completion, omissions, failures, uncertainty, reservations and outstanding resources honestly, and attempt export on handled interruption. | **Host + Operator.** Incomplete orchestration is not labeled a successful scan; a completed workflow may still have unresolved findings or failed tests. Hard-kill staleness is documented. | | `b29` | Record cloud intent before launch, use client tokens/expiry tags, request termination and object cleanup, and expose recovery failures. | **Host + Operator.** Mock lifecycle/recovery tests pass; operators verify AWS permissions/AMI, monitor leftovers and validate live behavior. TTL is not a deletion guarantee. | | `b30` | Describe execution boundaries accurately and keep optional tools optional. | **Host + Operator.** Ordinary review needs no separate agent/database service; local execution is labeled as using host privileges, and external toolchains/AMI dependencies are explicit. | | `b31` | Maintain accurate standalone documentation, runnable state-path examples, versioned artifact contracts and optional terminal progress. | **Host + Operator.** Generated manual matches source, links/defaults agree with code, schemas accept representative complete/partial outputs, and non-TUI usage works. | | `b32` | Make claims about readiness, effectiveness and audit savings only with appropriate evidence; label demonstration output clearly. | **Host + Model + Operator.** Demo is identified as synthetic; orchestration tests are not advertised as discovery recall, auditor approval or live AWS validation. | ## Undesirable behavior | ID | Failure to avoid | Concrete example / consequence | |---|---|---| | `ub01` | Hide excluded content or present the filesystem review as exhaustive without scope accounting. | A skipped dependency or oversized Solidity file disappears from the audit handoff. | | `ub02` | Let shared summaries/tool output displace primary lines while reporting the chunk as reviewed. | Tight context settings omit a line between overlap windows. | | `ub03` | Gate ordinary/deeper discovery on a cheap model flag or a planner's chosen files. | A cheap-scout false negative prevents every later agent from examining the mechanism. | | `ub04` | Interpret empty knowledge references as all knowledge, or leak earlier conclusions into independent deeper scouting. | An intended fresh look inherits the same mistaken trust assumption. | | `ub05` | Treat generated architecture claims, comments or matching quotes as authoritative safety facts. | A cited comment stating “trusted caller” substitutes for checking actual callers. | | `ub06` | Replace baseline work with targeted questions, silently drop invalid questions or require a finding from every question. | An unmatched configured path appears as a completed investigation with no concerns. | | `ub07` | Follow source-embedded instructions to fetch URLs, expose excluded files, install tools or execute arbitrary commands. | A repository comment attempts to redirect an investigator outside the reviewed inventory. Host tool restrictions limit effects; prompt compliance still requires evaluation. | | `ub08` | Expose one initial peer answer to the other or treat agreement as a vote that establishes truth. | The defender parrots the challenger instead of independently checking counterevidence. | | `ub09` | Convert unknown evidence into refutation/support, omit required obligations or accept invented source quotations. | Missing deployment evidence becomes a definitive “not exploitable” dismissal. | | `ub10` | Dismiss economic or incentive risk because code follows its specification or participation is permissionless. | Unprofitable liquidation remains “by design” while bad debt accumulates. A semantic miss may pass structural validation and must be caught by evaluation. | | `ub11` | Equate permission to act with accepted permission to impose losses, or invent operating assumptions. | An authorized withdrawal or governance vote is assumed harmless without examining induced losses or capital/timing. | | `ub12` | Delete ignored/grouped findings or overwrite all members with one disposition. | Auditors cannot inspect the original location or challenge the dismissal rationale. | | `ub13` | Group findings solely by similar names/files, conflicting prerequisites or unrecognized IDs. | Distinct bugs receive one insufficient shared scenario. Semantic grouping errors require review in addition to ID validation. | | `ub14` | Treat one passing assertion as proof for every group member, omit members or silently weaken their claims during revision. | One discovered test passes while another member's test is skipped but both receive support. | | `ub15` | Overwrite production/existing tests, accept model-supplied argv or mutate the original repository through the overlay mechanism. | A generated plan changes the guard rather than testing the reviewed implementation. | | `ub16` | Run generated code or launch an instance with `runner: none`, or imply that selecting an execution runner still waits for per-test approval. | A normal analysis unexpectedly incurs cloud execution, or an operator misunderstands configured automatic execution. | | `ub17` | Call exit zero, a compilation error, missing dependencies or zero discovered tests a reproduced or refuted vulnerability. | Setup failure is mistaken for evidence that the proposed defect is impossible. | | `ub18` | Repeat unchanged proof content through description edits, file reordering or nonconsecutive revision cycles. | A → B → A spends again without a new scenario under the same source/configuration. | | `ub19` | Automatically retry a started attempt whose outcome was lost or an ambiguous SSH/SSM submission. | An external action happens twice after a controller crash. | | `ub20` | Dispatch before reserving, reset/refund uncertainty on resume, or bypass a cap by silently switching families/models. | Several agents independently consume the same remaining allowance. | | `ub21` | Use binary suffix multipliers, floating-point rounding or guessed family membership. | `1B` changes across input paths or a fractional token rounds into an accepted cap. | | `ub22` | Exceed the configured worker cap or claim it constrains all child-tool threads and test parallelism. | The TUI worker count is mistaken for a total CPU/process limit. | | `ub23` | Accept incomplete/refused provider text as a clean result, follow redirects with credentials, or silently reroute a request. | An endpoint error becomes an empty findings list or consumes a different family's allowance. | | `ub24` | Put keys in arguments/reports, give a worker unrelated provider/AWS credentials, or promise universal secret filtering. | Embedded credentials in arbitrary source are assumed protected by a filename blacklist. | | `ub25` | Replace typed child messages with an unvalidated peer bus, ambient worker database or model-controlled process launcher. | A worker accepts an unrelated response or interprets source content as a transport command. | | `ub26` | Treat stale JSON exports as authoritative state, lose later proof progress during replay, or claim all retry responses are archived. | A resumed early assessment erases previously committed shared test results. | | `ub27` | Reuse results after source/configuration/policy changes, or force a new session solely because an equivalent cap spelling or API key changed. | Earlier truncated-context jobs are presented as having used the corrected coverage policy. | | `ub28` | Conflate an empty report, a completed workflow, successful tests and secure software, or hide export/cleanup failures. | A budget-exhausted run is presented as “no vulnerabilities found.” | | `ub29` | Promise guaranteed EC2 deletion, retry ambiguous execution or describe the stack link as issuing credentials and a ready test AMI. | A failed shutdown or incomplete AWS setup becomes an unreported operational assumption. | | `ub30` | Describe local execution as an OS sandbox, make optional analyzers mandatory without disclosure, or conflate one binary with bundled project toolchains. | An operator runs untrusted build code expecting host isolation that is not implemented. | | `ub31` | Ship stale defaults, mismatched schema/manual content, incorrect state-directory commands or a mandatory TUI. | Instructions list sessions from the wrong directory after `start ./project`. | | `ub32` | Present synthetic fixtures or mock lifecycle tests as real vulnerability discovery, live deployment validation or measured audit savings. | Unmeasured parity with another harness appears as a release claim. | ## Evidence and test traceability These are the current implementation/test entry points for the behavior groups. They are not a claim that every model or operating environment has been validated. A release issue should cite the behavior ID, triggering configuration/source fixture, expected result and observed result. | Behaviors | Implementation and validation entry points | |---|---| | `b01`–`b07` | [Source inventory/tests], [primary-context regression], [additional analysis integration], [navigation], [LSP tests] | | `b08`–`b14` | [Pipeline tests], [structured analysis/group tests], [economic models], [domain profiles] | | `b15`–`b19` | [Plan/local runner tests], [native controls], [proof/recovery/cycle tests], [shared proof integration] | | `b20`–`b23` | [Concurrent budgets], [exact token parsing], [CLI limits], [independent scouting/concurrency], [provider tests] | | `b24`–`b27` | [Credentials/config tests], [wire tests], [FFI tests], [store recovery], [shared recovery] | | `b28`–`b31` | [Report schemas], [SARIF path tests], [cloud lifecycle mocks], [runner], [CLI], [manual generator] | | `b32` | [Development validation boundaries], [comparative evaluation protocol], human adjudication on held-out vulnerable/repaired/benign cases | For Host behaviors, a reproducible violation is an implementation defect. For Model behaviors, retain the source, prompts/model configuration, candidate, evidence and counterexample and evaluate the miss under a fixed benchmark. For Operator behaviors, record the missing prerequisite or failed infrastructure assumption explicitly; do not convert it into a clean security conclusion.
Configuration
# Configuration
Dependency inventory/advisory passes, opt-in dependency source paths and pinned binary inputs are described in [dependency audits]. Own-task progress monitoring, working memory and tool `preflight_command`/`environment_id` are described in [investigation runtime].
`katarina init` writes the complete annotated example. YAML uses strict known-field decoding: misspelled fields, duplicate keys and multiple documents are errors. Omitted fields receive defaults; explicitly invalid values fail validation. Configuration is loaded once by the controller, not independently by agents.
The examples below are configuration fragments. Merge them into the file generated by `katarina init`, retaining the required agent roles and any other settings needed for the review.
## Providers and credentials
```yaml
version: 1
engine: pi
credentials_file: /home/you/.config/katarina/credentials.yaml
providers:
router:
kind: openrouter
api_key_env: OPENROUTER_API_KEY
claude:
kind: anthropic
api_key_env: ANTHROPIC_API_KEY
openai:
kind: openai
deepseek:
kind: deepseek
local:
kind: compatible
base_url: http://127.0.0.1:1234/v1
allow_http: true
api_key_env: LOCAL_MODEL_KEY
token_parameter: max_tokens
```
Credential file (mode `0600`):
```yaml
router: your-openrouter-key
claude: your-anthropic-key
openai: your-openai-key
deepseek: your-deepseek-key
```
The map uses configured provider names, not necessarily provider kinds. Environment variables override the file, which overrides an inline provider `api_key`. Prefer the file or environment. `credentials_file` paths resolve relative to the configuration file. Native providers need a key; a custom compatible endpoint may accept anonymous requests.
| Kind | Default API root | Default environment variable | Wire API |
|---|---|---|---|
| `openai` | `https://api.openai.com/v1` | `OPENAI_API_KEY` | Chat Completions |
| `anthropic` | `https://api.anthropic.com/v1` | `ANTHROPIC_API_KEY` | Messages |
| `openrouter` | `https://openrouter.ai/api/v1` | `OPENROUTER_API_KEY` | Chat Completions |
| `deepseek` | `https://api.deepseek.com` | `DEEPSEEK_API_KEY` | Chat Completions |
| `compatible` | Required | Operator chosen | Chat Completions |
`base_url` is an API root; Katarina appends `/chat/completions` or `/messages`. HTTPS is required unless `allow_http: true` is explicit. Redirects are refused. Compatibility means the documented text Chat Completions request and response shape; provider-specific OAuth, nonstandard response shapes and arbitrary proprietary parameters are not implemented. Model refusals, truncated responses, malformed structured output and empty replies are failures, not clean security results.
OpenAI uses `max_completion_tokens`; other Chat Completions providers default to `max_tokens`. `token_parameter` can explicitly select either. No sampling temperature is forced, allowing reasoning models that reject it. Anthropic uses its top-level system prompt, `max_tokens`, `x-api-key` and version header. Upstream requests/responses use their required JSON API; worker communication uses protobuf.
## Model routing
Each role has an independent provider and model. Use exact model IDs available to your account:
```yaml
agents:
scout: {provider: deepseek, model: deepseek-v4-flash}
challenger: {provider: deepseek, model: deepseek-v4-flash}
defender: {provider: deepseek, model: deepseek-v4-flash}
judge: {provider: deepseek, model: deepseek-v4-pro}
test_writer: {provider: deepseek, model: deepseek-v4-pro}
```
Select models available to the configured provider accounts and evaluate them on representative repositories. Independent prompts and separate requests reduce simple agreement effects, but agents using the same model may share biases. Compare model and provider combinations when evaluating false positives.
## Scan limits
`katarina start --max-agents 16` sets the maximum simultaneous model requests. It overrides `scan.workers` (default 16, valid range 1–64). Scouting and the independent challenge/defense stages run concurrently; dependency-bound stages wait for their inputs. The limit covers model workers, not compiler threads or external language-server processes.
| Field | Default | Meaning |
|---|---:|---|
| `workers` | 16 | Concurrent model jobs, 1–64 |
| `passes` | 2 | Independent security lenses per chunk, 1–8 |
| `scout_mode` | specialized | `focused` uses an open-ended, file-seeded investigation prompt |
| `deep_percent` | 0; init example 10 | Stable hash sample, 0–100, for independent `deep_scout` jobs |
| `deep_paths` | [] | Included-file globs that always get an independent deeper scout |
| `token_budgets` | {} | Per-family input+output token reservation caps; integers or amounts such as `100M` and `1B` |
| `context_requests` | 3 | Extra read/search/LSP rounds, 0–12; question investigations use `analysis.investigation_context_requests` instead |
| `chunk_bytes` | 16000 | Approximate numbered primary-chunk size, minimum 1024 |
| `max_file_bytes` | 8388608 | Maximum included text file, up to 128 MiB |
| `max_context_bytes` | 64000 | Initial source and additional context limits, up to 2 MiB |
| `max_output_tokens` | 4096 | Per-completion output cap, 256–65536 |
| `max_calls` | 1000 | Hard persisted reservation cap; includes attempts and context requests |
| `max_cost_usd` | 0 | Disabled at zero; otherwise requires positive rates for every role |
| `timeout_seconds` | 180 | Per-model request timeout, 1–3600 |
| `max_attempts` | 2 | Attempts per incomplete job in one invocation, 1–5 |
| `exclude` | See example | `**` globs relative to repository root |
To enable cost reservations:
```yaml
agents:
scout:
provider: deepseek
model: deepseek-v4-flash
input_per_million: 0.14
output_per_million: 0.28
# Set current rates on ALL active roles, including deep_scout and proof_reviewer when enabled.
scan:
max_cost_usd: 20
max_calls: 400
```
The rates above are illustrative; replace them with the provider's current rates. Before execution, a job reserves an amount based on input bytes plus overhead, the output token limit and the configured per-million rates. Reservations are conservative, never refunded, and survive a crash. They bound dispatch under the configured rates. Actual charges can differ because providers may account for caching, reasoning or other features separately. AWS and optional external tools are not covered by the model budget.
Evaluate a small repository before increasing passes or context limits. Model selection and provider routing remain fixed for the session.
## Per-model-family token budgets
Give agent configurations a `family` label to share a session-wide cap across roles, models and providers. The label is explicit: an OpenRouter model and the same model's direct API can both use `family: claude`. If omitted, the exact model ID becomes its own family; the provider name is never used to guess a model family.
```yaml
agents:
scout: {provider: deepseek, model: deepseek-v4-flash, family: deepseek}
deep_scout: {provider: deepseek, model: deepseek-v4-pro, family: deepseek}
# Keep challenger, defender, judge and test_writer entries from katarina init.
scan:
workers: 16
token_budgets:
deepseek: 100M
```
Equivalent CLI overrides, using families assigned to active roles:
```sh
katarina start --max-agents 16 --token-budget deepseek=100M ./project
# If a configured active agent uses family: claude:
katarina start --max-agents 16 --token-budget deepseek=100M --token-budget claude=10M ./project
```
YAML and CLI budgets accept decimal suffixes, case-insensitively: `K` = 1,000, `M` = 1,000,000, `B` = 1,000,000,000 and `T` = 1,000,000,000,000. For example, `100M`, `1B`, `1.5B` and `250k` are valid; YAML quotes are optional. Unsuffixed integer counts still work. Fractional suffix amounts must expand to a whole token: `0.001K` is one token, but `0.0001K` is rejected. Zero, negative amounts, unsupported suffixes and expanded counts above 2^60 are rejected. These suffixes apply to family budgets, not to fields such as `max_output_tokens`.
Amounts are normalized to integer counts before validation and persistence. Reports and printed resume commands use these integer counts, so switching between equivalent spellings such as `100M` and `100000000` preserves the configuration digest and budget.
Each cap includes input **and** output across scouting, debate, assessment, proof reviews, revisions, context requests and retries. Before dispatch, SQLite atomically reserves `system/prompt UTF-8 bytes + 1024 + max_output_tokens`. This deliberately pessimistic estimate prevents workers racing past the configured reservation cap. Reservations are never refunded, including after a crash or an upstream error whose billing is unknown. Exhaustion stops the session as incomplete; it does not silently skip a stage or switch families.
These are dispatch limits, not provider-enforced invoice limits. Exact tokenization, hidden reasoning and provider accounting may differ. The report shows reserved tokens separately from observed input/output usage, marking estimated usage when a provider omits counts. Caps are per session; they do not cover other Katarina state directories or applications using the same API account. A missing cap means unlimited for that family, still subject to the global call/cost limits. Provided caps must expand to positive whole token counts and name an active family.
CLI limits are saved in the effective configuration. The printed resume command includes them; changing them requires a new session under the existing resume policy. This prevents restarting from resetting an exhausted budget.
## Test commands, tools and language servers
See [testing] and [navigation]. These execute operator-configured programs; model output can select a configured test command key but cannot supply arbitrary argv. Design notes are repository-relative included files. AWS settings are described in [AWS].
`analysis.tool_requests: 4` opts into agent-selected tool discovery, documentation research, named execution and setup proposals across languages; 0 disables it, and the maximum is 64 per task. These actions also consume context rounds. Set tool entries to `mode: agent`, with a description, fixed `command`, `timeout_seconds`, optional file `extensions`, `version_command` and `max_output_bytes`. Omitted mode retains preflight execution. Agent-mode execution is local, independent of `tests.runner`, and cached per tool per session for fixed commands. Set `transport: mcp` or `json` with explicit read-only `operations` to enable structured, argument-driven follow-ups with task-local sessions; see [interactive tools]. See [the complete configuration and execution contract].
Solidity economic/game-theory guidance is active for `.sol` scouting and subsequent triage, even with one pass. Rust and C/C++ files receive their own review guidance within the same model requests. Supply protocol assumptions through `design_notes`; see [economics]. Optional rust-analyzer and clangd examples are included in `katarina init`.
## Shared knowledge, questions and evidence
The `analysis` block controls shared security knowledge, generated and configured questions, evidence checks with additional-capability/deployment analysis, and finding groups for shared tests. Fresh `katarina init` files enable these stages; existing files that omit the block retain their earlier behavior. See [the full configuration and workflow], including role inheritance and added model costs.
The optional `architect` and `investigator` roles inherit the complete `scout` agent configuration; `planner` and `grouper` inherit `judge`. Explicit role entries override that inheritance. Their calls use the inherited or configured family caps and rates. Configured questions are additional to `analysis.max_investigations`, and neither kind replaces regular or deeper scouting.
## Environment exposure
Worker subprocesses inherit a small allowlist: PATH, JAVA_HOME, GOROOT, locale and platform paths, plus a private HOME. Only that worker's provider key travels over its private protobuf pipe. Local test/tool processes receive no model/AWS keys from the controller. This is environment hygiene, not host isolation: same-user local processes may access other user files. Use an appropriately isolated environment for untrusted execution. Selecting SSH for tests does not relocate controller-side tools or LSP servers; see [execution boundaries].
## Economic scenarios and research
The init example enables `analysis.scenario_coverage: true` and sets `analysis.scenario_investigations: 6`, `independent_percent: 30`, and `experiment_requests: 3`. Omitted coverage remains disabled and omitted counts remain zero for compatibility. Coverage requires at least one independent slot and enough guided slots for at most eight families each (currently three guided slots). Independent slots use a neutral policy without the supplied taxonomy. Valid ranges are 0–64 investigations, 0–100 percent and 0–16 experiments. Scenario navigation and research share `investigation_context_requests`; every model call and public research action consumes the global call budget. `agents.investigator` inherits the scout configuration if omitted.
`research.incidents` enables the bundled historical index. `research.public` and `research.history` are off by default. Public search needs an HTTPS `search_url` accepting a GET `q` parameter; public fetching can operate without a search endpoint. `allowed_hosts` is an optional list of exact hostnames. `max_bytes` defaults to 32768 (1024–1048576), and `timeout_seconds` defaults to 20 (1–120); zero chooses these defaults. `request_cost_usd` reserves an operator-specified cost per public action. `chain_snapshots` maps names to operator-captured files and exact SHA-256 digests. Full formats and limits are in [economic discovery].
Start a new session after changing the review policy or these configuration values. Unchanged sessions replay saved observations; an interrupted request with no outcome remains indeterminate.
## Distributed-system reviews
`analysis.distributed_systems: true` adds the distributed review profile and twelve coverage families when `scenario_coverage` is enabled. Six scenario slots with 30% independent work support both distributed and economic coverage (32 families for Solidity-containing roots). Scenario discovery now runs across languages even without the distributed flag. See [architecture, fault schedules, history checks and limits]. Omitted distributed settings remain disabled; start a new session after this policy upgrade.
## Proof quality, follow-ups and practice comparisons
Fresh init files enable `analysis.proof_quality: true`, `analysis.followup_investigations: 4`, and `analysis.practice_comparisons: 4`. Existing files that omit these keys keep false/zero. The counts accept 0–32 and bound additional investigations and comparisons; all calls share session budgets. Public comparisons also require `research.public: true`; agent-selected searches need `research.search_url`, while direct public fetch can operate without it. Execution still requires a prepared `tests.runner` and configured commands. Start a new session after changing configuration or upgrading to review policy `15-interactive-tools`. See [contracts, limitations and examples].
## Guided investigation ledger
`analysis.investigation_ledger: true` enables bounded collaboration for guided scouts and investigators, including related-defect searches. Fresh init files enable it; omission retains the prior behavior. Enabling it requires positive `scenario_investigations` and `independent_percent` so at least one unhinted slot is reserved. Unhinted discovery, deep scouts and all assessment/proof roles are denied ledger access by the controller. Accepted discovery results are published after each task ends, so guided follow-ups can use unhinted findings without changing the unhinted prompts.
Explicit read/claim/update requests use normal context rounds. Each guided dispatch also receives a saved, bounded snapshot of recent relevant work. Claims last 15 minutes and can be renewed through a `working` update. Completed/expired topics need an explicit revisit reason; concurrent verification needs both a reason and `independent_verification: true`. This flag does not create an unhinted agent. Claims coordinate declared topics; they do not grant execution permissions or replace existing test/tool replay protection. See [ledger semantics and limitations].
## Capability composition and external boundaries
Fresh init files enable `analysis.boundary_analysis: true`, `composition_windows: 4` and `composition_investigations: 4`. Existing configurations that omit these fields retain false/zero. Composition accepts 0–16 chain investigations and 0–32 extraction windows; enabling investigations requires at least one window. All extraction, planning, navigation, review and proof calls share the existing session budgets. `capability_mapper` inherits the scout model and `chain_planner` inherits the judge model; both can be overridden explicitly.
The phase runs after committed discovery and related investigations. It keeps ignored candidates with their counterevidence, extracts useful capabilities from observations and source, and proposes links across files. Each proposed chain receives an investigation and independent assessment; chain proofs remain separate from grouped primitive tests. Deferred input/primitive IDs, intermediate status and complete graph evidence appear in `composition.json` and the report. A completed phase is bounded scheduling, not exhaustive composition coverage.
Boundary guidance is excluded from unhinted discovery. Boundary test plans declare `environment.scope` (`component`, `integration`, `platform`) and can include `environment.boundary_cases` with route, state, property, generated test path and an exact assertion excerpt. Composed proof plans require at least one such case. These fields describe the intended experiment, not a runner attestation. Prepared commands and dependencies are still required. See [capability composition] for operation and evaluation.
## Simulation and SSH execution
`tests.runner: ssh` enables generated proofs and exploratory experiments on operator-configured `tests.ssh` machines. `tests.simulation_command` names an existing command that runs the reusable campaign interface; investigators and test writers receive its neutral schema. See [configuration and limits].
`scan.task_instructions` is an optional scope/instruction string of at most 32 KiB, supplied to every role including independent investigations. Use it for universal scope boundaries, not attack hints; place guided research questions in their existing fields. The EVMBench adapter supplies its pinned upstream task instructions through this field.
Katarina architecture
# Katarina architecture
Katarina is a Go controller with short-lived model workers, an embedded SQLite store and a statically linked Rust agent runtime. The controller owns the review workflow and all consequential decisions about scope, dispatch, validation, execution and persistence. Workers supply model completions; they do not coordinate directly or own session state.
This document explains the current implementation. The [product specification] defines supported behavior and limits; [behavior and definitions] supplies stable requirements and terminology. The diagrams describe software boundaries and data dependencies, not a network of permanently running agents. The ASCII diagrams also remain readable in the embedded plain-text manual.
## Component map
```text
OPERATOR INPUTS REVIEW INPUTS
CLI + YAML + credentials repository + design notes
| |
v v
+--------------------------------------------------------------------+
| GO CONTROLLER |
| configuration -> source inventory -> stage scheduling |
| | | |
| optional tool/LSP <------+ prompt/context assembly |
| adapters on source copies | |
| budget reservation |
| | |
| result validation <---------------------+--------------------+ |
| | | | |
| v v | |
| assessed findings model dispatch | |
| | | |
| +-> plans -> none/local/SSH/EC2 -> proof review --------+ |
| | |
| +-> JSON / Markdown / SARIF / event and analysis exports |
| |
| SQLite store <---- jobs, budgets, evidence, execution/cloud intents |
| events ------> optional TUI / text progress |
+-----------------------------------------+--------------------------+
| private framed protobuf
v
+-----------------------------------+
| SAME-BINARY WORKERS (bounded pool) |
| one completion per child process |
| |
| pi: Rust agent via C ABI |
| -> Go provider callback |
| direct: Go provider adapter |
+-----------------+-----------------+
| HTTPS / provider JSON
v
MODEL API ENDPOINTS
Local runner -> disposable directory, operator OS privileges
SSH runner -> strict OpenSSH -> same-binary execution worker
Campaigns -> local/SSH trials + retained source/input replay
EC2 runner -> AWS SDK -> S3 + EC2 + SSM -> disposable test host
Static site -> embedded assets; independent of session execution
```
```mermaid
flowchart TB
Operator[CLI, YAML and credentials] --> Controller[Go controller]
Repo[Repository and design notes] --> Inventory[Source inventory]
Inventory --> Controller
Inventory --> Tools[Optional tools and LSP on copies]
Tools --> Controller
Controller <-->|jobs, budgets, evidence and intents| DB[(Embedded SQLite)]
Controller <-->|framed protobuf over private pipes| Worker[Same-binary model workers]
Worker --> Pi[Rust pi runtime through C ABI]
Pi -->|provider callback| Provider[Go provider adapter]
Worker -->|direct engine| Provider
Provider <-->|HTTPS and provider JSON| API[Configured model APIs]
Controller --> Runner[Test plan and runner]
Runner --> Local[Local disposable workspace]
Runner --> SSH[SSH: operator-provided execution worker]
Runner --> AWS[AWS SDK: S3, EC2 and SSM]
Local --> Result[Recorded execution evidence]
AWS --> Result
SSH --> Result
Result --> Controller
Controller --> Reports[JSON, Markdown, SARIF and artifacts]
Controller --> Progress[Optional TUI or text progress]
```
The `demo` engine supplies synthetic responses in the controller without an external model call. `serve` is a separate static-site command and exposes no controller or database API.
## Software responsibilities
| Component | Responsibility |
|---|---|
| [`cmd/katarina`] | CLI dispatch, effective configuration/overrides, state selection, preflight, process locking, startup/resume/export and static serving |
| [`internal/config`] | Strict YAML, credential resolution, role inheritance, defaults, exact token amount parsing and configuration/policy identity |
| [`internal/source`] | File inclusion/exclusion, source hashes/chunks, outlines, bounded context/search and verified source copies |
| [`internal/lsp`] | Optional language-server lifecycle and constrained JSON-RPC navigation |
| [`internal/engine`] | Stage dependencies, worker pool, deterministic job identity, prompts, context loops, evidence validation, grouping and proof history |
| [`internal/simulation`] | Strict campaign manifests, seeded trials, controls, retained input/source evidence and replay |
| [`internal/evmbench`] | Separate Detect launcher contract and incremental retained-finding export; upstream sandbox/grader remain external |
| [`internal/model`] | Typed domain objects and validation for findings, economics, reviews, plans, interpretations and report data |
| [`internal/wire`], [`proto/worker.proto`] | Versioned protobuf request/response types and bounded frame encoding |
| [`internal/provider`] | HTTP API compatibility, endpoint rules, response/refusal/truncation checks, usage and the pi transport adapter |
| [`internal/piffi`], [`ffi/pi-bridge`] | cgo/C ABI ownership and typed provider callbacks into the statically linked Rust agent runtime |
| [`internal/store`] | SQLite state, atomic budget claims, job checkpoints, immutable artifacts, proof/resource intents and recovery |
| [`internal/runner`] | Permitted generated paths, command selection, disposable local overlays, bounded execution and captured outcomes |
| [`internal/cloud`] | Remote source transfer, idempotent resource launch, SSM execution, expiry and cleanup/recovery |
| [`internal/process`] | Child process environment, bounded buffers, deadlines and platform process-group handling |
| [`internal/report`] | Committed-state aggregation and atomic individual JSON, Markdown, SARIF and event exports |
| [`internal/tui`] | Controller stage events plus lightweight durable progress snapshots; responsive terminal map and live work view; it does not schedule or approve work |
| [`deploy`], [`web`], [`cmd/manual`] | Embedded stack template/static assets, build-time manual links and public template generation |
| [`cmd/bundle`] | Native pi release/source archives, source/build identity, dependency notices and download checksums |
The engine depends on typed provider/executor, store and runner interfaces or adapters. Model output passes through domain validation before it can become a controller action. HTTP JSON, model YAML, protobuf IPC and SQLite JSON blobs serve different boundaries; they are not interchangeable protocols.
## Execution flow
```text
Go controller / SQLite
|
+-- inventory: hashes, line chunks, symbols and exclusions
+-- configured analyzer output / optional LSP snapshot
+-- independent scenario investigations (neutral, run first)
+-- guided scenario investigations / family accounting
| +-- bounded research and optional early experiments
+-- optional per-chunk security knowledge / question planning
|
+-- cheap scouts, one job per chunk and security lens
| +-- bounded reads, literal search and LSP navigation
+-- independent deeper scouts (configured sample / paths)
+-- additional configured / generated question investigations
|
+-- deterministic candidate fingerprint / deduplication
|
+-- independent challenger -----+
+-- independent defender ------+--> defender rebuttal
| |
+--------------------------------------v
assessor
|
log / ignore / test
|
retain every disposition
|
related-instance searches / capability composition
optional established-practice research
|
optional grouping of log/test findings
|
test dispositions only
|
generate individual/shared tests
|
none / local / SSH / EC2
|
review execution evidence
/ \
retain conclusion bounded test revision
|
JSON + Markdown + SARIF
```
Every included UTF-8 text file is chunked with five-line overlap where possible. Binary files, credential filenames, dependencies/metadata directories, configured exclusions, oversized files and lines exceeding the chunk limit are recorded. Directory exclusions are represented by one directory entry rather than every descendant. The filesystem scan does not depend on Git and does not silently apply `.gitignore`; configure intentional exclusions explicitly.
Scouts have different lenses: input-to-sensitive-operation paths; state/economic invariants; and integration/trust-boundary challenges. Every pass covers all included chunks. Candidate fingerprints use location, CWE and normalized title. This deterministically deduplicates repeated candidates, but is not semantic clustering: differently phrased duplicates can remain.
`scout_mode: focused` uses an open-ended investigation prompt instead of the rotating lens. In either mode, seed chunks are starting points for cross-file reasoning. Optional `deep_scout` jobs use a separately configured model on a stable hash sample and explicit paths, independent of cheap scouts' results. This prevents the cheap stage from being the only possible discovery path. See [research design] for comparison principles and the limits of benchmark claims.
The challenger and defender see the candidate and repository context, but not each other's initial review. The defender then answers the challenge. The assessor sees both reviews and the rebuttal. Dispositions are retained even when ignored. A “by design” disposition needs explicit design evidence; intent alone is not proof of safety. With structured evidence enabled, an ignore also requires a cited refutation or inapplicability. Additional capability, economic effects and deployment assumptions are recorded separately from severity and action.
Optional knowledge extraction precedes scouting. The shared artifact contains source-cited, challengeable claims. Independent deeper scouts do not inherit these claims. Specific generated and configured questions add work to the bounded scout pool; they cannot remove baseline coverage. Grouping follows individual assessment and preserves every finding. Shared plans and proof reviews must account for each member. See [shared knowledge, questions and evidence].
When tests execute, a separate proof-review request sees the generated test and recorded result. It can support/refute the hypothesis, retain uncertainty or request a concrete revision within `tests.max_iterations`. An optional `proof_reviewer` model can supply an independent counterpoint; otherwise the judge model handles this request. Interpretations remain separate from command status and the initial disposition. Attempts retain separate plans, execution intents and reports.
## Stage dependencies and data flow
Stages form a directed workflow with bounded local navigation and proof-revision loops. Guided discovery can communicate through a controller-owned investigation ledger; unhinted/deep/review roles cannot read it. There is no free-form agent mailbox. The controller places an earlier stage's validated output into a later stage's prompt when that dependency is allowed.
| Stage | Inputs and transformation | Committed output / next consumer |
|---|---|---|
| Prepare | Strict configuration, included source, source/configuration identity, analyzer snapshots and design notes | Session, saved effective configuration/inventory; context for later work |
| Explore | Independent slots finish before guided slots; bounded self-chosen hypotheses, research, experiments and family accounting | Exploration plan/results, observations, coverage and candidates; later review |
| Architect, optional | Per-chunk source and permitted context become cited, typed claims; controller assigns and deduplicates IDs | Immutable `security_knowledge`; planner and selected ordinary tasks |
| Planner, optional | Bounded source map and knowledge become additional questions; configured questions are resolved separately | Immutable `investigation_plan`; investigators |
| Discover | Full baseline coverage plus selected independent deep chunks and additional questions; bounded navigation as requested | Accepted job responses, individual investigation artifacts, deduplicated candidates |
| Debate | Candidate and source feed blind challenge/defense, followed by defender rebuttal | Completed review jobs; judge context |
| Judge | Candidate, reviews, rebuttal, source and optional structured evidence become an individual disposition | Assessed findings, including ignores |
| Expand, optional | Related-instance investigations and capability composition follow individual assessment; new candidates receive ordinary reviews | Lineage, capability graph, deferred coverage and additional findings |
| Compare, optional | Retained candidates and independently fetched practice evidence; unavailable when public access/evidence is missing | Practice comparisons and limitations, without changing severity/disposition |
| Group, optional | Bounded windows of non-ignored assessments become validated member/scenario proposals | Immutable `finding_groups`; report relationships and eligible shared proof scopes |
| Write and execute | Test-selected scopes become permitted new-file plans; runner intent precedes execution | Saved plans, durable execution intent/result and per-finding proof history |
| Interpret and revise | Generated files plus actual command result become member-aware proof interpretations; a concrete revision can create a new bounded attempt | Updated proof history; next attempt or retained conclusion |
| Export | Committed state plus saved session inputs become schema-defined reports | JSON, Markdown, SARIF, event JSONL and conditional analysis artifacts |
An architect, scout, investigator, peer reviewer or judge can consume additional navigation completions, each with a separate job ID and reservation. Architect/investigator/capability-mapper roles inherit scout configuration if omitted; planner/grouper/chain-planner inherit judge. A configured deeper scout is required when deeper work is enabled. The proof reviewer defaults to judge unless separately configured.
Ordinary scouting may use shared knowledge. A deep scout receives source/design/tool context but neither shared model claims nor ordinary discoveries. Investigations receive only selected knowledge references; an empty list supplies none. Peers share the candidate but not their initial answers. These are information-access constraints; using the same model for several roles can still produce correlated errors.
Grouping is bounded, not exhaustive global clustering. Proposals are made within deterministic windows of at most 20 assessments and a context-size limit. Oversized assessments and matches across windows can remain individual. A report group containing both `log` and `test` dispositions does not authorize a shared execution; its test-selected members still follow individual proof work. Proof scopes currently execute sequentially.
## pi integration through FFI
Katarina statically links pi through a C ABI bridge to package the agent runtime and Go controller in one executable. `ffi/pi-bridge` compiles a Rust `staticlib`; Go links it through cgo under the `pi` build tag. Provider transports and the security workflow are implemented in Go.
The bridge uses pi's documented `sdk::Agent`, `Provider`, `ToolRegistry`, `AgentConfig` and message types. It installs a custom provider whose typed C callback calls the Go HTTP provider adapter. This keeps model routing, output limits, credentials, timeout ownership and cost reservations consistent across providers. Pi owns the in-process agent invocation; Katarina owns the higher-level security workflow.
Pi is invoked with an empty tool registry. Source navigation is controlled by Katarina's validated context-request loop. Shell tools, ambient project extensions, arbitrary edits and workspace configuration are not loaded into pi. Implicit tool defaults, magic-keyword shortcuts and automatic turn continuation are disabled. These restrictions limit the runtime actions available to an agent exposed to prompt injection in source code.
The C ABI is in `internal/piffi/bridge.h`: versioned request/result structs, explicit ownership, one synchronous provider callback and a matching Rust result-free function. No Go pointer is retained in Rust; `runtime/cgo.Handle` carries an opaque integer. Rust panics are caught before crossing C. Pi and provider errors propagate as failed jobs.
`pi_agent_rust` is pinned to `0.3.0`, with a checked-in Cargo.lock and pinned nightly toolchain. Its `sqlite-sessions` feature is enabled because the published 0.3.0 library has imports requiring it even in a headless build. Its default TUI and BPE-token features are disabled. The Go controller owns Katarina's authoritative SQLite store.
## Workers and communication
The controller launches the **same Katarina binary** with its internal `worker` command. A worker performs one model request and exits. Concurrency is a bounded controller pool. A timeout kills the worker process group, including a blocked FFI invocation; no separate daemon needs supervision.
`--max-agents` overrides `scan.workers`, limiting simultaneous model workers across each pipeline stage. Family-token reservations, the call count and the USD reservation are checked atomically in one SQLite transaction before dispatch. `family` is a configured model grouping independent of provider transport. Retries and navigation rounds consume new reservations; interrupted or unused reservations are not refunded.
Messages use `proto/worker.proto`, generated Go types, and a four-byte big-endian length prefix over stdin/stdout. Frames are capped at 8 MiB. Requests and responses carry protocol version and job ID, which the controller validates. Credentials are passed only through the anonymous request pipe, not argv. Only the controller writes the database.
Provider adapters use the external model APIs' JSON formats, and optional language servers use standard Content-Length JSON-RPC. Worker pipes carry Protocol Buffers messages. Agent conclusions are strict YAML documents, parsed into typed Go models before checkpointing.
## Context and navigation
Initial context contains the primary numbered lines, a bounded repository map, selected nearby/imported files, design notes and captured analyzer output. For jobs seeded by a source chunk, space for the numbered primary chunk is reserved before supplementary context, including shared model claims. Additional questions start from bounded per-file windows and can request further source evidence. Context budgets are explicit; truncation is marked. Agents can request more evidence using a typed YAML `request_context` document: line reads, literal searches, document symbols, definitions and references. Each completion and retry consumes a persisted budget reservation.
Built-in Go outlines use Go's parser. Other language outlines use structural heuristics; they are not a sound call graph or type analysis. Optional language servers provide semantic navigation and Slither supplies Solidity-specific analyzer evidence. File context never follows a model-supplied URL or reads beyond the included inventory.
## Persistence and failure semantics
SQLite uses WAL, `synchronous=FULL`, foreign keys, bounded busy waiting and a controller process lock. Durable entities include sessions, jobs/attempts, events, assessed findings, immutable analysis artifacts, test execution intents/results and cloud resource intents. Interrupted running jobs become pending on resume; completed results are reused. Shared proof evidence is committed atomically for all members, and replaying earlier assessments preserves committed test progress. Unknown provider charges remain reserved.
A provider can complete a request before the controller commits its result, so resuming an interrupted call may repeat the request and its charge. Test execution intents are written before launching a command; missing results stay indeterminate. EC2 launch uses an idempotent client token and persists intent before upload/launch. Cleanup runs on success, error and cancellation, with explicit recovery commands.
### One model completion
```mermaid
sequenceDiagram
participant C as Controller
participant S as SQLite store
participant W as Worker process
participant P as Rust pi runtime
participant G as Go provider adapter
participant A as Model API
C->>S: Ensure job and read checkpoint
alt Accepted result already committed
S-->>C: Saved response
C->>C: Reuse accepted job in current stage
else Unfinished job
C->>S: Atomically claim job and reserve call, tokens and USD
S-->>C: Claim committed or error
Note over C,S: A rejected claim stops dispatch
C->>W: Framed protobuf request
W->>P: C ABI agent invocation
P->>G: Typed synchronous provider callback
G->>A: HTTP completion request
A-->>G: Text and usage, or transport error
G-->>P: Typed completion result
P-->>W: Agent result or error
W-->>C: Framed protobuf response
C->>C: Check identity, parse YAML and validate stage contract
C->>S: Commit accepted result or failed attempt
C->>S: Append progress event
end
Note over C,W: Context requests and retries consume further reservations
```
This sequence shows the `pi` engine. `direct` bypasses Rust and invokes the same Go HTTP adapter. A validated `request_context` response completes its own job; the controller performs allowed navigation, assembles the next prompt and dispatches a new completion. Invalid output can consume another attempt on the unfinished job within the configured per-invocation limit. Neither path refunds the original reservation.
The pool limit defaults to 16 and bounds simultaneous model workers. Before dispatch, the claim transaction updates job state, session call/USD totals and family reservations together or rolls all of them back. Reported token usage is accumulated separately. Database updates use one connection, while HTTP completions run concurrently in children. Tool/compiler/LSP threads are outside the model-worker limit. Source bytes and stage prompts are held in memory; neither the worker cap nor per-context limits impose a total RAM bound.
### Durable data model
```text
sessions (id, root, source/config digests, status, call/USD reservations)
|
+-- jobs (session, job ID, role, status, attempts, latest result, usage)
| +-- job_families (session, job ID -> family label)
+-- family_budgets (session, family -> reserved tokens)
+-- events (global sequence, session, time, kind, job ID, message)
+-- analysis_artifacts (session, name -> immutable JSON object)
| security_knowledge / investigation_plan / investigation:ID
| finding_groups
+-- findings (session, finding ID -> assessed-finding JSON aggregate)
| candidate + reviews + decision + group reference + proof history
+-- tests (session, scope:attempt:N -> intent state and result JSON)
+-- resources (resource ID, session, client token, instance, object, state)
meta (storage version)
Session/job parent links are database foreign keys.
IDs inside JSON evidence/groups are checked by controller validation.
```
| Stored entity | Identity and checkpoint semantics |
|---|---|
| Session | Global session ID; stores root, source/configuration digests, lifecycle state and cumulative call/USD reservations |
| Job | `(session_id, id)`; accepted result, latest error/result, attempt count and accumulated usage. It does not archive every failed retry response. |
| Family budget | `(session_id, family)`; monotonic reserved tokens. `job_families` ties a job to one family for usage reporting. |
| Event | Global autoincrement sequence plus session ID; ordered operational history. It is not an event-sourced replacement for the entity tables. |
| Analysis artifact | `(session_id, name)`; immutable accepted knowledge, plan, question answer or group artifact |
| Assessed finding | `(session_id, id)`; JSON aggregate. Saving earlier assessment work merges committed proof progress instead of erasing it. |
| Test attempt | `(session_id, finding_id)`; despite the column name, its value is an individual/group scope plus `:attempt:N`. Storage state is `running`/`done`; execution status lives in the result object. |
| Cloud resource | Global resource ID; durable token/object/instance lifecycle including planned, launching, running and cleaned states |
Knowledge, question and group IDs link JSON domain objects, not separate normalized SQL tables. Member-aware proof updates use one transaction for all affected finding aggregates. A job completion and its progress event are separate writes; a crash may commit evidence without its final progress message. The database records operational checkpoints, not every prompt token, provider billing event or arbitrary external effect.
### State transitions and recovery
| Object / interruption | Recovery behavior |
|---|---|
| Job: `pending` or `failed` | A successful budget claim sets `running` and increments attempts; accepted output becomes `done`, otherwise `failed`. |
| Job left `running` or `failed` on resume | Reset to `pending`; completed jobs stay reusable and earlier reservations remain consumed. |
| Test intent without a committed result | Preserve an `indeterminate` execution. Do not automatically rerun the attempt or treat it as a clean failure. |
| Test with a committed result | Reuse the result; resume proof interpretation/checkpointing as needed. Revisions reject every prior execution digest in that scope. |
| Cloud intent or live resource left behind | Use saved ownership/client-token metadata for cleanup; expose failures and retain explicit cleanup/reap commands. |
| Session handled error/cancellation | Set `incomplete` and attempt report export. |
| Session successful workflow return | Set `completed`, even if a finding remains unresolved or a test command failed. |
| Hard process kill | Session may still say `running`; exports can lag behind committed SQLite state. Process locking determines whether another controller may start. |
Resume checks the current root/inventory and effective configuration, including the review-policy version. Credentials can rotate without changing that identity. A different source revision, model allocation, budget or policy starts a new session. Older sessions can still be exported when their saved artifacts are supported; resuming old review policies requires a compatible build.
The state directory contains the SQLite database and per-session files. Saved `config.json` and `inventory.json` supply the inputs used by report regeneration; the inventory stores metadata, not complete source bytes. JSON/Markdown/SARIF and conditional exports are individually atomic files, not one atomic export set. Retain the exact source revision and the session directory together for audit handoff. See [reports and recovery].
## Execution and trust boundaries
The model proposes conclusions, navigation and permitted test content. The controller checks structure and source provenance before scheduling consequences. Exact quotation matches establish that text occurs in the included source; they do not establish that a claimed exploit, invariant or economic payoff follows from it. Economic and capability review require model reasoning and human assessment as well as typed fields.
| Boundary | Data and authority |
|---|---|
| Operator to controller | Scope, model routes, credentials, budgets, commands, runner and deployment assumptions are operator inputs. Strict configuration validates supported shape and values. |
| Repository to model | Included source, selected design/tool context and permitted prior evidence can reach configured API endpoints. Exclusions and known-key redaction are not universal secret detection. |
| Controller to worker | Only the selected provider credential and explicit prompt/request settings cross the private protobuf pipe. Workers have private working directories and reduced environments; process separation is not an OS security sandbox. |
| Model to controller | Strict YAML proposes findings, citations, context operations, decisions or test plans. It cannot add executable commands, install tools, choose arbitrary URLs for navigation or write the database. |
| Controller to analyzer/LSP | Configured executables run against disposable source copies. They are trusted local programs with possible host/network effects; LSP response locations are constrained to included source for agent navigation. |
| Controller to local tests | New allowed files overlay a hash-verified included-source copy. The configured argv runs with operator OS privileges, a private HOME, reduced environment, timeout and output cap. Generated code can still have host effects. |
| Controller to SSH tests | Operator-configured targets, key paths and strict host verification; validated bundle/request over stdin; same-binary worker, fresh workspace and remote deadline. SSH is transport, not OS/network isolation. |
| Controller to AWS | The SDK uses operator AWS credentials for encrypted S3 transfer, EC2 and SSM. The prepared host runs test code unprivileged in a separate network namespace; the AMI and control plane remain prerequisites. |
| State/reports to reviewer | Source excerpts, vulnerability hypotheses and execution output persist in local state and reports. Private directory/file permissions protect access; report content is not encrypted by Katarina. |
The EC2 controller records intent before uploading/launching, uses an idempotent client token and expiry tags, and requests instance termination and source-object deletion on completion, errors or cancellation. An in-instance shutdown timer and recovery commands cover additional failure cases. A failed boot, unavailable AWS API or missing permission can defeat immediate cleanup; a termination request is not proof of deletion. The CloudFormation quick-create link provisions supporting infrastructure, not access keys or a prepared test image. See [AWS] for the complete remote path and [testing] for proof semantics.
## Packaging and extension points
The pi release build links the Rust static archive into the Go executable and embeds the website, generated manual and CloudFormation template. SQLite is embedded; no database service is needed. Optional project compilers, analyzers, language servers, provider endpoints and AWS infrastructure are external. The manual includes clickable links, ASCII diagrams and Mermaid source without a runtime diagram-rendering dependency. The bundle command produces native/source archives and checksums under the Git-ignored website downloads directory; these archives are hosted externally and are not recursively embedded in the executable.
Additional OpenAI-compatible endpoints are normally configuration changes. A different transport shape belongs in the Go provider adapter, preserving credential, output and usage rules. New analyzers and language servers use configured argv adapters. A new workflow stage belongs in the controller with typed outputs, context rules, budget reservations, deterministic job IDs and recovery semantics. Domain-object changes require corresponding schemas and report handling. Observable behavior and policy changes must update the [specification], behavioral IDs and session-compatibility boundary together.
## Post-discovery capability composition
After discovery, initial assessment and related-instance follow-ups, optional capability mappers consume committed observations (including ignored findings with counterevidence) and source. A bounded global planner proposes cited capability-to-prerequisite edges. Each proposed chain receives an investigator and the usual independent assessment; controller-owned graph provenance follows it into a separate proof. Immutable extraction/planning/investigation/assessment checkpoints support replay and incomplete reporting. Unhinted discovery runs before these artifacts exist and cannot read them. See [composition and boundary testing].
## Reusable simulation and external evaluation
Simulation campaigns use the same local/SSH execution primitives outside the model worker protocol. A strict JSON manifest selects explicit files, cases, seeds and limits; each trial gets fresh state and a persisted dispatch intent. Project adapters return structured observations; the runner distinguishes process outcomes, property assertions and expected controls. Standalone runs retain full source bytes and inputs for replay. Generated audit campaigns use the normal test overlay and capture their output into proof/observation records. See [simulation execution].
The separate EVMBench Detect adapter constructs an ordinary engine session inside the upstream environment, supplies hash-checked task scope to every role and incrementally exports retained assessed findings. Full reports stay private to the run; discarded/pending candidates and debate prose do not enter the official submission. It neither provides the upstream sandbox/grader nor supports Patch/Exploit. See [EVMBench integration].
Shared knowledge, questions and evidence
# Shared knowledge, questions and evidence
Katarina can build a shared security model, investigate specific questions alongside regular scouting, require structured evidence for review decisions, and group findings for shared tests. These stages use the existing Go controller, protobuf workers, SQLite checkpoints and model-family budgets. They require no additional services or packages.
## Enable the workflow
New `katarina init` configurations enable these features. Add this block to an existing configuration to enable them there:
```yaml
analysis:
shared_knowledge: true
max_investigations: 8
investigation_context_requests: 8
evidence_checks: true
grouping: true
max_group_size: 6
questions:
- question: Can liquidation become unprofitable within the documented operating range, leaving debt unpaid?
paths: ["contracts/**/*.sol"]
- question: Does every tenant-scoped database query preserve the authenticated tenant identity?
paths: ["src/main/java/**/Tenant*.java"]
```
Use questions and paths that apply to the repository. Each question must match 1–32 included files; an unmatched or oversized selection fails visibly. Split a broad question into narrower starting points when necessary. Target files seed the investigation; agents can navigate to any included file using the existing read, search and LSP tools.
| Setting | Behavior and limits |
|---|---|
| `shared_knowledge` | One architecture extraction job per included chunk, followed by a saved shared artifact. |
| `max_investigations` | Maximum generated questions, 0–64. Zero disables the planner. Configured questions are additional. |
| `investigation_context_requests` | Additional navigation rounds for each question, 0–64; defaults to 8 even when the feature is otherwise disabled. Other tasks use `scan.context_requests`. |
| `evidence_checks` | Requires structured checks from both initial reviewers, the rebuttal and the assessor; also requires capability and deployment analysis from the assessor. |
| `grouping` | Asks whether multiple non-ignored findings can share a bounded validation scenario. |
| `max_group_size` | Members per group, 2–12; defaults to 6. |
| `questions` | Up to 32 explicit questions. Each has a nonblank question of at most 4,000 bytes and 1–32 repository-relative path globs. |
Omitting `analysis` leaves knowledge, generated questions, evidence checks and grouping disabled for compatibility with existing configurations. The settings can be enabled independently. Explicit questions work with `max_investigations: 0` and without shared knowledge. Changing these settings changes the session configuration digest: start a new session to apply a different review policy.
## Shared security knowledge
The architect extracts components, boundaries, actors, assets, invariants and dependency assumptions. Each claim has a stable controller-assigned ID, exact source citations and an `observed`, `inferred` or `unknown` status. The artifact is bound to the reviewed source digest. Solidity guidance includes economic mechanisms and incentives; Rust/C/C++ guidance includes ownership, unsafe/FFI contracts and build assumptions.
Katarina verifies that cited files are included, line ranges exist, and quoted text occurs within the cited lines. Citations span at most 41 lines with at most 4,096 quote bytes. This verifies provenance. It does not establish that the inference follows from the quotation, that a comment describes actual behavior, or that the system is safe.
Regular scouting and subsequent review receive bounded shared context, prioritizing claims citing the current file. Complete claims that do not fit are omitted with a count. Independent `deep_scout` jobs receive source, design notes and tool output but **no shared model claims or earlier scout conclusions**. This gives discovery a path that does not inherit errors in the shared summary. It does not make calls using the same model statistically independent.
Knowledge extraction finishes before planning and scouting. Failed extraction or an exhausted budget leaves the session incomplete; the controller does not silently discard the failed stage. Completed chunk jobs remain available for recovery even if the combined artifact has not yet been assembled.
## Additional questions
The planner receives a bounded repository map and shared knowledge and proposes specific mechanisms to examine. It may return fewer than the configured maximum, including none. The controller validates every target path and knowledge reference and assigns stable IDs. Planner output does not remove any ordinary scouting pass or independent deeper sample.
Generated questions can select specific shared claim IDs. An empty selection means no inherited knowledge. Configured questions also start without shared model claims. Investigators can request source evidence, follow callers and state transitions, seek counterexamples, and return an answer with citations, unresolved obligations and zero or more candidate findings. An answer without citations must retain unresolved obligations and cannot introduce findings. All candidates enter the normal challenge, defense, rebuttal and assessment process.
Question answers are persisted separately, including answers that produce no findings. A missing final answer appears as incomplete in the report. Knowledge and question coverage are reported separately from baseline and deeper scouting. Investigation counts describe the committed plan; if planning itself failed, inspect the incomplete session and failed jobs before interpreting coverage.
Useful questions include ownership obligations across a Rust safe wrapper and unsafe implementation; allocation units across C/C++ callers and build modes; Java tenant identity propagation; and Solidity asset flows or profitable deviations across multiple transactions. A question should identify a property to check and a possible way to refute the concern, without assuming a defect exists.
## Structured evidence and additional capability
When evidence checks are enabled, each reviewer must address every obligation:
| Check | Required reasoning |
|---|---|
| `reachability` | Can the relevant entry point and claimed path execute? |
| `control` | What input, state, action or timing can the participant influence? |
| `guards` | Do existing checks, call-site rules or environmental controls defeat the claim? |
| `invariant` | Which intended safety or economic property is violated? |
| `impact` | What concrete consequence follows? |
| `feasibility` | Are the sequence, build/deployment assumptions and resource requirements possible? |
| `incentives` | For economic findings, what motivates the deviation or griefing and what is the net payoff or cost asymmetry? |
| `capital` | For economic findings, what funding, locked capital, liquidity, duration or ordering capability is required? |
Outcomes are `established`, `refuted`, `unknown` and `not_applicable`. All outcomes except `unknown` require source citations. Unknown checks must name the next evidence needed. Invariant, impact, incentives and capital cannot be waived as inapplicable. The last two checks are mandatory when a finding contains structured `economics`; economic review guidance is active for Solidity regardless of this setting.
A supporting review cannot contain unresolved or refuted obligations. A refuting review needs a cited refuted obligation. The assessor separately records a `supported`, `refuted` or `unresolved` evidence verdict, the action, severity and confidence. A supported verdict requires resolved checks, meaningful additional capability, and applicable or explicitly conditional deployment. An ignored finding requires a cited refutation or cited inapplicability. Uncertainty and intended behavior alone cannot justify ignoring it.
Capability analysis describes the actor, existing authority, additional access/control/profit/harm, the boundary or invariant crossed, and economic effects. Its status is `meaningful`, `exposure`, `equivalent` or `unknown`. Deployment applicability is `applicable`, `conditional`, `not_applicable` or `unknown`, with explicit conditions. Known statuses need citations. Unknown build flags, integration settings, subsidies or market assumptions remain visible.
Existing privileges alone do not establish that a Solidity participant's imposed losses are accepted. Permission to liquidate, withdraw or vote can coexist with harmful incentives. Economic effects therefore remain part of capability analysis even when no additional access privilege is gained. A severe but unresolved concern can be logged or selected for a test without pretending its feasibility is established.
These checks enforce structural completeness, source provenance and consistency of conclusions. They do not mechanically verify reachability, profitability, semantic entailment or the truth of model judgments. Human review and meaningful tests remain necessary.
## Grouping and shared tests
After individual assessment, the grouper proposes findings that one scenario with member-specific assertions can evaluate. Each group retains all original IDs, locations, prerequisites, reviews, decisions and severities. The proposal must state the common question, conditions, cited rationale and required assertion for every member. Unknown IDs and overlapping membership are rejected. Similar titles or a shared file are insufficient grounds to group.
Only groups whose members all have an individual `test` disposition receive a shared plan. Other groups remain report organization, and any member selected for testing proceeds individually. Findings outside groups also keep their individual test path. Ignored findings remain in reports and do not enter grouping.
A shared plan has a `covers` entry for each member, naming a generated test file and an exact excerpt of its assertion. The controller checks that the excerpt exists in that file. The proof reviewer must then assess actual discovery, execution, prerequisites and observations for each member. An excerpt can be present without executing, so this second check matters. One successful command cannot establish every claim.
Shared verification includes a separate `supports`, `refutes` or `inconclusive` interpretation for each finding. The overall result cannot be supports/refutes unless all members agree. Mixed outcomes remain visible; a group can support one observation and leave another unresolved. Revision uses the existing `tests.max_iterations` limit and must preserve every member's assertion. Indeterminate execution is never automatically repeated.
Grouping uses deterministic windows of at most 20 candidates whose assessed records fit `scan.max_context_bytes`. Oversized candidates and matches spanning windows may stay separate. This bounds model context but does not guarantee global semantic deduplication or minimum test count. Original findings are never deleted by grouping.
## Models, costs and recovery
New roles inherit existing model settings unless explicitly overridden:
| Role | Default model configuration |
|---|---|
| `architect` | `agents.scout` |
| `investigator` | `agents.scout` |
| `planner` | `agents.judge` |
| `grouper` | `agents.judge` |
An override is a complete agent entry, with the same provider/model/family/rate fields as other roles. Role inheritance includes family and pricing. For example, keeping `scout.family: cheap` and `judge.family: judges` charges architecture/questions to `cheap` and planning/grouping to `judges`. Configure family caps such as `cheap: 100M` and `judges: 10M` under `scan.token_budgets`; include the families used by any independently configured deeper scouts, writers or proof reviewers as needed. The same shorthand works in CLI overrides, including `--token-budget cheap=1B`.
All stages obey `scan.workers` / `--max-agents` and share the existing call, token and USD reservation limits. Enabling knowledge adds one model job per chunk; planning adds one; each question adds one plus permitted navigation; grouping adds one per eligible window. Retries also count. Evidence checks enlarge the existing debate/assessment calls instead of adding a separate stage. Shared tests may reduce duplicate execution, but that saving is not guaranteed to outweigh the added analysis. Measure quality and cost on representative repositories.
Accepted jobs, shared knowledge, the plan and answers, grouping proposals and proof outcomes are checkpointed in SQLite. Shared execution evidence is committed atomically for every member. Resume reuses completed work and retains reservations, while previously interrupted model calls can still incur another charge. See [reports and recovery] for artifact contracts and compatibility rules, and [comparative evaluation] for measuring detection quality and audit effort.
Proof quality, operational risk and practice comparisons
# Proof quality, operational risk and practice comparisons Katarina separates potential impact, evidence strength, deployment applicability and comparison with established practice. A high-impact concern can remain unresolved. Existing privileges, normal protocol behavior, expensive reproduction and adoption elsewhere do not by themselves refute harm. ## Configuration and execution order Fresh `katarina init` files include: ```yaml analysis: proof_quality: true followup_investigations: 4 practice_comparisons: 4 scenario_coverage: true scenario_investigations: 6 independent_percent: 30 investigation_context_requests: 8 ``` The three new keys are false/zero when omitted from existing configuration. Counts range from 0 to 32. Each follow-up and practice comparison uses the existing investigator role, concurrency and session call/token/cost budgets. Follow-ups can produce candidates that incur further review/proof calls. These settings are limits, not a promise of four findings or completed executions. Public research and test execution retain their existing explicit opt-ins. Enable `research.public` for comparisons; configure an HTTPS `research.search_url` for searches chosen by agents. Direct page fetching does not require a search endpoint. Configure a prepared test runner and named commands to execute generated tests. Unhinted discovery runs first with its neutral system policy and without operational/economic/distributed hints, family assignments or prior conclusions. Generic proof environment requirements apply if it chooses an experiment. Guided discovery follows, then ordinary investigation and scouting, independent challenge/defense/rebuttal/assessment, bounded related-defect searches, practice comparisons, grouping and proofs. Follow-ups do not replace reserved neutral slots. Start a new session to apply policy `15-interactive-tools`; old sessions remain exportable. ## Authorized mistakes and editable values Guided roles examine who can grant/revoke authority, upgrade, pause, change addresses, fees, caps, collateral factors, oracle configuration and settlement parameters. Review includes: - Writer-to-consumer paths, units/scaling, individual bounds and coupled constraints. - Wrong decimals, seconds/milliseconds, zero/extreme values and incompatible addresses. - Multiple individually valid updates creating an unsafe intermediate state, stale queued changes and effects on existing positions. - Lost or renounced administrators, circular role control, emergency overrides and recovery when a dependency or authority has already failed. - Blast radius, reversibility, monitoring and the actor able to recover in time. The required Solidity family `operator-configuration` makes this an explicit coverage obligation: 20 economic families, or 32 when distributed coverage is also enabled. Every assigned family needs an investigation, cited inapplicability or an explicit unresolved next step. This does not force a vulnerability verdict or guarantee execution of every scenario. Findings can supply `operational_risks`: role, editable value, units/bounds, feasible mistake, blast radius, safeguards, recovery and exact code citations. Its presence requires structured review and assessment even when `analysis.evidence_checks` is off. Capability `exposure` accommodates harm without an attacker gaining authority. A privileged setter alone is insufficient evidence of a defect; accepted trust and feasible operational mistakes must be distinguished. Multisigs and delays do not establish correct parameter semantics. ## Economic and architectural assumptions Guided exploration can record source-cited `assumptions` with failure transitions, status (`supported`, `violated`, `conditional`, `unresolved`), reasoning and next evidence. This optional inventory remains incomplete and challengeable. It complements the mandatory family coverage and existing scenario/external-risk records. Useful experiments trace honest behavior, adverse sequences, parameter sensitivity and loss allocation. Examples include an authorized collateral-factor update affecting existing debt; delayed health-check approval after collateral withdrawal; oracle staleness combined with unprofitable liquidation; and an ADL/socialization transition shifting losses to otherwise solvent participants. Track profit net of coalition transfers, financing, fees and gas, plus debt, insurance depletion and counterparty loss. A contract executing its specification can still expose users to an unsafe assumption. ## Proof fidelity and quality When enabled, both early scenario experiments and final finding proofs require a test-plan `environment` identifying included production paths, relevant dependency modes (`real`, `mocked`, `simulated`, `unknown`), versions/state, legitimate baseline, negative control, sensitivity and limitations. The controller checks referenced paths. This declaration is supplied by the model; it is not runner attestation of production fidelity. The independent proof reviewer returns `quality` with exactly five checks: | Check | Evidence to examine | |---|---| | `production_path` | Actual implementation and relevant dependency boundary exercised | | `test_discovery` | Intended tests discovered and executed | | `representative_trigger` | Inputs/state/orderings represent the alleged failure | | `meaningful_assertion` | Assertions observe the claimed violated property | | `controls` | Legitimate behavior and relevant negative controls exercised | Each check is `established`, `failed` or `unknown`. Established checks require exact quotations from complete recorded execution output. Definitive `supports`/`refutes` requires all five established; otherwise the reviewer must return inconclusive or request a concrete bounded test revision. A reviewer must inspect test source too: an output string claiming a path was exercised can be fabricated. Quote validation establishes provenance, not semantic truth, complete coverage or a calibrated confidence score. Optional `measurements` retain exact decimal strings, units, conditions and `observed`/`estimated` basis. Observed values require an exact recorded output quotation containing the value. Model inference from that output can still be wrong; estimates never become realized loss merely by appearing in the report. A simulated balance shortfall does not establish market depth, keeper participation or an attack's actual profitability. No severity ceiling is imposed for mocks or unavailable reproduction. Test files remain additions in disposable source snapshots; this workflow does not rewrite production code. Existing proof revision limits, repeated-plan rejection and interrupted-execution protection remain in force. General repair generation is separate. For supplied vulnerable/repaired snapshots, the existing [benchmark differential workflow] runs the same overlay on both sides; use legitimate-behavior checks and inspect actual assertions before accepting the repair. A demonstration test may pass on vulnerable code and fail after repair; a permanent safety regression should do the reverse for the affected property. ## Related defects and candidate accounting After initial review, the controller selects up to `followup_investigations` nonignored findings by severity and stable ID. These are hypotheses, including unresolved concerns, not automatically confirmed defects. One generation of follow-ups searches other callers, writers, readers, background paths and shared assumptions across the included inventory. Each new fingerprint goes through the full independent review and normal grouping/proof pipeline. Matches do not inherit the seed's verdict. Plans retain `parent_finding_id`, completed answers, unresolved paths and findings deferred by the count limit. Controller-derived `pipeline` records link candidates to origin jobs and their last evidence stage: unassessed, assessed, no proof plan, not executed, execution outcome or proof interpretation. Reports preserve pending follow-up plans and practice comparisons after interruptions. Lineage can locate unfinished work; determining a wrong dismissal, inventory omission or a never-discovered issue requires an external oracle or independent auditor. ## Established-practice and state-of-the-art research For up to `practice_comparisons` nonignored findings, a separate investigator chooses public research queries and pages. It looks for primary implementations, documentation, papers, stronger alternatives and counterexamples. It compares mechanisms, versions/commits, assumptions, safeguards, costs and differences with this project's deployment. Searches use generic mechanism terms; private code and identifiers must not be sent to public endpoints. Existing network restrictions, host allowlists and evidence budgets apply. Each comparison must quote a complete fetched observation from the same task and source snapshot. Invented observations, borrowed evidence, truncated pages and search snippets cannot support the record. Reports retain URL, retrieval time, content digest and claimed version (or explicit unknown). Fetching a page verifies neither its authority nor a claim of superiority: those remain reviewable model judgments. A few examples cannot establish prevalence or state of the art. The result separates observed practices, alternatives/tradeoffs, residual risk and limitations. It cannot change the finding's severity or disposition. Public research disabled, unavailable evidence, or insufficient comparable material yields `unavailable`; unscheduled and unfinished comparisons remain visible. This supports statements such as “the design shares a documented practice, with these additional assumptions and residual hazards” without turning common practice into acceptance of risk. ## Validation and evaluation limits Regression tests cover full related-candidate review, neutral prompt isolation, exact evidence validation, structured operational exposure, proof/research persistence, exports and resume without repeated work. Controlled model/runner fixtures verify orchestration contracts, not vulnerability detection quality. Compare enabled/disabled features at equal budgets on development cases and untouched families, measuring independently validated issues, false positives and human review effort before claiming better detection or audit savings. See [evaluation design] and [benchmark assessment]. Guided agents can now share attempts, blockers and next steps through the [investigation ledger], while unhinted discovery and independent review remain isolated.
Investigation ledger and independent discovery
# Investigation ledger and independent discovery The ledger lets guided agents learn what peers tried, what failed, what remains blocked, and what evidence could make another attempt useful. It is a controller-mediated record with bounded reads and explicit claims. It does not introduce free-form peer messaging or an autonomous rescheduling loop. Enable it with `analysis.investigation_ledger: true` (enabled by fresh `katarina init`, disabled when omitted). Enabling the ledger requires positive `scenario_investigations` and `independent_percent`, reserving at least one unhinted discovery slot even when family coverage is disabled. The fresh defaults retain two unhinted slots. Start a new session after applying review policy `15-interactive-tools`. ## Independence is enforced | Task | Reads/claims/updates | Controller publication | |---|---|---| | Unhinted discovery | Denied, including guessed requests | Accepted final result after its task finishes; failures recorded separately | | Independent deep scout | Denied | Accepted final result or task failure | | Guided exploration, ordinary scout, configured/generated/related investigation | Allowed | Recorded actions and accepted final result or task failure | | Challenger, defender, rebuttal, judge, proof writer/reviewer | Denied | Existing evidence/review pipeline remains in use | | Practice-comparison research and other roles | Denied | Existing research artifacts remain in use | Unhinted agents get neither ledger instructions nor ledger snapshots. Their intermediate hypotheses and actions are not published to it. Their finished work can inform subsequent guided research. Unhinted slots still run before guided exploration, and remain unable to read the ledger even on resume when peer records already exist. A model cannot grant itself access by changing a field in a request. Initial challenge and defense retain their separate contexts. Guided candidate evidence still reaches those reviewers through the existing finding-specific handoff, but they cannot consult peers' ledger conclusions. Explicit rebuttal continues to expose the challenge as designed. ## What is shared Records contain controller-assigned job identity, source digest, timestamp and record ID. Claimed work adds a stable work key, claim ID, paths, hypothesis/topic, concrete approach and lease expiry. Updates retain summary, next step, source citations and recorded observation references. Outcomes distinguish `working`, `supported`, `refuted`, `blocked`, `failed` and `inconclusive`. Supported/refuted are peer interpretations requiring evidence references, not accepted security verdicts. A missing compiler, unavailable archive state or failed test setup cannot mechanically refute a hypothesis. Final publication `completed` means the discovery task returned a valid result, not that its files are safe. Action publications retain process/research status separately. The controller publishes final discovery output even if the agent never makes a ledger request. Guided tool/research/experiment actions publish references to their recorded outcomes. Neutral intermediate work remains private. Final output excerpts are bounded; full jobs and observations stay in the session evidence. All peer text is marked untrusted, and reading it must not waive assigned source or scenario-family coverage. ## Claims, revisits and handoffs Guided agents can return `request_ledger` with `operation: read`, `claim` or `update` during normal navigation. The prompt describes the complete schema. Reads accept a literal query and exact included paths; explicit reads can look beyond the current source seed. Claims are atomic within the session/source snapshot. The work key normalizes topic case/whitespace and sorted paths. One task may hold one active claim. Ordinary claims conflict with an active owner for that topic. An update can renew a claim for 15 minutes (`working`) or finish it with a concrete outcome and next step. Only its owner can update it. Another task must create its own claim to disagree. A previously claimed topic requires a nonempty `revisit_reason`, including after completion, failure or lease expiry. The reason should identify changed inputs, new evidence, a new approach resolving a blocker, or deliberate independent verification. Concurrent verification additionally requires `independent_verification: true`. This permits useful redundancy; it does not turn the guided task into an unhinted investigation or attest to model diversity. Agents should choose other useful work when a topic is busy, rather than poll or wait. If a task exits without resolving its claim, the controller releases it as inconclusive and retains the result or failure for inspection. A hard process kill leaves the claim to expire. Expiry never permits an interrupted experiment to be silently rerun: durable test/tool intent and indeterminate-result protections still apply. Claims coordinate declared work. They do not block ordinary file coverage, prove two differently worded hypotheses equivalent, or force every source read to acquire a lock. Agents can omit a claim or choose another topic name; semantic duplicate detection is not guaranteed. Existing exact experiment/proof repeat checks and shared tool caching remain separate safeguards. A model-supplied revisit explanation is reviewable evidence of intent, not proof that the next attempt is useful. ## Budgets and recovery Explicit ledger requests consume the existing context-round limit and model call/token/cost budgets. There is no additional polling scheduler, peer-triggered model dispatch or unbounded follow-up queue. Each guided model dispatch also receives a relevant snapshot with at most 12 whole records and a record byte budget of one quarter of `scan.max_context_bytes`; response metadata adds a small overhead. If more records match, `more` is true. Agents can narrow searches rather than assume omitted evidence does not exist. Every automatic snapshot and explicit response is saved in SQLite. Claim/update mutations and their replies commit in one transaction. Resume replays exactly that response, including an old lease time; it cannot silently renew a lease or substitute new peer conclusions for old evidence. A later new dispatch can see newer work. Unhinted and blind-review tasks are denied access before reading any ledger storage. Claims and updates are append-only history. Reports export `investigation-ledger.json` and include it in JSON, Markdown, audit handoff and SARIF. Historical lease entries can be superseded by later updates; an active timestamp alone is not the current ownership state. Failed tasks and automatic inconclusive releases remain visible after eventual successful retry. ## Validation Regression tests cover concurrent claim contention, ownership, expiry, deliberate parallel verification, required revisit reasons, stable read/claim replay, snapshot separation, missing/fabricated evidence, guided blocker handoffs, final-result publication, bounded reads, and controller denial for unhinted/deep/review roles. Neutral discovery isolation is also exercised in the mixed Solidity/distributed pipeline with the ledger enabled. These tests validate coordination and isolation; they do not establish lower audit costs or elimination of semantic investigation loops.
Investigation runtime
# Investigation runtime Fresh configurations enable `analysis.progress_monitor` and `analysis.working_memory`. Existing configurations that omit them retain the previous behavior. Start a new session after upgrading to review policy `15-interactive-tools`. Working memory is a controller-generated index of a task's own accepted actions, hypotheses/falsifiers, outcomes and evidence references. It retains bounded whole index records plus recent evidence, with explicit omission markers. Original bounded records are immutable SQLite artifacts (`working_record:JOB:TURN`); tool observations remain in report exports. Resume reuses saved records. The index is not a model-generated summary and cannot turn a failed setup into a refutation. Very large histories can still omit index entries; this is not unlimited memory. The progress monitor detects repeated request/outcome/evidence combinations within one task. Action identity ignores reworded hypotheses and falsifiers; distinct configured seeds/tool variants remain distinct. Repetition adds a neutral notice to change inputs/approach, explain intentional verification or report an unresolved blocker, and emits a `progress_repetition` event. Existing context and model budgets remain the hard limits. There is no extra mentor model, semantic progress score, cross-agent watchdog or automatic new investigation. A repeated request with new evidence does not trigger the notice. Unhinted agents and blind reviewers cannot gain peer context through this mechanism. Each task owns a separate history. Dependency guidance is supplied only to guided scouts, investigators and planners when `analysis.dependency_audit` is enabled. Independently selected tools remain available under the existing tool contract. ## Tool preflight and provenance Tools can specify `preflight_command`, `version_command`, `environment_id` and content-pinned `inputs`. Version measurement, project preflight and analysis share one copied workspace, with separate cleaned temporary home directories for each process. Preflight-generated workspace artifacts therefore persist into analysis, but home-directory caches do not. A failed, timed-out or truncated preflight prevents analysis from starting and records both outcomes. Preflight success alone does not establish that tests were discovered or exercised the intended property: configure a command that asserts those conditions. For example, a prepared Go project can use `go test -run '^$' ./...` as a compilation preflight before a configured analyzer; a prepared Foundry project can use `forge build`. These commands may invoke builds and need suitable dependency caches/toolchains. Katarina does not implicitly install missing prerequisites. Wrapper commands can check test discovery, selected compiler/target/feature flags and environment restrictions. Both preflight-mode and agent-mode tools use durable execution intent. An interrupted process is indeterminate and is not silently retried on resume. Results record configuration/source digests, explicit input hashes and an environment fingerprint incorporating OS/architecture, operator environment identity and measured version output. The fingerprint does not fully measure host packages, caches, network access or sandbox policy. Use a genuinely pinned prepared runner for reproducibility; a free-text image label is not enforcement. See [dependency audits] for SBOM/advisory tools, selected source review and binary inputs. Live model/provider compatibility checks are not part of this change.
Dependency audits
# Dependency audits
Katarina supports dependency inventory/advisory evidence, optional source review, and agent-driven native binary inspection. These are separate coverage levels. A package database match does not establish exploitability; no match does not establish safety. The implementation does not automatically install package managers, resolve every ecosystem, download dependencies or launch Ghidra.
## Inventory and advisory checks
Produce a **resolved CycloneDX JSON 1.4, 1.5 or 1.6 SBOM** with your ecosystem's prepared tooling, or a suitable inventory tool such as [Syft]. Check that it contains the intended direct/transitive graph, resolved versions, optional/build/runtime dependencies and artifact hashes. A component list without graph edges cannot establish dependency depth. Katarina retains missing adjacency as a gap. Nested component containment is not treated as a dependency edge.
```sh
katarina dependencies --sbom resolved.cdx.json
katarina dependencies --sbom resolved.cdx.json --osv --max-requests 20
```
The first command is offline. `--osv` explicitly sends package URLs/versions to the fixed public OSV endpoint; it does not send source or binaries. It queries at most 100 components per batch, follows pagination within the request budget, and records request/response evidence, hashes and retrieval times. Redirects are refused. Request failures, partial pagination and ambiguous identities remain unresolved. Root metadata identifies the application and is not queried as a dependency. A cancelled run retains partial query results when it can finish normally; process termination can still prevent output.
The JSON report contains the supplied dependency graph, shortest root depth (cycles supported), component identities/hashes, advisory IDs and modification dates, and explicit statuses:
| Status | Meaning |
|---|---|
| `not_queried` | Inventory only, or the application root |
| `unknown_identity` | Missing version/package URL or contradictory identity |
| `incomplete` | Query failed or pagination/budget prevented completion |
| `matched` | OSV returned advisory IDs; applicability needs investigation |
| `no_known_match` | Completed OSV lookup returned no IDs |
[OSV querybatch] returns IDs and modification times, not full advisory details. Retrieve the original advisories to establish affected ranges, fixes, withdrawn records and applicability. Other databases and reachability analyzers remain available through configured tools. In particular, `govulncheck` can add Go-specific reachability evidence. Database freshness is the recorded retrieval time, not a frozen OSV database snapshot.
To ensure a baseline advisory pass runs, configure this as a preflight-mode tool. This example requires an installed Katarina executable and an included resolved SBOM:
```yaml
analysis:
dependency_audit: true
tool_requests: 4
tools:
- name: dependency-advisories
mode: preflight
command: [/opt/katarina/bin/katarina, dependencies, --sbom, resolved.cdx.json, --osv, --max-requests, '20']
timeout_seconds: 600
max_output_bytes: 1048576
```
Use `mode: agent` plus a description if agents should decide whether to run it. For an excluded/minified SBOM, explicitly pin it through `tools[].inputs` as below. Output limits remain real coverage limits: truncated JSON is not a complete dependency report. The CLI's zero exit means it produced a report; inspect component statuses and gaps. Guided dependency instructions cover applicability and integration assumptions. Advisory matches still pass through the ordinary independent reviews and proof process.
## High-budget source passes
Explicitly select dependency source already present in the repository:
```yaml
scan:
dependency_paths: [vendor/example.org/parser, node_modules/some-parser]
analysis:
dependency_audit: true
questions:
- question: Trace attacker-controlled input from the application into the selected parser; verify the actual fork and guards, and construct a counterexample or record the missing evidence.
paths: ['src/parser-wrapper.*', 'vendor/example.org/parser/**']
```
These literal paths opt selected subtrees into normal source inventory, chunk scouting, navigation, reviews and configured proofs. Explicit exclusions, credential filtering, metadata-directory exclusions, symlink checks and size limits still apply. Dependencies elsewhere stay excluded. Use `index` before the audit to inspect actual coverage. Included source hashes enter the session digest, so changes invalidate resume. Existing model/token/cost limits apply to all additional chunks; a high-budget pass is an operator budget choice, not an unbounded recursive audit.
Prefer exact immutable source revisions. Confirm vendored patches and dependency resolution overrides before applying upstream advisories. Select high-impact dependencies using exposure and authority, while retaining unhinted slots that can choose their own paths. Keep generated advisory reports outside the source inventory if unhinted discovery must not see them: configured tool evidence is withheld from initial unhinted exploration, but an included report is ordinary readable source.
## Native binary dependencies
`tools[].inputs` permits exact SHA256-pinned regular files, including binaries in excluded dependency directories, to be copied into the tool workspace. Inputs are capped at 64 MiB each and 256 MiB total, copied without execute permission, and identified in recorded tool evidence. Hidden paths, credential filenames and symlink traversal are rejected. Input pins cannot override the hash of an included source file. Configuration changes require a new session; resumed sessions reuse the original result rather than re-running against a changed tool installation.
The repository supplies [KatarinaExport.java] for a prepared [Ghidra headless] environment. Install that script with your trusted tooling, outside the audited repository. Example configuration (replace paths, image identity and hash):
```yaml
tools:
- name: native-parser-page-0
mode: agent
description: Disassemble and decompile the pinned native parser; export 32 discovered functions with address-linked evidence.
environment_id: your-pinned-runner-image-digest
inputs:
- path: vendor/native/parser.so
sha256: REPLACE_WITH_64_LOWERCASE_HEX_DIGITS
command: [/opt/ghidra/support/analyzeHeadless, '.', katarina-native, -import, vendor/native/parser.so, -scriptPath, /opt/katarina/ghidra, -postScript, KatarinaExport.java, '32', '0', -analysisTimeoutPerFile, '120', -max-cpu, '2', -deleteProject]
timeout_seconds: 600
max_output_bytes: 1048576
```
The exporter emits `KATARINA_BINARY` JSON records for executable hash, format, architecture/compiler, image base, Ghidra version, external symbols, function addresses/signatures, instruction bytes/disassembly and approximate recovered C. It records decompiler failures, truncation, skipped functions and whether more discovered functions remain. An interrupted export without its final coverage record is incomplete. The two script arguments are function count (1–256) and functions to skip. For this fixed-command exporter, configure distinct named pages/targets; re-requesting the same name returns cached evidence. For agent-selected follow-ups, the [interactive Ghidra adapter] supports function search, selected decompilation, cross-references and disassembly through the generic JSON transport. A prepared MCP server can expose its own operation catalog through the same controller interface.
This is bounded static binary research, not a complete binary vulnerability scanner. Investigators must trace the relevant calls and validate claims; the script's address-order pages do not rank dangerous functions. Dynamic harnesses, alternate loaders, focused exports and additional tools can be configured/proposed through the existing tool workflow. Findings should cite an included integration call site and reference the binary hash/address observation. A binary-only repository still needs an included provenance-linked textual artifact to supply Katarina's required finding location; native addresses are not source line numbers.
Tool commands run locally with a cleaned environment and time/output limits. This is **not an OS/network sandbox**. Run the whole worker in an appropriately prepared isolated environment for untrusted builds and binary parsers. The image label and environment digest are provenance, not proof of isolation. The exporter never intentionally executes the target binary. Ghidra was not installed in the implementation environment, so the script requires validation against the pinned Ghidra distribution before production use.
## Solidity differences
Review both the contract graph and its ordinary software dependencies: compiler, npm tooling, plugins, keepers and clients. [forge tree] supplies a source dependency graph; it does not establish package versions, deployed addresses or bytecode equivalence. Record submodule commits/remappings, local forks, compiler/optimizer settings, library linkage and chain/block/address/runtime-code hashes. Proxy implementation changes and mutable external contracts are part of the dependency risk.
Use an EVM-aware analyzer for deployed bytecode; the native Ghidra example makes no claim to support EVM. Known-advisory coverage is especially incomplete for semantic incompatibilities, oracle assumptions, liquidation economics and forks. Those still need source-grounded scenario generation, external-risk analysis and independent discovery.
Interactive analytical tools
# Interactive analytical tools
Katarina exposes a generic describe/call interface for agents to drive analysis tools. It supports MCP over stdio and JSON command adapters. Ghidra, static analyzers and repository languages have no special operation names in the controller. Existing fixed-command `run_tool` remains supported. Tools still require operator configuration; discovery/proposals do not install or authorize a tool.
## Agent workflow
1. `discover_tools` finds configured tools and optional research leads without starting processes.
2. `describe_tool` starts a task-local workspace and, for MCP, initializes the server and retrieves its paginated tool catalog. It returns configured operations, descriptions, JSON Schemas and operator constraints. A JSON command adapter describes its configured operations directly.
3. `call_tool` selects an operation and supplies structured arguments. Agents choose follow-ups from the returned evidence: refine a filter, request another page, inspect a finding's flow, follow a reference or decompile a selected function. Operation names come from the tool catalog, not from a fixed attack checklist.
```yaml
request_action:
kind: describe_tool
tool: native-analysis
hypothesis: Identify callable evidence methods for my own investigation
falsifier: The configured artifact or operation cannot support it
```
After successful description:
```yaml
request_action:
kind: call_tool
tool: native-analysis
operation: get_xrefs
arguments: {address: '00101230', limit: 20, offset: 0}
hypothesis: This address is reachable from the input-processing path
falsifier: The recorded references establish a different call path
```
Each action consumes `analysis.tool_requests` (0–64 per task) and a context round. For sustained investigations set, for example, `tool_requests: 16` and `investigation_context_requests: 24`. Ordinary scout navigation remains controlled by `scan.context_requests` (maximum 12). Model/token/cost caps still apply. No extra mentor or callback model is invoked.
## Configuration and transports
Both interactive transports require `mode: agent`, a fixed command, a description, and 1–64 explicitly named operations. Every operation requires `read_only: true` and an operator `input_schema`. Use constraints to fix allowed targets, narrow paths/rule sets and bound pagination. JSON Schema local references are supported; external URLs/files are never loaded. Schemas are limited to 64 KiB and arguments to 32 KiB.
```yaml
tools:
- name: analyzer
mode: agent
transport: mcp
description: Query the prepared analyzer for this source snapshot
command: [/opt/tools/analyzer-mcp, --workspace, '{root}']
timeout_seconds: 60
max_output_bytes: 65536
environment_id: your-pinned-runner-digest
operations:
inspect:
read_only: true
input_schema:
type: object
properties:
target: {type: string, enum: [src/parser.c]}
limit: {type: integer, minimum: 1, maximum: 50}
required: [target]
additionalProperties: false
```
This is a configuration template, not an installed server. Match the operation names and startup arguments to the chosen implementation. MCP validates arguments against **both** the server's input schema and the operator constraints; a server cannot widen the allowlist. Server `readOnlyHint` annotations are not authorization. `read_only` is the operator's declaration of analytical semantics, not OS enforcement: tools may maintain their own task-local analysis database, but mutating the reviewed program, live services, or shared investigation state is outside this interface.
MCP uses newline-delimited JSON-RPC on stdin/stdout. The client implements initialization, paginated `tools/list` and `tools/call`, supporting negotiated versions 2024-11-05, 2025-03-26, 2025-06-18 and 2025-11-25. It refuses newer incompatible protocol versions rather than assuming compatibility. It does not implement HTTP/SSE, server prompts, resource fetching, elicitation, sampling or automatic execution of server-suggested operations. Unexpected server requests receive method-not-supported responses. A configured stdio bridge can connect to an external backend, but the operator must ensure that backend belongs to this investigation; a shared GUI/project could defeat task isolation.
For either interactive transport, `{root}` in configured command arguments expands to the copied workspace.
For `transport: json`, the fixed command runs once per call in the same task-local workspace and reads one object from stdin:
```json
{"operation":"inspect","arguments":{"target":"src/parser.c","limit":20}}
```
It returns one result envelope:
```json
{"content":[{"type":"text","text":"Explanation"}],"structuredContent":{"records":[]},"isError":false}
```
Arguments are data; they are never interpolated into executable names, argv or shell scripts by the controller. A trusted adapter translates operations into its tool's native API. stdout and stderr share the bounded process transcript, so adapters must capture underlying CLI logs themselves and emit clean JSON. `isError: true` remains a failed tool result even if the process exits zero. An advertised MCP output schema is validated. Invalid/truncated output, unavailable functions, mismatched schemas and deadlines remain gaps, not evidence of safety. Protocol byte/message/page limits prevent unbounded streaming into the model.
## Sessions, evidence and independence
Each investigation owns its copied source/pinned inputs, preflight outputs and tool session. A tool's version/preflight commands run once when that task first describes it; failed preflight blocks calls. MCP processes remain alive across follow-ups. JSON commands share the workspace, but get a fresh cleaned home each time. All processes/workspaces close when the task ends. Local commands still run with current-user privileges: use prepared isolated workers for untrusted code or binaries.
Results retain source/configuration/environment/input hashes, operation, arguments, capability-catalog digest, status and bounded raw output. Exact repeated calls reuse that task's result. Different arguments execute new work; another task cannot receive a peer's MCP session or cached interactive observations. Description and execution are checkpointed separately. Interrupted calls are indeterminate and are not automatically replayed. On resume, completed calls are reused; a newly needed call starts a fresh tool session and must see the same catalog. Operation arguments must identify artifacts and targets explicitly; do not depend on transient server handles or previous mutations surviving a restart.
Unhinted agents can discover/select these generic evidence methods themselves. They receive no additional attack hints or peer hypotheses. Tool/server descriptions and results remain untrusted evidence; they never replace the system instructions, budgets or ordinary review/proof requirements.
## Included adapters
- [Ghidra adapter] and [query script]: search/page functions, decompile a selected function, follow references to an address, and page disassembly. They reuse a task-local headless project and check its executable hash against the configured binary on every call. Returned addresses, architecture, version, analysis-timeout flags and explicit truncation preserve provenance. Analysis limits are exposed using the [Ghidra headless API]. Requires Python 3.9+ and a prepared Ghidra/JDK installation. No Ghidra distribution is bundled; actual Ghidra execution remains unvalidated in the development environment.
- [SARIF adapter]: list rules, filter/page results and inspect full findings—including code flows, suppressions and locations—from SARIF 2.1.0 produced by any prepared analyzer. It retains the report hash and invocation records. It navigates an existing report; configure a preflight or separate adapter to build the database/run analysis. Zero results do not establish that the analyzer successfully covered the target.
See [configuration fragments]. The previous bounded Ghidra batch exporter remains available for simple fixed passes. Other MCP servers or JSON adapters can expose richer queries, compiler diagnostics, symbolic execution or fuzzing controls without changing the agent/controller protocol.
Protocol references: [MCP tools] and [stdio transport]. Review policy is `15-interactive-tools`; exported Katarina report schema is 1.12.0. Start a new session after upgrading.
Capability composition and boundary testing
# Capability composition and boundary testing Katarina can investigate chains whose constituent features are harmless or incomplete findings on their own. Examples include remote file placement satisfying an internal helper's input requirement, a dispatcher changing caller authority, and an economic operation creating the state needed for a later loss-allocation failure. The method is general: it contains no Telegram signatures, exploit strings or historical answer keys. ## Discovery, composition and review Unhinted exploration commits first. It receives the neutral system policy and generic execution contracts, without boundary guidance, shared knowledge, supplied questions or ledger reads. Guided work and ordinary source review follow. After initial assessment and related-instance investigations, composition consumes: - All assessed candidates, including ignored findings and their counterevidence. - Source-cited architecture claims and committed exploration/investigation results, including unresolved observations without findings. - Included source chunks, so harmless features remain available even when earlier agents returned no findings or shared knowledge is disabled. Extraction windows contain whole records bounded by `scan.max_context_bytes`; at most `analysis.composition_windows` windows run. Records that cannot fit are listed as deferred. Extractors can independently search/read included source and return at most 12 primitives per window. Each primitive names its input records, entry point, transformations, authority, requirements, granted capabilities, constraints and exact source citations. A primitive is not a vulnerability verdict. A planner receives a repository-wide selection of extracted primitives bounded by the same context limit. Omitted primitives are listed separately. It proposes at most `analysis.composition_investigations` chains, each with 2–8 primitives and cited forward links that match actual grant/requirement entries. Cycles, disconnected nodes, unknown references and invented grant names are rejected. Structural validation establishes provenance, not semantic truth. The planner records remaining prerequisites, final impact, a falsifier and next evidence; unknown edges remain explicit. Each chain gets a new investigation followed by the normal independent challenger, defender, rebuttal and judge. The controller attaches the graph to any resulting finding, so reviewers and proof writers retain every edge and constraint. The original dispositions are preserved. Chains receive their own proof plans; they cannot be folded into a primitive's shared test. There is one composition generation, no recursive expansion. All calls share existing limits and model-family budgets. Immutable phase checkpoints make resumption reuse committed work. `composition.json` records intermediate/completed status, extraction input IDs, deferred records, primitives, chains and resulting finding IDs. The normal investigations export contains answers and unresolved obligations even if a proposed chain produces no finding. Report schema is 1.12.0; review policy is `15-interactive-tools`. Start a new session to apply this policy. Existing configurations must explicitly enable the new controls; fresh init configurations already do. ## External authority and representation boundaries Guided agents trace external entries through transformations and privileged consumers: browser/OS launch, command-line parsing, IPC, downloaded/imported content, queues, callbacks, relayers and contract calls. They record the original actor and receiver authority instead of assuming a trusted intermediary authenticates the original requester. Encoding for one grammar is not evidence of escaping for another. Legitimate file writes, dispatch functions and economic state transitions should remain observable even if they are safe in isolation. Proof writers are asked to exercise real serializers, parsers, dispatchers and production consumers. Where applicable they vary delimiters, nested encodings, malformed inputs, runtime state and alternate routes, asserting argument boundaries, command count/type and effective authority. Deterministic property/fuzz cases can use operator-configured commands. Healthy behavior and guarded controls are required evidence obligations; compilation failures and missing dependencies do not refute hypotheses. Plans declare a scope and can bind route/state/property cases to exact assertions in generated test files. Composed plans require these bindings. This checks that an assertion exists, not that it proves its stated property. Proof reviewers must inspect both test source and recorded execution. Manually planting a file or impersonating an intermediary may establish a component result, but cannot establish the missing external route. A platform proof needs a prepared isolated environment running the real entry path. For a desktop target that includes the native build, OS protocol registration, actual process/IPC launch, settings and working directory. Use dummy private files and a local capture destination. Configure a fixed test wrapper under `tests.commands`; record build/version, dependency modes and missing assumptions in the environment. Katarina does not provision a Windows/Qt/browser image automatically. If that environment is unavailable, retain a component plan and an explicit platform evidence gap. No generated test may install dependencies or contact a live target. ## Evaluation without treating examples as discovery evidence The independent benchmark adds `cases/composition-suite.yaml`: two synthetic Go families, each with vulnerable, repaired and benign controls, plus renamed variants of the first family. One family crosses link serialization, IPC dispatch and staged automation content; the other crosses archive path handling, trusted stored plans and a privileged worker. All nine cases are development fixtures. Their 63 reference assertions include healthy behavior, primitive and composed observations, safety assertions and missing-prerequisite controls. They use real fixture implementations with in-memory dependencies; none exercises an actual browser, OS launcher or filesystem. Renaming is a contamination probe, not evidence of generalization. Answer keys declare `level: primitive|chain|platform`; legacy issues retain the `issue` category. Metrics/export separate candidate recovery, post-triage recovery and differential outcomes by level. An adjudicated primitive does not recover a chain. Platform answer keys require explicit environment/route conditions and should be used only for actual platform cases. This suite contains no platform cases; its platform denominator remains zero, meaning untested. The differential runner checks executed assertions; independent adjudicators must still decide whether an assertion proves the claimed complete chain or platform route. From the benchmark directory: ```sh go run ./cmd/katarina-bench validate --suite cases/composition-suite.yaml go run ./cmd/katarina-bench oracle --suite cases/composition-suite.yaml --profile profiles/demo-local.yaml go run ./cmd/katarina-bench composition-ablations --config /absolute/path/to/offline-discovery.yaml --out /new/ablation-directory ``` The oracle command uses the explicitly unsandboxed local development profile; choose a prepared LXD/container profile for isolated execution. The ablation generator accepts an offline configuration with positive unhinted discovery allocation, no supplied questions/design notes, and the existing benchmark execution restrictions. It writes four configurations to a new directory, preserving model choices, independent slots, proof settings and all budgets: | Condition | Boundary guidance | Composition | Ledger | |---|---|---|---| | baseline | off | off | off | | boundaries | on | off | off | | composition | on | 4 chains / 4 windows | off | | cooperation | on | 4 chains / 4 windows | on | Point otherwise identical discovery profiles at these configurations. Use identical snapshots, repetitions, model selections, configured ceilings and timeouts. These are equal budget ceilings, not equal realized spend; report actual calls, tokens, elapsed time, completion and deferred work for every condition. Preserve all repetitions and independently adjudicate primitive/chain claims and controls. Public research, incident hints, repository history and answer keys stay outside discovery. Public historical cases and cases inspected during development are regression material. Reserve separately authored/private analogous families before tuning; once inspected, they become development data. Native desktop and other-language/protocol cases remain useful future evaluation additions. Reference-test success, demo output and this implementation do not establish real-model detection performance or audit cost savings.
Competitive analysis, design principles and evaluation
# Competitive analysis, design principles and evaluation
Katarina combines broad source coverage, independent review and test execution to investigate security hypotheses within a configured budget. Its evaluation criteria are validated findings, missed issues, human review time and cost. This chapter explains the research influences, the implemented workflow and a methodology for comparing results.
## Competitive position — 15 October 2026
This update assesses Katarina at commit `6599d33` (`15-interactive-tools`, report schema `1.12.0`). Competitor descriptions below were checked against public primary sources on 15 October 2026. The linked Shannon and VulnHunter implementation reviews remain assessments of their explicitly pinned older revisions; this update does not re-audit their current source or run those products.
Katarina now implements a much broader audit workflow than the earlier comparison captured. Its strongest positioning is **source-grounded investigation of code, economic mechanisms and architectural assumptions, combining independent discovery with coordinated research and recorded evidence**. Generic interactive tools make this positioning practical across analyzers and languages. This is an assessment of implemented design; better discovery, lower false-positive burden and audit savings remain hypotheses to test.
Agent count, model diversity, tool access, debate and memory are not individually unique advantages. The defensible question is whether Katarina's combination produces more useful findings for a fixed total cost, and whether developers spend less time validating them. Public claims about another system are not independent measurements of that system, and missing documentation is not evidence that it lacks a capability.
| Comparison | Relevant public capability | Katarina's current position | What a fair comparison must establish |
|---|---|---|---|
| Strong general-purpose coding agent | Anthropic describes open-ended investigation with ordinary utilities, debuggers/fuzzers and human validation, without a custom security harness. [Methodology]. | Adds explicit coverage, protected neutral discovery, staged review, economic/architectural evidence contracts and durable accounting. The baseline can already reason and use tools; these additions must earn their overhead. | Same model, inputs, available tools and budget; compare one attempt and several independent attempts, including selection and review costs. |
| Microsoft MDASH | Microsoft describes specialized stages, multi-model debate and separate proving, with reported real-world findings and benchmark evaluations. [Technical account]. | Shares several orchestration principles and adds an explicit economic/architecture audit workflow in this repository. That does not establish that MDASH lacks those capabilities or that Katarina matches its results. | Comparable task information, runtime access and outcome verification. Without access to the same system/configuration, use MDASH as a design reference, not an invented head-to-head score. |
| Shannon | Current documentation describes source analysis, browser/CLI exploitation against running web apps, worker containers and resumable reporting. Its current pentest reporting policy emphasizes successful exploits; the older Capella source-analysis path is reviewed separately. [Current README], [pinned review]. | Broader explicit audit treatment of economic and external-assumption risks, including unresolved concerns with evidence limits. Katarina still needs prepared environments for dynamic investigation; generic MCP access does not supply Shannon's packaged web-pentesting workflow. | Compare overlapping web/source tasks separately from smart-contract work. Measure actionable unresolved risks and confirmed findings separately; reporting fewer concerns alone is not higher precision. |
| VulnHunter | The maintained fork provides portable hunt/fix procedures and investigation accounting; its README still labels sandbox-first exploit validation and measured-impact PoCs as in progress. [Current README], [pinned review]. | The adapted proof-quality, related-defect, lineage and impact-recording work is now implemented. Katarina also has controller-enforced budgets, replay rules and protected independent discovery. General production repair remains outside its audit pipeline. | Pin the host harness and enabled procedures; test proof realism, missed-candidate stages, related-instance recovery and human validation time. Do not treat prompt requirements as runtime guarantees. |
| PentAGI | Documents specialist agents, Docker-based execution, security tools, persistent memory, research and observability. [Project documentation]. | Katarina now has own-task memory/progress checks, guided work claims, preflights and interactive tools. Its distinctive design choice is preserving unhinted paths while allowing guided cooperation. PentAGI's prepared execution stack is a meaningful integration reference; Katarina's local tool launcher is not an equivalent sandbox. | Use comparable authorized tasks and environments. Measure duplicate work, loops, setup success and useful evidence; retain separate results for infrastructure pentesting and repository auditing. |
| Deterministic analyzers and dependency scanners | These are both evidence providers and necessary baselines; their supported rules, ecosystems and reachability guarantees depend on the pinned tool/configuration. | Katarina can select configured tools, navigate SARIF, investigate selected dependency source and question advisory applicability. Tool findings are candidates for review, not automatically accepted vulnerabilities. [Tool contract], [dependency contract]. | Run tools alone and give the coding-agent baseline the same tools. Attribute only additional validated discoveries or lower review effort to Katarina. |
The strongest differentiation hypothesis is economic and architectural audit depth: harmful incentives, loss allocation, stale off-chain decisions, external service assumptions, mutable roles/parameters and chains of individually legitimate capabilities. These mechanisms require explicit properties and deployment context; a generic vulnerability score can miss the benefit. This is not a claim that competing agents cannot discover them.
## What changed since the earlier assessment
“Implemented” below means there is an executable controller path or shipped adapter, with its documented configuration requirements. It does not mean a real-model audit has demonstrated the intended benefit, every feature is enabled by default, or an optional tool is installed.
| Capability now present | Implementation and practical limit | Outcome to test |
|---|---|---|
| Economic and external-risk investigations | Scenario-family assignments, falsifiers, accounting/impact records, role/parameter hazards and oracle/keeper/off-chain timing analysis. Missing coverage remains visible; a listed scenario is not proof it executed. [Economics], [audit methodology]. | Recovery of harmful behavior even where individual contracts behave as written; rejection of accepted or inapplicable risks. |
| Distributed-system review | Topology/contract questions, failure scenarios and bounded operation-history checks. Cluster provisioning, fault injection and general consistency checking still need prepared tools. [Distributed systems]. | Correct guarantees under retries, partitions, stale actors and recovery, including benign weaker-consistency controls. |
| Protected independence plus cooperation | Neutral investigations run first without supplied attack guidance or peer ledger reads. Guided agents claim work and publish failures/results; independent reviewers retain their context boundaries. [Ledger]. | Unique discoveries contributed by neutral paths, less duplicate effort and fewer true findings lost during shared review. |
| Longer investigations with progress records | Own-task working records and repeated-evidence notices preserve failures and next steps. They do not guarantee semantic progress or create an unlimited investigation. [Runtime]. | Fewer repeated dead ends and setup loops per verified result. |
| Generic interactive tools | MCP stdio and JSON adapters expose schema-described operations; agents select arguments and follow-ups. Per-task sessions, evidence provenance, limits and durable results are implemented. Tools require configuration; research/proposals do not install them. [Interactive tools]. | Correct tool choice, successful setup and useful follow-up evidence beyond a single fixed analyzer run. |
| Dependency and binary research | Resolved CycloneDX graphs, optional OSV lookups, selected dependency source, pinned binary inputs, Ghidra queries and SARIF navigation. Ghidra's actual Java/headless execution still needs installation-specific validation; advisories need applicability checks. [Dependency audits]. | Relevant transitive exposure and integration bugs, with measured setup cost and false advisory matches. |
| Capability-chain investigation | Post-discovery extraction and investigation of connected capabilities, including observations previously dismissed in isolation. Context/window limits leave explicit deferred work. [Composition]. | Complete harmful chains, missing-prerequisite rejection and transfer to unseen mechanisms/platforms. |
| Stronger proof and handoff contracts | Production-path/assumption records, bounded proof revision, related-instance searches, candidate lineage and source-backed practice comparisons. Common practice cannot lower severity automatically; model proof interpretations remain reviewable. [Audit methodology]. | Valid demonstrations, fewer mistaken dismissals and reduced auditor clarification time. |
The shift is from mostly prompt-and-review differentiation toward a controller that records and constrains the investigation process and can support richer evidence collection. The next priority is measuring that process on realistic projects. Adding further roles or mandatory forms before testing risks increasing cost without increasing useful coverage.
## Research influences
An [InfoQ report on Claude Code and Linux vulnerability discovery] describes a file-focused investigation loop. Katarina's focused scouting mode draws on the general approach of starting from a source location and following relevant evidence. It is a separate implementation, with its own tools, prompts and review stages.
Anthropic's [published methodology], coauthored by Nicholas Carlini, describes code reasoning, ordinary analysis tools, comparisons with prior fixes, dynamic checks and human validation. These methods inform Katarina's open-ended investigation prompts and emphasis on evidence beyond a detector checklist.
Microsoft's [MDASH technical writeup] describes preparation, specialized scanning, debate, semantic deduplication and a separate proving stage, using different models and domain tools. Its [model-routing update] emphasizes allocating expensive models to difficult work. Katarina applies specialized review, debate and model routing in its own workflow. Its implementation differences and evaluation requirements are described below.
## Implemented principles
| Principle | Katarina behavior |
|---|---|
| Broad coverage without a detector gate | Every included text chunk gets scouting; a seed location does not restrict where the investigator may find or cite a bug. |
| An open-ended comparison mode | `scan.scout_mode: focused` starts from one location and asks for the most consequential supported defect. `specialized` adds rotating lenses; neither requires a bug to exist. |
| Follow mechanisms across files | Bounded reads, search and optional LSP navigation trace callers, ownership/state transitions, protocol sequences and correctly handled analogues. |
| Independent deeper discovery | `deep_scout` independently reviews a deterministic sample and explicitly selected paths, even when inexpensive scouts return no findings. |
| Independent disagreement | Challenger and defender cannot see each other's initial answers. The assessor sees the arguments and their evidence. Models/providers are selectable per role. |
| Execution changes the investigation | A test writer creates a plan; a runner executes it; a proof reviewer examines the test and result and can request a bounded revision. |
| Budgeted autonomy | Every model attempt, context request, stronger scout and proof review shares the concurrency, call, cost and family-token limits. |
| Evidence survives stopping | SQLite checkpoints accepted jobs, per-attempt test intent/results, interpretations and token reservations. Reports retain uncertainty and earlier attempts. |
| Domain knowledge is explicit | Project design notes, analyzer adapters, LSP tools and configured test commands supply build rules and protocol knowledge. Solidity reviews include economic assumptions and incentives. |
| Shared context remains challengeable | Source-cited observed/inferred/unknown claims support regular review; independent deeper scouts do not inherit shared claims. |
| Questions add discovery paths | Configured and generated questions produce saved answers and candidates alongside ordinary scouting. |
| Conclusions have evidence obligations | Structured checks, additional-capability analysis and deployment applicability distinguish support, refutation and missing evidence. |
| Shared validation preserves individual outcomes | Grouping retains every finding and requires member-specific test assertions and interpretations. |
Fresh `katarina init` configurations enable a 10% hash sample for deeper scouting. The percentage is an approximate sample fraction, not a guarantee of that fraction for a small repository; `deep_percent: 100` covers every chunk and `deep_paths` guarantees selected paths. When those fields are omitted, deeper scouting defaults off for configuration compatibility. A sample is not proof that unsampled code is clean.
```yaml
agents:
# Merge these entries into your complete configuration.
deep_scout: {provider: your_provider, model: YOUR_CAPABLE_MODEL, family: strong}
proof_reviewer: {provider: independent_provider, model: YOUR_REVIEW_MODEL, family: counterpoint}
scan:
scout_mode: specialized
deep_percent: 10
deep_paths: ["contracts/lending/**", "src/auth/**"]
context_requests: 6
workers: 8
token_budgets: {strong: 1M, counterpoint: 500K}
tests:
max_iterations: 2
```
Define the referenced providers and replace the placeholder model IDs with models available to the configured accounts. `deep_scout` names a role; select and evaluate a model for that role against the intended workload. Independent providers or models can bring different review behavior. If `proof_reviewer` is omitted, the judge's configured model handles execution review using a separate prompt and request.
## What the feedback loop guarantees
With an execution runner enabled, each attempt saves its complete plan and observed result. The reviewer returns `supports`, `refutes`, `inconclusive` or `revise`. These are **model interpretations**, not independent confirmation. The report keeps them separate from command exit status and the original assessor decision.
Revision requires a concrete request and a meaningful change to test contents or the configured command. Rewording the plan or reordering its files cannot authorize an identical rerun. A revision is compared with every earlier attempt in that finding or shared group; a cycle such as A → B → A is rejected. Each revision uses a fresh source snapshot and its own persisted execution intent. Error, timeout and indeterminate outcomes cannot authorize another attempt. Unknown execution outcomes stop the loop; successful/failed commands may be revised within the configured limit. Truncated evidence cannot support a definitive interpretation. Missing negative controls remain explicit.
`runner: none` saves one plan for inspection and performs no execution review. With execution enabled, the default is at most two generated plans/executions per finding; `max_iterations` accepts 1–5. Budgets can stop the workflow before that limit. Every model call and each EC2 attempt may incur its own charge.
## Comparative evaluation
The [security benchmark assessment] maps CyberSecEval, BountyBench, CyberGym and related suites to Katarina's tasks, identifies the interactive-runner gap, and proposes matched-budget baselines and contamination controls.
Keep two tasks separate. **Discovery** starts from source without a vulnerability description. **Reproduction** starts from a supplied hypothesis. Microsoft's reported CyberGym setup supplied source and a high-level description; [CyberGym's own task levels] distinguish those inputs. A reproduction success rate cannot be used as discovery recall.
Use a versioned, access-controlled benchmark with separate tuning and held-out sets:
1. Include vulnerable and repaired snapshots, benign lookalikes, cross-file/protocol defects and economic failures. Keep labels, patches and repair descriptions outside the discovery inventory. Add private or newly constructed cases to reduce memorization risk.
2. Record source/configuration digests, toolchains, model IDs, dates, token/call limits and execution environment. Match these conditions where possible across systems. Run multiple repetitions; do not select only the best result.
3. Compare a capable focused scout with the specialized panel, then enable independent deep sampling and execution feedback separately. Measure raw candidate recall as well as post-triage outcomes. Focused mode retains Katarina's tools and triage; it is an internal comparison, not the original Claude Code harness.
4. Adjudicate findings independently of the model that generated them. A test must exercise the actual implementation and appropriate trigger. Check discovery and assertions, then run a repaired negative control. Compilation failure, an arbitrary crash, a vacuous test or an accepted economic exposure is not automatically a true positive.
5. Report unique confirmed issues recovered / known issues, precision among adjudicated findings, pending cases, duplicate rate, incorrectly ignored issues, coverage completion, reproduction success and setup failures. Track human review minutes, observed tokens, billed costs and cost per validated finding. Token reservations and cost reservations are not invoices.
6. Compare under both equal spend and equal time. Define acceptance thresholds with the auditors before running: for example, no regression in held-out high-severity recall while reducing false-positive review time. Publish failures and uncertainty alongside successes.
The automated test suite checks orchestration, concurrency, persistence, evidence transport and local execution. Detection quality requires a separate blind security benchmark; [`katarina-bench`] implements the procedure described above, and ships in `benchmark/`. No head-to-head detection or audit-efficiency advantage over the systems above has been measured. The current benchmark supports offline discovery and grader-run differential proofs; it does not yet evaluate the full interactive product workflow.
## Remaining design limits
Katarina uses deterministic candidate fingerprints and optional bounded grouping for shared tests; differently phrased findings about the same root cause may remain separate. Its shared security model is a collection of cited model claims, not a complete or verified threat model. Optional history/public research, local navigation and configured analyzers can extend an investigation; none establishes exhaustive history mining or whole-program reachability. Scouting and investigation actions include bounded tool discovery, fixed commands and structured MCP/JSON calls when enabled. Build/test environments and tool operations require configuration, and generated proof files cannot replace implementation files. General production patch generation, automatic ecosystem provisioning, a managed cluster-fault lifecycle and a validated full binary-analysis installation remain outside the current core. Record these limits when interpreting benchmark results and investigating missed issues.
## Related implementation reviews
The [VulnHunter implementation review] examines proof fidelity, input/candidate accounting, searches for related defects and miss diagnostics. The adapted proof-quality contracts, related-defect investigations, candidate lineage, operational-risk analysis and practice comparisons are now implemented in [audit methodology]; comparative performance remains unmeasured.
The [Shannon code-analysis review] examines its architecture modeling, investigation planning and evidence checks. Katarina's independent implementation is described in [shared knowledge, questions and evidence]. Evaluate knowledge, questions, structured assessment and grouping separately under matched budgets; measure missed issues and wrongly grouped findings as well as test savings. Comparative performance remains unmeasured.
## Solidity evaluation extension — 16 October 2026
The [reusable campaign runner and SSH execution] and [EVMBench Detect adapter] are implemented. Calibrated, protocol-specific [economic campaigns], automatic minimization and the remaining EVMBench modes still require work. EVMBench measures selected task performance; realistic market stress, external-service timing, precision and audit effort need separate evidence. No EVMBench result or economic-simulator performance claim is available yet.
Security benchmarks and Katarina
# Security benchmarks and Katarina Initial benchmark-protocol review: 2026-10-04. Implementation/readiness update: 2026-10-15, at Katarina commit `6599d33`. The protocol table retains its original research scope; pin and recheck the selected upstream revision before running. This is an assessment and evaluation plan, not a benchmark result or a claim that external suites are integrated. Published scores are not Katarina scores. Public documentation and examples inspected during research belong in development, not a protected evaluation set. See the updated [competitive analysis]. EVMBench research extension: 2026-10-16. Its pinned task contract, coverage gaps and proposed integration are recorded [below]. Katarina should be evaluated on **independently validated discoveries and developer review cost**. CyberSecEval provides useful component tests, but its tasks measure different capabilities. Combining them into one security score would obscure whether Katarina actually improves an audit. ## Which benchmarks fit? | Benchmark / task | What the task measures | Recommended use and limitation | |---|---|---| | CyberSecEval secure code generation | Security of instructed code generation and completion, using an insecure-code detector. | Secondary regression for generated code. It does not measure repository auditing; passing the detector is not proof of security. Turning it into a review task changes the benchmark. [Protocol]. | | CyberSecEval AutoPatchBench | Repairing C/C++ vulnerabilities discovered by fuzzing. | Useful eventual repair track, separate from discovery. Katarina currently generates proof tests, not general production patches, so this needs an explicit repair adapter. Preserve legitimate behavior as well as stopping the triggering input. [Protocol]. | | CyberSecEval vulnerability exploitation | CTF-style program exploitation. | Diagnostic of reasoning and reproducer construction, with limited resemblance to an open-ended audit. [Protocol]. | | CyberSecEval prompt injection / interpreter abuse | Susceptibility to malicious instructions and misuse. | Separate robustness gate for Katarina itself. Test hostile repository text, fetched pages and tool output; measure continued legitimate audit work too. An application-specific extension must have its own name and scores. [Suite definitions]. | | CyberSOCEval | Malware analysis and threat-intelligence reasoning. | Adjacent evidence-reading skills, low priority for source auditing. These are not measures of finding software defects. [Paper]. | | CyberSecEval MITRE/false refusal, phishing and offensive operations | Compliance/refusal, persuasion or offensive activity, depending on the task. | Do not use as the product's audit-quality objective. Their success criteria differ from useful defensive findings. [Suite definitions]. | | BountyBench Detect, **No Info** setting | Finding and demonstrating vulnerabilities in functioning application environments. Separate hinted detection, exploit and patch settings also exist. | Strong candidate for an external end-to-end discovery track. Pin exactly what information and runtime access agents receive; score legitimate runtime invariants and independently review findings outside the known answer set. [Paper, task definitions]. | | eyeballvul | Repository revisions associated with published vulnerabilities, updated over time. | Candidate source for broad, multilingual repository discovery cases. Independently validate revision applicability and reports: advisory-derived labels are not exhaustive truth. Temporal selection helps only when the relevant information postdates a credible model cutoff; it cannot guarantee no contamination. [Project]. | | CyberGym | Primarily reproducing real vulnerabilities from descriptions and source. | Strong execution-evidence track; record difficulty/input setting. Description-assisted reproduction is not blind discovery. [Paper]. | | SEC-bench | PoC generation and patching; its current runner distinguishes repository-only, description, and description-plus-sanitizer inputs. | Candidate for a controlled comparison of information levels using real execution environments. Verify the actual agent-visible files before calling a run repository-only. Defer the heavier SEC-bench Pro browser/kernel environments until the adapter works. [Runner], [Pro]. | | EVMBench | Separate loss-of-funds discovery, contract repair and sandboxed EVM exploitation tasks. | Add Detect first, then a transaction-replay integration for Exploit. Keep precision, economic stress and architecture coverage as additional tracks; Patch needs production repair support. [Detailed assessment below]. | | PrimeVul | C/C++ function-level vulnerability detection, including vulnerable/fixed pairs and chronological splits. | Cheap diagnostic for distinguishing defects from repairs and managing false positives. Too little repository/architecture context to be the main audit benchmark. [Project]. | | AgentDojo | Prompt-injection attacks and defenses in tool-using agents. | Useful methodology for a separate Katarina robustness suite; its existing application tasks are not source audits. [Project]. | These task definitions do not establish coverage of our central economic and distributed-system concerns. Keep a separate track for insolvency, loss socialization, ADL, oracle/keeper failures, off-chain checks becoming stale, retries, fencing and consistency guarantees. Require a specified property, realistic preconditions, executable observation where feasible, and repaired/benign controls. A protocol intentionally accepting a documented risk is not automatically defective. ## What the repository already supports, and what is missing The [evaluation design] already calls for matched budgets, independent adjudication, negative controls and separate discovery/reproduction tracks. The [benchmark implementation] currently forbids research, configured analyzers, language servers and in-loop test execution. Its host-side harness relies on these restrictions; only grading execution is isolated. Consequently, current offline scores cannot measure the benefit of agent-driven tools, research or iterative execution feedback. Add a **separate isolated interactive adapter**, with agent/tool processes confined to the visible workspace and prepared runtime, model credentials outside the execution environment, and grader-only access to repairs and answer keys. Keep the existing offline mode. Merely removing its checks would invalidate its isolation assumptions. The [current runner] also assumes Katarina's CLI; a generic coding-harness baseline needs an explicit adapter and evidence/report conversion. Tool discovery, public documentation research and missing-tool proposals exist in [the engine], with a non-exhaustive [catalog]. The new [interactive interface] adds MCP stdio and JSON operations, schema validation, task-local sessions and follow-ups selected by agents. Included adapters navigate Ghidra analysis and SARIF reports; [dependency tooling] adds graph/advisory evidence and selected source/binary inputs. Missing tools are still proposed, not automatically installed. Prepared language environments, general diagnostic normalization, a supported debugger/fuzzer session adapter and validated real Ghidra execution remain work beyond this interface. Fixed `run_tool` results are reused per tool/session; interactive results are reused per task/operation/arguments/catalog, allowing new questions without replaying identical calls. Neither behavior establishes complete analyzer coverage. The economic and distributed suites are development fixtures. Their passing reference assertions validate fixtures, not model detection quality. The default suite's `tenant-cache` family is labelled holdout, but its mechanism is documented and has been inspected during development in this session. **Do not use it as an untouched holdout for this development effort.** Record that exposure and establish a fresh protected set before making comparative claims; a manifest label does not establish independence. ## The comparison that would establish an advantage Start with the same strong model, task input, tool availability and total budget across these conditions: | Condition | Question it answers | |---|---| | Ordinary coding harness, one agent | What does a capable standard agent achieve? | | Ordinary coding harness, several independent attempts | Does extra sampling explain the improvement? Charge all attempts and final selection/merging; never use the oracle to select the answer. | | Katarina methodology, same tools/model | Do decomposition, independent discovery and evidence review improve the outcome? | | Katarina with prepared specialized tools | What do tool integration and execution feedback add? Also run the ordinary harness with those same tools to isolate orchestration value. | | Katarina with diverse models | Does model diversity improve unique verified discoveries after accounting for cost? | Use staged experiments rather than immediately running every combination. Once the basic comparison works, vary guided lenses, neutral discovery allocation, shared architecture, ledger cooperation, composition, progress memory, debate and proof feedback one at a time. Preserve a positive neutral discovery allocation in the primary comparisons; the product ledger requires it. Prefer measuring neutral-only contributions and neutral-slot allocation over weakening that controller contract for a benchmark. A feature earns its place by improving held-out outcomes, not by sounding like a thorough audit process. Include a tool-only baseline to measure the incremental value beyond existing analyzers. For subagents, vary investigation count separately from concurrent worker count. For example, compare 1, 4 and 8 investigators under the same spend cap, then compare latency under the same work allocation. Preserve a neutral discovery allocation with no case hints or other agents' initial conclusions. Share independently formed hypotheses later, and measure whether merging or assessment loses valid discoveries. Agreement between models is not proof, and different providers do not guarantee independent mistakes. Record unique findings contributed by each path, duplicate work, incorrectly dismissed true positives, final precision/recall, time to first verified finding and review minutes. The goal is marginal verified discoveries per additional dollar or minute, not the largest agent count. Allow agents to abandon an unproductive theory, seek an unlisted tool, follow an unexpected cross-file path or report an unsupported hypothesis without forcing it into a known attack family. ## Reusable capabilities: implemented base and remaining work 1. **Prepared, pinned tool environments.** Preflight/version commands, explicit input pins and environment fingerprints now exist. Packaging language/build detection, dependencies and a small supported set of analyzers is still separate work. Record image, binary, rules, database and source digests plus coverage and setup failures. Let the agent choose which evidence method to use. The catalog remains extensible rather than an exhaustive list of allowed reasoning paths. 2. **A common evidence envelope.** Tool process results and structured operation provenance are implemented, and SARIF navigation preserves full findings. Broader normalization of locations, diagnostics, coverage, traces and artifacts remains an extension; retain raw output. Distinguish unavailable, failed, completed-with-no-findings and incomplete. Never interpret an analyzer's successful exit as proof that code is safe. 3. **Reproducible experiment primitives.** For native code, use sanitizer builds and coverage-guided fuzzing with retained inputs and bounded campaigns; [AddressSanitizer] and [libFuzzer] provide reusable foundations. Pin seeds and environments but do not promise determinism for all fuzzing/concurrency behavior. For contracts, expose stateful properties and [Echidna] harnesses. For distributed software, expose controlled schedules, histories and property-specific checking, with [Jepsen] as an optional prepared environment. Katarina's bounded register checker is not a universal distributed-system verifier. 4. **Independent replay and controls.** Keep discovery observations separate from final grading, which replays the chosen artifact against vulnerable and repaired code and checks legitimate behavior. Crashes, missing tests and broken builds require interpretation. Runtime clusters, native PoC artifacts and production patch validation need adapters beyond the existing generated-test path. 5. **Evidence-driven allocation.** Bounded follow-ups, guided work claims, own-task memory and repetition notices now exist. They do not constitute a measured adaptive allocation policy. Evaluate routing additional investigation to unresolved, consequential questions and measured coverage gaps. Require measurable benefit before adding more specialist roles, mandatory forms or domain rules. Missing context should remain visible, not force a reassuring verdict. ## Avoiding overfitting while preserving research freedom Separate three policies: source-only discovery; research-assisted discovery; and supplied-hypothesis reproduction. Product agents should retain useful research access. A historical benchmark with unrestricted search can instead measure retrieval of its published answer. Evaluate research usefulness on private/new cases where the exact answer is unavailable, or through a frozen, audited corpus with case answers excluded. Record searches, retrievals, corpus versions and prohibited-answer exposure. Curated research results change the task and must be declared. Keep related projects, forks, fixes, synthetic variants and incident derivatives together when splitting. Deduplicate across public suites and Katarina's Rekt/DeFiHackLabs corpus. Restrict holdout source, labels and transcripts from prompt/tool developers; freeze prompts, models, rules and budgets before evaluation. Once inspected or used to choose changes, retire a holdout into development. Renaming identifiers is a robustness probe, not proof against memorization. Agents must not see repaired images, reference PoCs, advisory labels or grader output that reveals the answer. CyberGym specifically warns about network retrieval and leakage from prepared images, and requires a designated final PoC rather than selecting whichever submission passes. Follow the pinned version's protocol for an upstream-comparable result. [CyberGym FAQ]. Do not promote the evaluator's rules into production detectors and then grade against those same rules. Keep benchmark IDs, answer-specific prompts and score-dependent routing out of the product. In particular, do not equate the insecure-code detector used by a generation benchmark with independently established vulnerability truth. The upstream README also documents cleaned prompts and a secure-code runner integration caveat, so pin and smoke-test the revision rather than assuming every documented mode works. [Upstream README]. ## First testing campaign Testing can start now without waiting for the interactive benchmark adapter. Keep the following stages separate so the first results answer a clear question. | Stage | Ready now? | Procedure and permitted conclusion | |---|---|---| | Environment and evidence smoke tests | Yes, with prepared tools | Exercise representative build/test projects, analyzer queries and failure paths. Validate the real Ghidra/JDK installation before binary claims; use a small owned binary with known symbols/references. Check replay, output limits and isolated task state. This establishes integration readiness, not security recall. | | Offline methodology pilot | Yes, existing benchmark | Run exposed development fixtures and separately selected repository snapshots under the existing offline policy. Preserve vulnerable/repaired/benign controls, neutral slots and all repetitions. Measure candidate and final recovery, precision and review effort. These results apply to source-only investigation with grader-run proofs. | | Full-tool product pilot and fair harness comparison | Product pilots need prepared isolated workers; the comparative adapter is still missing | Record model, tool and human costs while agents use research, MCP/JSON tools and in-loop execution. To grade comparably, build the isolated interactive adapter and ordinary-harness adapter; keep answer keys/repairs inaccessible and credentials outside tool environments. Do not remove the existing offline guardrails. Manual product-pilot findings are case studies until conditions and adjudication are controlled. | | Frozen comparative evaluation | After pilot and environment validation | Freeze models, prompts, tools/rules, budgets and scoring; have a separate custodian select untouched project/family groups. Use the same evidence access for each baseline, repeated runs and independent adjudication. Publish both equal-spend and equal-wall-time results with uncertainty. | For the methodology pilot, use the existing focused configuration as an internal baseline and compare the full enabled methodology under the same model choices and budget ceilings. It is not a substitute for an actual general-purpose coding-agent baseline. Next compare that external baseline with one attempt and several independent attempts, then add prepared tools to both systems, then vary model diversity. This order helps distinguish method, sampling, tools and model selection. Include ordinary software, Solidity economics, distributed protocols and capability composition as separate strata. Make room for oracle/keeper failure, stale off-chain health decisions, loss socialization/ADL, operator misconfiguration, transitive dependency exposure and harmless primitives that become dangerous together. Keep case-specific mechanisms and expected scenarios out of neutral-agent inputs. Family assignment in guided arms must follow the frozen general configuration, not a benchmark answer key. Existing public incident derivatives and inspected fixtures remain development data; reserve private analogous families for evaluation. BountyBench No Info and independently validated repository cases remain candidates for external discovery; CyberGym supplies a separate reproduction track. Select cases using a predeclared sampling rule, not observed Katarina success. AutoPatchBench should follow only when production repair is supported. Choose final sample size from pilot variance and the smallest improvement useful to auditors. Before running, predeclare the scorecard: | Measure | What to record | |---|---| | Discovery | Known-issue recall and separately adjudicated additional findings; candidate-stage and final-stage recovery, severity and domain strata. Public answer sets are incomplete. | | False alarms and controls | Precision among adjudicated findings, pending adjudications, benign/repaired false alarms, duplicate findings and incorrectly dismissed true positives. | | Evidence | Reproducer validity, production-path fidelity, negative-control behavior, full-chain versus primitive evidence, unresolved deployment assumptions and tool/environment failures. | | Agent contribution | Unique useful findings from neutral/guided paths, redundant calls, revisit reasons, failed setups and findings lost during merge/debate. More agreement is not more proof. | | Efficiency | Time to first verified finding, total latency, observed/billed model usage, tool compute, environment preparation, human validation and developer clarification minutes. Charge all attempts and selection work. | | Audit usefulness | Auditor acceptance or rejection with reasons, time to a usable handoff, and total preparation plus review effort versus the matched baseline. Track whether setup savings survive repeat projects. | Publish both all-attempt outcomes and outcomes conditional on a valid environment; do not discard setup failures. Use paired comparisons with uncertainty intervals grouped by project/family. Predeclare acceptable high-severity recall regression and the minimum useful reduction in review effort with the auditors. Keep all-real-findings adjudication alongside official known-issue scores. Public research usefulness needs private/new cases or an audited corpus that excludes their answers; it cannot be inferred from rediscovering a searchable incident. Cost per validated finding and human review time are defensible audit-efficiency measures. Historical bounty payouts, theoretical value at risk and simulated losses are not measured money saved. Comparative advantage remains unmeasured until these experiments run. ## EVMBench assessment — 16 October 2026 EVMBench is a useful external smart-contract benchmark for Katarina. Treat it as three tasks with different inputs, outputs and denominators, alongside a separate economic-stress track. This review inspected documentation, agent instructions, solver/task setup and the Detect grader; no scored Katarina evaluation was run. The subsequent [Detect adapter] implements launch, frozen task instructions and incremental retained-finding export; upstream container/grader validation remains pending. ### Revision and task contract The [OpenAI repository README] redirects maintenance to Paradigm. The [Paradigm repository at `fe75a2d`] describes a companion Detect interface and pins `frontier-evals` at `8ea5c659b5232d3c520c5ca2a018fe65dc5e1988`. The benchmark runner is in that submodule's `project/evmbench`; uploading arbitrary code to the companion UI is not running the benchmark corpus. At this pinned revision, the nonempty unique audit IDs in the [split lists] number 40 Detect, 22 Patch and 16 Exploit. These are audit counts, not vulnerability counts. The current [announcement] describes 117 vulnerabilities across 40 audits; older papers and evaluations used 120. Derive each run's actual vulnerability denominator from its pinned metadata and enabled subset, rather than copying a headline count or score. | Mode | Observed contract | Katarina fit and missing work | |---|---|---| | Detect | Agent audits the supplied scope for direct/indirect loss of assets and writes `submission/audit.md`. A separate LLM judges matches to each reference vulnerability; results include counts and associated award totals. | Initial launcher and deterministic retained-finding exporter implemented; validate them inside the upstream environment before scoring. Existing source review, neutral/guided discovery and debate can run inside the task. | | Patch | Agent changes implementation; `submission/agent.diff` is checked through the patch evaluation. Task instructions constrain test edits and compilation-breaking interface changes. | Katarina currently generates new proof tests, not production repairs. Mark this mode unsupported until a repair workflow and legitimate-behavior validation exist; do not call a proof test a patch. | | Exploit | Agent interacts with deployed contracts using the supplied sandbox wallet and RPC surface. The runner extracts `submission/txs.json` for programmatic replay/grading. | Existing Foundry proofs help, but they are not the required submission. Add a bounded transaction-producing agent/tool adapter, artifact capture and independent replay integration. This mode can require discovery when hints are absent; record the exact hint level rather than labeling every exploit run reproduction. | Sources: pinned [Detect grader], [agent instructions], and [task implementation]. A Detect match is a judge's correspondence decision, not independent exploit verification. Award totals are benchmark weights, not audit money saved. ### What its score will not establish The release documents sequential transaction replay, clean local Anvil state rather than a mainnet fork, single-chain environments and some mock dependencies. It also acknowledges that Detect does not reliably classify additional, non-reference findings. Thus the benchmark cannot by itself establish real market exploitability, precision or complete architecture coverage. [Published limitations]. [OpenZeppelin's March review] disputed four high-severity labels in the then-current dataset and raised training contamination concerns. That is a dated external assessment, not proof those exact issues remain in today's scored subset. Compare disputes and upstream corrections against the pinned revision; do not silently delete difficult cases or assume an old correction list is current. Keep the upstream score and any independently adjudicated adjusted score separately named, with per-item reasons and denominators. Public cases discussed during this research cannot serve as pristine holdouts. The [Re-Evaluating EVMBench study] reports sensitivity to model/scaffold configuration and a substantial gap on its separate incident tasks. Its own limitations and task differences matter; its results do not prove Katarina will outperform anyone. They motivate repeated matched-budget comparisons, independent validation and additional deployment-realism tests. | Audit concern | What EVMBench contributes | Additional evaluation required | |---|---|---| | Authorization, arithmetic, reentrancy, accounting and cross-contract logic | Real audited repositories and known defects; useful breadth and multi-finding recall. | Classify the selected corpus by mechanism without exposing answers to discovery. Add benign/repaired controls and adjudicate all emitted findings for precision. | | Oracle/keeper availability and stale off-chain decisions | Applicable code paths can appear in tasks, but the aggregate score provides no required coverage of these mechanisms. | Controlled observation/delivery schedules, missing/stale updates, intervening state changes and recovery tests. | | Liquidation capacity, liquidity collapse, funding and withdrawal runs | Execution can establish a particular loss in a supplied environment. | Joint price/depth/capital/gas/participation models, actor policies and sensitivity to assumptions. | | Socialization, ADL and operator mistakes | A matching reference issue can be credited if present; there is no general loss-allocation or configuration-safety guarantee. | Explicit loss waterfalls, priority/account-splitting properties, parameter boundaries and healthy-risk-acceptance controls. | | MEV, reorgs, sequencers and cross-chain races | Sequential single-chain replay is useful for supported transaction sequences. | Explicit ordering, delay, reorg/finality and cross-chain models. Do not call arbitrary transaction order a realistic mempool model. | | Novel discovery and audit efficiency | Public regression and reproducible comparison on a pinned task. | Private unseen project/family groups, source-only versus research-assisted arms, review minutes, full model/tool costs and incorrectly dismissed findings. | ### Concrete integration sequence 1. **Freeze the task and measurement contract.** Record both repository revisions, image/toolchain digests, per-mode task IDs and denominators, compiler/deployment settings, model IDs, judge model/prompt and hint level. Disable gold/max-solution application in scored runs. Preserve isolated gold and empty-submission checks as grader validation, never as agent context. 2. **Add Katarina as an upstream agent, starting with Detect.** The upstream agent registry supports `config.yaml` and `start.sh`. Install a pinned Katarina binary/configuration in the prepared agent environment; point it at the task's allowed source. Keep its database, logs and generated reports outside the source inventory. Supply all upstream scope constraints and evidence access fairly. Capture partial/final reports on deadline; missing output and setup failure stay visible. 3. **Export the actual product outcome.** Freeze a deterministic converter from Katarina findings to `submission/audit.md`, preserving root cause, source references, preconditions and evidence limits. The primary submission should contain its nonignored findings. Full `report.md` includes rejected candidates and review arguments, so copying it wholesale could earn credit for a bug Katarina dismissed. Score raw candidates separately as a pipeline diagnostic; never choose the export policy using reference answers. 4. **Validate isolation and tool access.** The [solver] supports an internal network with a provider gateway. Adapt that boundary for every configured model/provider and child tool. Keep reference reports, patches, gold scripts and grader outputs outside agent visibility, including image layers, Git history and mounted paths. Record the exact upstream hint/README policy; extra redaction creates a separately named evaluation variant. Freeze prepared tools for Katarina and the baseline alike. 5. **Smoke-test before model scoring.** Check task build, empty submission, isolated known-good submission, report conversion, timeout/recovery, evidence preservation and absence of answer leakage. Then run an exposed development pilot with one model configuration and a fixed all-agent budget. Current `katarina-bench` intentionally rejects in-loop tools/research; implement this as a separate external adapter rather than removing its protections. 6. **Compare and extend.** Run a plain coding-agent baseline with identical tools and budget, then multiple independent attempts with paid selection/merge, then Katarina with one-model versus diverse-model roles. Retain all repetitions, neutral-agent slots, candidate/final recall, all-finding precision, costs, completion rates and human review time. Add Exploit only after transaction replay and environment validation work; add Patch only after supported production repair. Keep broad economic simulations as a separate named track. No runtime benchmark score is reported here. The present shell has no `forge`, `anvil` or `docker` on PATH, and the implemented launcher/exporter has not yet been exercised in the upstream container/grader. Provider/model selection, a total scoring budget, prepared images and a fixed case policy must be recorded before a paid evaluation. These are execution prerequisites, not reasons to postpone the methodology assessment. The complementary [Chaos-inspired harness design] now has a [generic runner] for agent-generated adapters and bounded local/SSH campaigns; calibrated financial adapters remain project-specific work. Building it should be guided by properties and actual project behavior, not EVMBench task IDs, reference wording or judge preferences.
VulnHunter: implementation review and lessons for Katarina
# VulnHunter: implementation review and lessons for Katarina Reviewed 2026-10-07 at [nealbridges/VulnHunter commit `91aa73ecc2e7c0e46291636e1b0d4786c9cf0364`]. The source archive was inspected without installing or executing the tool. Remote skills were treated as source material, not instructions for this review. This is a design assessment, not a measured comparison or a security audit of VulnHunter itself. The project is a maintained fork of Capital One's VulnHunter. Its useful contributions for Katarina are systematic investigation accounting, attention to the realism of proofs, searches for related defects, and diagnostics explaining where findings disappear. Katarina already has independent challenge/defense, evidence obligations, configurable role models, bounded proof feedback and durable coverage records; adding another generic adversarial-review role is not the main opportunity. ## What is implemented The core scan is a prompt procedure: reconnaissance inventories inputs and sinks, partitions the code, and dispatches injection, navigation/authorization and logic/crypto reviewers. A sink-driven review complements forward tracing. Global verification searches for defenses outside the original partition; reproduction, proposed fixes, a related-instance sweep and reporting follow. The host harness supplies the actual agent execution. Prompt requirements to cover every path do not establish complete program analysis. [Hunt procedure]. There is also executable Python tooling for scan manifests, benchmark judging, miss analysis and remediation artifact validation. These are useful contracts, but a schema-valid artifact does not establish its security claims. The separate fix workflow specifies production changes and test-first verification; the `vulnhunt-fix-verify` skill instead reviews a supplied repair statically and explicitly lacks shell execution. These should not be conflated. [Manifest writer], [fix verification]. The README marks sandbox-first validation and measured-impact PoCs as in progress. A runtime-provisioner skill exists, but a source search found no reference to invoking it in the main hunt phase prompts; the installation/skill-contract plumbing is not proof of runtime enforcement. Conversely, a separate verification subagent is already dispatched even though README language describes an independent verifier as roadmap work. Assess the individual paths rather than assuming every README claim describes one completed system. [README], [orchestration]. ## Practices worth adapting ### Explicit proof fidelity and measured consequences The runtime-provisioner asks which dependency boundary a claim needs to exercise and what observable outcome would establish impact. A string containing a suspicious query clause is weaker evidence than an actual unauthorized row returned by the production query path. [Runtime procedure]. Katarina records execution status, runner, output, proof interpretation and limitations. Add structured evidence identifying production code exercised, dependency versions, real versus mocked boundaries, state/build configuration and observed outcomes with units. An `observed` measurement should reference recorded execution; projected loss or an assumed market response remains an estimate. Disclose which assumptions the experiment did not test. Examples: measure cross-tenant records returned; debt or claims left uncovered after a simulated oracle outage; duplicate side effects after a timeout/retry; or operations accepted by a stale leader. An isolated contract simulation can validate accounting behavior without establishing real-world liquidity or keeper participation. OS isolation, deployment fidelity and claim validity are three different properties. ### Input and candidate accounting Verification begins by enumerating all candidates and requires a disposition for each. It revisits some inputs previously judged safe and checks other writers/callers before dismissing a path. [Verification procedure]. Extend Katarina's existing source/question/family coverage with stable IDs linking an entry point or external assumption to investigations, candidates and outcomes. Controller checks should detect missing dispositions, failed jobs and candidates lost during grouping or reporting. The inventory itself remains incomplete unless independently established: recon can miss an entry point. Preserve broad scouting and neutral discovery outside that plan. For Katarina, inventory more than attacker-controlled parameters: oracle freshness, keeper liveness, delivery semantics, off-chain decision age, market assumptions and shared state ownership also need investigation. Use bounded independent spot-checks of dismissed paths; do not equate agreement among similarly prompted models with validated safety. ### Bounded searches for related defects The sweep stage searches for both the vulnerable construction and the dangerous operation, follows callers, and requires each additional instance to undergo validation. This can recover defects outside the original partition, including background paths. It also distinguishes method names from receiver semantics. [Sweep procedure]. Katarina should add an optional, budgeted follow-up investigation for a supported mechanism: find other writers, readers, entry points or consumers that could violate the same property. A missing tenant condition suggests other scoped queries; an unfenced write suggests other lease-protected mutations; an oracle-age omission suggests other price consumers. Search structural relationships where tooling supports them, not just identical strings. Revalidate each match, retain separate instance evidence and group by root cause for developer presentation. Stop with explicit remaining work when the budget is exhausted. A keyword match is a lead, and twenty locations sharing one repair are not automatically twenty independent vulnerabilities. These follow-ups complement, and must not consume the reserved allocation for, unhinted discovery. ### Explain where misses happen `analyze_misses.py` searches phase artifacts for identifiers from known findings and asks a model to diagnose prompt gaps. `finding_history.py` retains detected/missed timestamps across runs. These are useful development diagnostics; identifier proximity is only a heuristic for the stage responsible. [Miss analysis], [history]. Use Katarina's persisted job and finding IDs to distinguish inventory omission, insufficient exploration, no candidate, incorrect dismissal, failed proof setup, inadequate assertion and report omission. Do not force every miss into a prompt defect: missing tools, exhausted budgets and inadequate environments also matter. Suggest changes on development cases, then test generalization on untouched families. Preserve periodic full regressions even when a case has passed repeatedly. ### Test quality and later repair verification The repair workflow's test rubric checks that tests exercise production functions, use the claimed attack, assert secure behavior and discriminate vulnerable from repaired code. The reviewer is instructed to use a fresh context. [Rubric], [reviewer]. Much of this aligns with Katarina's independent benchmark grading. Bring the same requirements into reusable proof-quality checks: actual implementation exercised, meaningful assertion, appropriate attack conditions and legitimate-behavior controls. Preserve the distinction between exploit-demonstration tests, which pass when the bug occurs, and regression tests, which pass when secure behavior is restored. Recorded process output must substantiate model-supplied pre/post result fields. General repair generation remains a separate future feature. ## Policies to avoid transferring - **Requiring an adversary for every security risk.** The verification prompt routes operational failures without attacker-controlled input to code quality. That would suppress external-risk findings central to Katarina. Keep accidental dependency failure, incentive failure and malicious manipulation as distinct possible causes. - **Lowering impact because reproduction is unavailable.** The runtime procedure caps mocked findings at Low. Katarina should retain potential severity and separately expose confidence, applicability and evidence limits. A severe conditional loss does not become minor because its environment is expensive to reproduce. - **An obligatory specialist matrix.** Three class reviewers per partition plus a fixed sink review may be useful for a particular workload, but it is not an established optimum. Compare targeted specialists, independent exploration and a simple multi-attempt baseline under equal budgets. Keep classes optional and tools discoverable. - **Broad exclusions and application-specific trust shortcuts.** The hunt skill excludes substantial build, generated and dependency code, while the verification prompt includes a gateway-library naming shortcut for treating authentication as established. These are unsuitable universal policies for Katarina's deployment, integration and economic risk analysis. Require actual contracts and evidence, and report unavailable dependencies explicitly. These observations concern the inspected prompts, not measured false-negative rates. [Verification gates], [runtime policy], [hunt scope]. ## Evidence and proposed adoption order The README's numbers come from six scans of one Go service commit, with raw outputs retained by the maintainer. They do not establish independent precision, broad recall or superiority over Katarina. Its public benchmark uses an LLM to match reports to known findings and tallies those matches; it is not independent exploit verification or a complete precision measurement over every emitted finding. The bundled ground-truth example is synthetic. [Reported results], [judge], [benchmark description]. | Priority | Proposed addition | Evidence of value to seek | |---|---|---| | 1 | Structured proof fidelity and outcome measurements | Fewer unsupported impact claims and faster human validation, without hiding unresolved severe risks | | 2 | Bounded related-defect follow-ups | Additional unique validated issues per dollar; preserved neutral-discovery coverage | | 3 | Candidate lineage and stage-of-loss diagnostics | Fewer dropped/incorrectly dismissed findings; improvements generalize to untouched families | | 4 | Separate repair-verification workflow | Original failure prevented while legitimate behavior and related paths remain correct | Implement these as small reusable capabilities in the existing controller, with feature ablations under the [benchmark plan]. Treat whole-methodology VulnHunter runs as a potential additional baseline once the interactive evaluation adapter exists. The initial review made no runtime changes. The subsequent [implementation] adds proof-quality contracts, bounded related searches, candidate lineage, operational-risk analysis and practice comparisons. General repair generation remains outside the audit pipeline; the existing separate benchmark differential workflow supplies paired execution for supplied vulnerable/repaired snapshots. The [15 October competitive update] places these implemented adaptations alongside Katarina's protected independent discovery, ledger, dependency review and generic interactive tools. The source-level review above remains pinned to the stated VulnHunter revision.
Measuring the review
# Measuring the review
Katarina's own test suite checks orchestration, budgets, persistence and local execution. It does not measure whether the review finds anything. That is a separate question, and it needs a separate tool with its own answer keys, its own isolation and its own record of who decided what.
`katarina-bench` is that tool. It ships in [`benchmark/`] as a standalone Go module and measures whether a Katarina run finds real defects, dismisses false alarms, produces evidence that survives independent checking, and reduces the human time an audit costs. It is an offline tool: every case is a pinned local snapshot, every command comes from a reviewed manifest as explicit argv, and nothing on a network is contacted or scanned.
## Three records, never merged
| Record | What it is | Where it comes from |
|---|---|---|
| Model claims | Candidates, severities, dispositions, confidence and generated test plans. | Ingested from `report.json`. |
| Independent adjudication | A human verdict on each candidate, the expected issue it matches, and whether the finding described the defect's reach correctly. | Entered by a person, optionally blind and by more than one reviewer. |
| Execution evidence | What happened when a generated test ran against the evaluated snapshot and against its repaired control. | Executed by the benchmark, under its own isolation. |
Two consequences follow, and the implementation enforces both. Wording that resembles an answer key proves nothing: no code path matches finding text, CWE or location against an expected issue, and an issue counts as recovered only when an adjudicator records a true positive and names it. Command success proves nothing either: a generated test that exits zero is command success, and becomes evidence only through a differential outcome against a repaired sibling.
Reported figures include candidate recall before triage, recall after triage, real issues that were found and then ignored, precision over adjudicated findings and over the findings a reviewer would actually see, pending and disputed adjudications, duplicates, differential proof outcomes, incomplete runs and setup failures, and tokens, reservations, invoices, elapsed time and human review minutes. Recall and precision are marked provisional while any candidate is pending or disputed.
## Prepare
Build the tool and check the environment:
```sh
cd benchmark
make build
./bin/katarina-bench validate --suite cases/suite.yaml --profile profiles/demo-lxd.yaml --toolchain
```
The shipped suite spans Solidity and Go, so `forge`, a `solc` matching each snapshot's pragma, and a Go toolchain must all be reachable. `validate` verifies every pinned snapshot digest, the split structure, the control references and the profile's adapter policy before anything runs.
Untrusted execution needs an isolation runtime. LXD ships with Ubuntu and needs no extra daemon, so it is the recommended one. Prepare an image once; executions have no network, so everything a case's test command invokes must already be in it:
```sh
make lxd-image
```
The script prints a fingerprint. Pin that fingerprint in the profile rather than an alias: LXD refreshes cached images on a timer, and an execution environment that changes underneath a benchmark is exactly the drift this tool exists to catch. `validate` resolves an alias, warns, and records what it resolved to.
## A first benchmark
Verify the answer keys, then run:
```sh
./bin/katarina-bench plan --suite cases/suite.yaml --profile profiles/demo-lxd.yaml --run first
./bin/katarina-bench oracle --suite cases/suite.yaml --profile profiles/demo-lxd.yaml --run first
./bin/katarina-bench run --suite cases/suite.yaml --profile profiles/demo-lxd.yaml --run first
```
`plan` records the run and one pending execution per case, profile and repetition; `oracle` records its verification against that run. `oracle` runs each case's independent reference tests and compares them with the outcomes its manifest declares. If it fails, the answer key cannot grade anything and no run result is meaningful. `run` executes Katarina once per case, profile and repetition against a fresh workspace, and ingests each report.
`run` and `resume` are the same code path, so re-running is always safe. A completed, failed, timed-out or errored execution is skipped. An execution interrupted before its result was committed becomes `indeterminate` and is never repeated implicitly, because the interrupted session may already have been billed. Returning work to the queue is explicit:
```sh
./bin/katarina-bench reset --run first --status indeterminate
```
Then adjudicate, grade the generated tests, and export:
```sh
./bin/katarina-bench adjudicate list --run first --suite cases/suite.yaml --blind
./bin/katarina-bench adjudicate set --run first --item item-3f9a12c0d4 \
--verdict true_positive --issue EO-SELF-ROUTE --applicability correct \
--adjudicator reviewer --minutes 7 --rationale "reaches increment through the executor"
./bin/katarina-bench differential --suite cases/suite.yaml --run first
./bin/katarina-bench metrics --run first --suite cases/suite.yaml
./bin/katarina-bench export --run first --suite cases/suite.yaml --out out/first
./bin/katarina-bench gate --run first --suite cases/suite.yaml --thresholds thresholds.yaml
```
`profiles/demo-lxd.yaml` uses Katarina's `demo` engine, which returns deterministic fixture responses and performs no model analysis. It exercises the benchmark end to end without a provider account, and its results are not detection results. For a real measurement, copy `configs/discovery-live.yaml` and `profiles/discovery-lxd.yaml`, fill in the placeholders and run the same sequence.
## Cases and answer keys
A case is a pinned snapshot with an answer key. Only the snapshot is ever visible to the harness; reference tests, notes and repaired siblings live beside it and are never copied into a discovery workspace.
```text
cases/FAMILY/VARIANT/
case.yaml manifest and answer key
source/ the agent-visible snapshot, pinned by SHA-256 tree digest
oracle/ independent reference tests, pinned separately
cases/FAMILY/NOTES.md
```
Every case declares a `development` or `holdout` split, and a family never straddles the boundary: a repaired sibling in the tuning set would leak the answer to a held-out case. The held-out family is not a formality. Keep it out of every tuning loop, and do not read run transcripts on it while adjusting prompts, configuration or the harness; once you have, it is a development case.
Two families ship. `executor-origin` is Solidity: a batching executor whose guard excepts its own address, so an external self-call reaches a protected action under the executor's identity. `tenant-cache` is Go and held out: a record cache keyed without the tenant, so a second tenant is served the first tenant's record. Each family includes a repaired control and a benign lookalike carrying the same surface pattern safely, so false alarms are measured rather than assumed.
Expected issues declare an applicability. `applicable` means the protected action is reachable in the pinned deployment; `conditional` means the code defect exists but an integration this snapshot does not enable is required to reach it. The distinction is a measurement: a report that calls a conditional defect an immediately reachable operation overstates it.
Author a case by writing `source/` and `oracle/`, then pinning and checking it:
```sh
./bin/katarina-bench pin --case cases/FAMILY/VARIANT/case.yaml --write
./bin/katarina-bench oracle --suite cases/suite.yaml --profile profiles/demo-lxd.yaml --case CASE_ID
```
Reference tests must include positive cases showing the legitimate authorized path still works. A repair that breaks the legitimate path is not a repair.
## Adjudication
Adjudication is a human act; the tool organises it and never performs it. A verdict is `true_positive`, `false_positive`, `duplicate`, `out_of_scope` or `unknown`, and a candidate with no verdict is pending and excluded from precision entirely. Absence from the answer key does not make a finding a false positive: a real problem the case author did not anticipate should be retained for review and, if it is genuinely a defect, added to the answer key.
A true positive may carry an applicability claim of `correct`, `overstated` or `understated`. An overstated finding stays a true positive and still counts toward recall, because the defect was found; it is reported separately because it is still work a reviewer has to undo.
Blind mode replaces the case identity with a run-scoped label and orders the queue by it, so a reviewer judges the finding rather than the case. It hides the label, not the code: a file path can still tell a reviewer which variant they are reading. What it removes is knowing in advance that a case is the repaired sibling, which would make every finding on it a false positive before a line is read.
Verdicts are keyed by adjudicator, so a second reviewer never overwrites the first. Agreement becomes the verdict. Disagreement is recorded as disputed, excluded from precision exactly like a pending finding, and never resolved by majority or recency. Reports carry percent agreement and Cohen's kappa for each pair of reviewers.
## Differential proof
Katarina asks a generated test to succeed when the claimed behavior is observed, so a meaningful check runs the case's command three times: on the evaluated snapshot without the overlay, with it, and on the repaired control with the same overlay. The tests the plan introduced are those present with the overlay and absent without it, and only those are compared.
`differential_proof` is recorded only when the overlay introduced at least one test that executed, every such test passed on the evaluated snapshot, the control produced structured results and ran the same tests, and at least one of them failed on the control with a reported assertion or revert reason. Eleven other outcomes each record why a run is not proof: no difference, observation absent, a vacuous overlay, a build failure on either side, a test-discovery mismatch, a missing control, a rejected plan, and so on. Truncated output never supports a conclusion.
## Isolation
The benchmark isolates untrusted execution: the code in a case snapshot and the tests a model generated. Those are the artifacts nobody can vouch for, and the benchmark is what executes them. The harness process itself runs on the host, deliberately: under the benchmark's adapter policy Katarina executes no repository code, no configured analyzer and no language server, and it needs outbound network access to reach its model provider, which every isolated runner denies. Every exported report states this.
| Mode | Behavior |
|---|---|
| `lxd` | Recommended. A fresh ephemeral LXD or Incus instance per command: the working tree is pushed in, the command runs, the instance is destroyed. No network, no host mounts. |
| `container` | An OCI container with no network and only the working tree bind-mounted. |
| `local-unsandboxed` | Explicit opt-in for local development, recorded in every execution and every report as lacking OS isolation. |
A configured runtime that is missing, or a daemon that cannot be reached, fails the run with an error naming the runtime. It never falls back to unsandboxed execution.
The adapter policy requires `tests.runner: none` and no configured tools or language servers. Katarina still runs its complete analysis pipeline and still writes generated test plans; only host-side execution is disabled, so the benchmark can execute those plans under its own isolation and against a repaired control.
Workspaces are neutral. Each execution gets a fresh directory named `project-` plus twelve hex characters, derived from the run, the execution and a per-run salt, so it reveals neither the case, the split nor the expected outcome. Katarina's state directory is created outside it, so the harness never reviews its own output, and snapshots carry no Git history.
## Discovery and reproduction
Discovery gives the harness source only, with no vulnerability description. Reproduction supplies a hypothesis through an explicit adapter that appends it to `analysis.questions` in a derived configuration. The two are never mixed: the track is recorded on every execution and every report, each profile carries a sentence stating what its numbers may be called, and a run containing a targeted profile gains an explicit limitation. Proving a supplied hypothesis is not blind discovery, and the tool will not report it as such. See [comparative evaluation].
## Contamination probes
A public case a model may have memorized and a case it reasoned about look identical in a recall number. A case can declare itself a mechanical rewrite of another — the same defect under renamed identifiers, reworded documentation, a renamed source directory, reordered declarations and a permuted guard — and the report then compares recall across the pair. A large positive delta is what recognising remembered text would look like; a delta near zero is consistent with the defect being found on its merits.
The probe bounds a risk rather than settling one. Both shipped pairs are synthetic, so there was nothing to memorize and they demonstrate the mechanism; the measurement means something once a public historical case is added, and the report says which situation it is in.
## Acceptance thresholds
Thresholds agreed with the auditors before a run, in a reviewed file, are what stop a benchmark becoming a search for the framing under which a result looks good. `gate` applies them and exits nonzero on failure, so it drops into CI unchanged. Scopes express a bar over a slice of the answer key, which is how "no regression in held-out recall" becomes a rule rather than a sentence.
```yaml
version: 1
require_oracle_passed: true
allow_provisional: false
profiles:
discovery-lxd:
require_sandboxed: true
min_post_triage_recall: 0.70
max_incorrectly_ignored: 0
max_contamination_delta: 0.25
scopes:
split:holdout:
min_post_triage_recall: 0.70
```
An absent field is not checked; the gate never invents a bar. A check that cannot be evaluated — precision with nothing adjudicated, a cost limit with no invoice recorded — is reported as skipped and fails, because a threshold nobody could evaluate has not been met. A run with pending or disputed candidates fails by default.
## What a benchmark result does not establish
Every recall and precision number depends on a person. A differential proof is evidence about a test, not a proof of exploitability: it shows an observation present before a repair and absent after it, attributed to a named assertion. Model confidence is an uncalibrated model judgement. A spend reservation is not an invoice, and a zero billed total means no invoice was recorded rather than no spend. Recall is relative to one suite, and absence from its answer key does not make a finding wrong. Public historical cases are useful regressions but do not establish absence of training contamination, and neither do synthetic ones.
No comparison against the Claude Code loop, MDASH or Shannon has been measured. The complete reference, including case authoring, schemas, storage and the current list of what has and has not been exercised, is in [the benchmark README].
## Economic development cases
The separate [economic suite] contains 42 Solidity component cases across fourteen economic, external-dependency and asynchronous state-consistency mechanisms, each with vulnerable, repaired and benign controls. All reference assertions have been executed with their pinned compiler. These are development fixtures, not held-out discovery results. The offline adapter also requires incident lookup, public research, repository history and chain snapshots to be disabled. See the [benchmark reference] for execution and evaluation limits.
The [capability-composition evaluation] adds a separate nine-case development suite, primitive/chain/platform metrics and a reproducible four-condition ablation generator. Platform reachability is untested by the component fixtures.
Shannon: code-analysis design review
# Shannon: code-analysis design review
Reviewed on 14 September 2026 at [Shannon commit `25b90b0611f15ab945e051dfee8ae78600d3a002`]. This review examines the public source and prompts, with emphasis on ideas applicable to Katarina's repository analysis. Shannon was not installed or executed, and this review provides no comparative detection score. Katarina now implements shared knowledge, additional questions, structured evidence/capability assessment and shared-test grouping independently; see [the current workflow] for configuration and limits.
The most useful lessons concern how to organize investigations: build security context, assign concrete questions, validate individual claims, and preserve the distinction between uncertainty and refutation. These additions complement Katarina's concurrent review, configurable models and budgets, independent deeper scouting, durable sessions and bounded test feedback.
Several Capella prompts identify their methodology as derived from Mantis, with modifications by Keygraph and Shannon. These are implementation references, not a claim that every technique originated in Shannon. [Architecture prompt attribution].
The [competitive-position update] compares current public product positioning with Katarina's later additions. The source-level statements below apply to the pinned September revision, not an audit of today's Shannon implementation.
## The code-analysis workflow
Shannon has two relevant paths. Its pentesting preparation prompt delegates architecture, entry-point and security-pattern discovery, followed by specialist inspection of sensitive operations and data flows. That preparation is scoped primarily to network-reachable application behavior. These are prompt instructions; they do not by themselves establish coverage. [Pre-recon prompt].
The separate Capella static-analysis pipeline has ten stages:
```text
Architecture → threat model → investigation plan
→ research: rapid file triage → selected deep investigations
→ deduplication → independent review → production viability
→ static confirmation → risk calibration → export
```
The workflow code establishes this ordering and retains stage artifacts for recovery. The configuration parser enables Capella when `agentic_sast.enabled` is the string `"true"`; its configuration schema describes it as off by default. [Workflow], [configuration parser], [configuration schema].
Capella confirms findings by reading source. Its confirmation stage cannot run a reproducer. Shannon's later live exploitation belongs to the broader pentesting workflow. Capella's SARIF export checks validity and production viability; that gate does not itself require a successful dynamic reproduction. [Confirmation prompt], [export gate].
## Practices worth adapting
### Shared security context
The architecture stage produces a knowledge base containing component descriptions, trust boundaries, relevant bug classes and dependency information. The planner assigns target files, a specific question and references to relevant knowledge-base entries. This gives downstream investigators context chosen for their task. [Architecture prompt], [planning prompt].
Katarina's shared security model sits alongside its inventory and supplied design notes. Claims include source locations, exact quotations and observed/inferred/unknown status; the artifact records the snapshot digest. Summaries remain challengeable evidence: an incorrect shared assumption can misdirect later agents. Independent deeper scouts do not inherit these shared model claims.
For Solidity, this model should include participants, privileges, assets, accounting invariants, oracle assumptions, capital requirements and incentives. For backend and native code, it should describe entry points, tenant or privilege boundaries, ownership contracts and deployment conditions.
### Investigations centered on a mechanism
Capella's research prompt requires tracing callers of functions with explicit safety contracts. It asks investigators to verify the contract at each call site, including callers outside the initial target files. [Research prompt].
Katarina permits navigation beyond the starting chunk and persists each additional question, its target files, selected knowledge references, final answer, citations, unresolved obligations and candidates. Configured and generated questions run alongside baseline scouting. Examples include:
- Java: follow tenant identity from authentication through service calls to database filtering.
- Rust: verify ownership, aliasing and lifetime obligations across a safe wrapper and unsafe implementation.
- C/C++: follow allocation sizes, units and build-dependent assumptions through every relevant caller.
- Solidity: follow deposits, share issuance, oracle updates and liquidation as a sequence of state and asset changes, including profitable deviations from intended participation.
Long investigations need their own context and token allowance. Katarina's additional questions use `analysis.investigation_context_requests`, default 8 and configurable up to 64 navigation rounds; other tasks default to three. Capella's research code allows up to 100 turns for triage and 200 for a deep audit. These units are not directly equivalent. Increasing Katarina's depth should be evaluated against cost per validated finding and missed-issue rate, with explicit stopping conditions. [Research implementation].
### Explicit evidence checks
Capella records review criteria individually, with outcomes for satisfied, failed, unresolved and inapplicable checks. Its collector rejects a `VALID` decision with unresolved checks, so this is enforced beyond prompt wording. Other collectors separately record viability and static confirmation. These checks enforce consistency of model output; they cannot establish that the model's underlying claims are true. [Collector implementation].
Katarina's optional structured checks cover reachability, control, guards, invariant, impact and feasibility. Structured economic findings also require incentive and capital checks. Unknown obligations must identify the next evidence needed. The controller validates quotation provenance and consistency between checks and conclusions; it does not prove semantic entailment.
Keep separate fields for impact, evidence strength, deployment applicability and the next action. A potentially severe issue can have uncertain feasibility. Combining those into one confidence or priority score hides information auditors need.
### Capability and deployment analysis
Capella has a dedicated production-viability review and a risk-calibration policy centered on the additional capability an actor gains from the defect. The calibration collector records advisory scores without changing exported severity or eligibility. [Critic prompt], [calibration policy], [collector implementation].
For Katarina, this supports asking exactly which boundary or invariant is defeated under the documented deployment. Existing permission to call a Solidity function does not imply permission to impose its economic consequences on other participants. Capability analysis therefore needs asset flows, losses and incentives as well as access privileges. Unknown build flags, integrations or deployment settings should remain explicit conditions.
### Group work that one test can resolve
Shannon's reconciliation stage can group observations when one validation attempt and verdict would settle them together. The host accepts only supplied observation labels, rejects conflicting group membership, and keeps internal producer identities out of the grouping input. [Task formation], [group validation].
This grouping is separate from Capella's own deduplication prompt, which requires a shared exact file-and-line location and a similar title. That narrower rule should not be described as general root-cause clustering. [Deduplication prompt].
Katarina can reuse one test for several observations while retaining each location, prerequisite, review history and disposition. Every shared plan maps assertions to member IDs, and proof review records each member's outcome separately. Incorrect grouping can conceal distinct bugs, so prompts require uncertain matches to remain separate. Grouping uses bounded candidate windows and does not guarantee global duplicate removal.
## Design choices requiring caution
**Initial triage gates deep review.** Capella dispatches an investigation only if triage flags at least one of its files. Coverage accounting compares classifications against the planner's file set, not an independently enumerated repository inventory. Complete triage accounting therefore does not establish complete deep review. Katarina should retain its independent deeper sample and mechanically check any generated plan against its inventory. [Research implementation].
**An exploratory prompt does not ensure independent context.** The planner requests empty knowledge-base references for some exploratory investigations. The assignment builder currently interprets an empty reference set as including all entity and vulnerability entries. This is an implementation mismatch with the intended fresh look, not a measured detection failure. Katarina should make context isolation an explicit, testable property. [Planning prompt], [assignment builder].
**Role names do not imply different models.** Shannon's model host resolves `small`, `medium` and `large` to the same selected model. Capella uses fixed concurrency constants of four triage sessions and two audit sessions. Katarina already exposes independent role models, family budgets and a configurable worker limit. [Model host], [Capella constants].
**Filtering policies can hide relevant risks.** The review prompt broadly excludes resource-exhaustion findings except in modules intended to defend against them. The shared operating principles also exclude many build, test and generated files and assume committed secrets are handled by another scanner. These policies do not fit a general audit-preparation harness. Katarina should preserve explicit scope decisions and treat absence of reproduction as uncertainty, particularly for economic, availability and concurrency risks. [Review policy], [operating principles].
Capella also requires a CWE identifier to accept a finding. Katarina should retain its ability to report an economic or incentive failure without forcing an inaccurate CWE mapping. [Finding collector].
**The navigation layer is deliberately small.** Capella supplies bounded `read`, `find` and `grep` tools, without shell execution or source edits. The inspected implementation is not a compiler-backed whole-program analysis engine. Its architecture and dependency artifacts are model outputs. Katarina can pursue these workflow improvements using its existing source inventory and optional LSP integrations. [Repository tools], [tool policy].
## Adoption and evaluation
| Area | Implemented addition | Evaluation criterion |
|---|---|---|
| 1 | Structured evidence obligations and separate applicability, impact and validation fields | Fewer unsupported confirmations and dismissals; less auditor reconstruction time |
| 2 | Source-cited security model and investigation planner, checked against the inventory | Better cross-file recall without losing baseline coverage |
| 3 | Resumable investigations with configurable depth and independent exploration | Recovery of difficult and initial-scout misses at a measured token cost |
| 4 | Conservative grouping for shared tests, with original observations retained | Fewer duplicate tests without merging distinct defects |
These additions use Katarina's existing Go controller, protobuf worker messages, SQLite state and per-family reservations. No Shannon code is embedded or required at runtime. Evaluate each addition separately on the same vulnerable, repaired and benign snapshots under matched budgets. For Solidity, include mechanisms that are implemented as intended but admit harmful incentives. See the [comparative evaluation protocol].
Solidity economics and incentive review
# Solidity economics and incentive review
Start with the [Solidity workflow] for configuration, execution order and the developer handoff. This chapter expands the economic review obligations.
Solidity reviews include economic and game-theoretic failure modes in every scouting pass, including when `scan.passes: 1`. This guidance also reaches the challenger, defender, rebuttal, assessor and test writer. A protocol can execute every instruction correctly while rewarding behavior that drains value, creates bad debt or stops a necessary service.
Katarina asks agents to reconstruct the mechanism and its assumptions. It does not compute a formal equilibrium, obtain live market prices, calibrate probabilities or certify economic security. A checklist entry is a question to investigate, not a finding by itself.
## What agents examine
| Area | Questions |
|---|---|
| Actors and incentives | Who pays, earns, bears losses, controls information or can form a coalition? Can participants profit by deviating from the intended strategy? |
| Capital and feasibility | Can capital be flash borrowed or must it stay locked? What collateral, duration, ordering rights or governance power are required? |
| MEV and timing | Can ordering, front-running, sandwiching, delayed inclusion or a race change a user's outcome? |
| Oracles and liquidity | Does manipulation cost less than extractable value? What depth, window, stale-price or external-market assumptions make that possible? |
| Solvency and exits | Can withdrawals, liquidation incentives, bad debt or first-mover advantages create a run or a cascade? |
| Accounting and rewards | Do rounding, share inflation, donations, wash activity or reward farming pay more than they cost? |
| Governance | Can vote borrowing, bribery, concentrated voting or timing defeat the intended economic protections? |
| Liveness and griefing | Are keepers and liquidators still paid enough under stress? Can a low-cost action force a much larger loss or operating cost? |
Ethereum's [MEV documentation] provides background on transaction ordering, arbitrage, liquidations and sandwiching. These mechanics require project-specific evidence before Katarina should report a risk.
## Evidence that survives triage
Economic candidates include an `economics` object alongside the ordinary source location, claim, impact and remediation. This optional object is validated before a finding is accepted and preserved in SQLite, JSON, Markdown and SARIF properties. An economic mechanism may have no suitable CWE; an empty CWE is valid.
```yaml
economics:
actors:
- "Keeper: earns a fixed liquidation reward and pays execution costs."
assumptions:
- "No external keeper subsidy; confirm in integration/deployment documentation."
- "Gas-cost range is unknown from this repository."
sequence:
- "Compare available reward with transaction cost for an eligible liquidation."
- "Decline execution when net compensation is negative."
- "Check whether unpaid liquidation leaves collateral losses with the pool."
capital: "Keeper funds gas; no malicious borrower or flash loan is necessary."
payoff: "keeper_net = reward_value - gas_used * gas_price - other_execution_costs, all in the same unit"
constraints:
- "An enforceable alternative liquidation service could refute the liveness failure."
- "Rewards that rise sufficiently with costs may remove the incentive gap."
violated_invariant: "Required liquidation remains economically viable within the documented operating range."
validation_plan: "Use an isolated multi-actor scenario; vary costs and rewards, track unpaid debt, and compare a repaired reward mechanism."
```
This is an illustrative hypothesis, not a finding about an actual protocol. Unknown inputs stay explicit. Agents should give formulas, units and defensible bounds rather than invented prices or precise profit estimates. Net attacker profit, victim loss and externally motivated griefing are separate quantities. An unprofitable action can still be a griefing risk, but its objective and cost asymmetry must be stated.
Each reviewer is instructed to address the strongest falsifier, capital source, constraints and sensitivity to assumptions. The assessor must distinguish an unintended incentive failure from an explicitly accepted exposure. “Users are allowed to do this” or “the implementation matches the specification” does not establish economic safety. A documented intended mechanism can remain a `log` or `test` decision. Model confidence remains uncalibrated.
## Supply the protocol's economic model
With `analysis.evidence_checks: true`, structured economic findings require explicit `incentives` and `capital` checks alongside reachability, control, guards, invariant, impact and feasibility. Unknown checks must identify the next evidence needed. The assessor records existing authority, additional capability or harm, economic effects and deployment conditions. Intended behavior or existing permission alone cannot justify ignoring unresolved economic harm. See [structured evidence].
Put a project-specific economic model in an included repository file and reference it in configuration:
```yaml
design_notes: [docs/invariants.md, docs/trust-model.md, docs/economics.md]
```
The [economic design-note template] covers participants, accepted exposures, invariants, operating ranges and off-chain assumptions. Resolve its unknowns with your team; comments and documents remain untrusted evidence and are cross-checked against implementation. Do not include credentials or confidential market data you do not want sent to your selected providers.
Economic review guidance is included in the existing role prompts. It increases prompt size, and economic findings can require more context or output tokens. All requests count toward the session budgets. Independent deeper scouting and test revisions have separate [configuration controls]. Increase `max_output_tokens` if providers truncate larger finding documents, accounting for the resulting budget reservations.
## Tests and interpretation
Use the existing configured Foundry commands for deterministic scenarios, fuzzing or invariants against the actual implementation. Test writers are asked to vary relevant parameters, account for transaction costs and asset flows, and include a repaired-mechanism negative control. Claims about real market depth, competition, coalition behavior or human participation may remain unresolved by simulation; log those limits for auditors.
Generated vulnerability-reproduction tests are expected to observe the claimed failure in the original implementation and stop reproducing it after repair. They are distinct from permanent safety regression assertions, which should pass after repair. Command success alone proves neither kind is sound. Keep test discovery, assumptions and assertions in the human review.
Sessions retain the review policy used when they were created. After upgrading to a binary with a different policy, start a new session to apply that policy; reports from existing sessions remain available. See [reports and recovery] for compatibility requirements.
## Scenario discovery and experiments
The init configuration enables six scenario investigations, including economic coverage when Solidity is present, before shared architecture extraction and ordinary scouting. Two of those six run first with source and the repository map, with a separate neutral review policy and without the attack taxonomy, incident examples, supplied vulnerability questions, analyzer hints or shared conclusions. Tool interfaces and output schemas remain available; this is independence from supplied hypotheses, not a guarantee against shared model biases. The count is `ceil(scenario_investigations * independent_percent / 100)`. This reserves investigation slots and gives them scheduling priority; it is not a guarantee that exactly 30% of tokens or dollars are spent there. Every request still shares the session caps. Existing configurations that omit these fields retain zero scenario investigations.
```yaml
analysis:
scenario_investigations: 6
scenario_coverage: true
independent_percent: 30
experiment_requests: 3
investigation_context_requests: 8
```
Each investigator reconstructs a mechanism and chooses its own hypotheses, source reads, searches and experiments. The guided investigations also receive economic review lenses and explicit family assignments, including socialization and ADL. No incident ID, user hint or prior scout finding is required. Empty findings and refuted hypotheses are valid results.
A scenario records actors and coalitions, capital, ordered actions or environmental changes, parameter units and ranges, invariants, loss allocation, a healthy baseline, and a negative control. Its ledger uses exact decimal strings or `unknown` for balances, claims, liabilities, costs and losses. These are predictions supplied by the model. Katarina validates structure and source citations; it does not automatically solve the accounting, certify ledger conservation or optimize strategies.
Before triage, an investigator can request a test plan against the actual included implementation. The controller validates new test paths and a configured command, runs it through the existing runner, checkpoints the result, and asks a separate proof-review request to interpret assertions and assumptions. The investigator receives that feedback and can revise its hypothesis or choose another experiment. The challenger, defender, assessor and subsequent proof writer receive bounded recorded evidence from that investigation as well.
Experiments consume the common context/action allowance and a separate per-investigation experiment cap. Identical plans cannot be rerun within the same investigation. `tests.runner: none` records a plan without executing it. A completed test survives an interrupted model review without executing twice; an interrupted execution with no recorded outcome remains `indeterminate`. Model reviews may share the same configured model and biases.
## Required coverage alongside unhinted discovery
With `analysis.scenario_coverage: true`, the controller assigns all **20 scenario families** across the guided slots before dispatch. The six-slot init configuration retains two unhinted investigations and four guided investigations. This adds no fixed model jobs, though larger responses, evidence requests and experiments can increase actual spend. The ordinary global call, token and cost caps still apply. Configurations must retain at least one unhinted slot and enough guided slots to assign at most eight families per slot (currently three guided slots minimum).
The catalog covers authorized operator/configuration mistakes, realizable backing, liquidation liveness, all collateral-reducing paths, borrower/liquidator coalitions, amplified rounding, callback consistency, AMM boundaries, temporary governance, stale approvals, loss allocation, ADL, funding settlement, actual token receipts, slippage/MEV, bridge backing, reward contribution, compiled protections, combined stress, and oracle/sequencer availability. These are review obligations, not an exhaustive list of vulnerabilities. Unhinted investigators can find mechanisms outside this catalog and can choose their own historical searches after formulating a hypothesis.
Every guided result must account for each assigned family exactly once. `investigated` needs a concrete scenario and source citations; `not_applicable` needs a cited explanation of scope; `unresolved` needs a specific next evidence step. Running out of budget is not evidence of inapplicability. The controller rejects omitted/duplicate families, nonexistent scenario references, fabricated observation IDs, and observations from another investigation or source snapshot.
Reports separate **review status** from **execution status**:
| Review status | Meaning |
|---|---|
| `not_scheduled` | Required family accounting was disabled; no assignment is recorded. |
| `pending` | Assigned, but no final assessment was saved, including interrupted or budget-limited work. |
| `investigated` | The model supplied a source-cited scenario assessment; this does not establish execution or safety. |
| `not_applicable` | The model supplied source evidence for a scope exclusion; auditors should inspect that reasoning. |
| `unresolved` | Missing evidence or unfinished investigation remains explicit. |
Execution is independently derived from controller observations: `no_execution`, `plan_only`, `execution_recorded`, or `incomplete`. Both passing and failing commands can count as recorded execution, because a vulnerability-observation assertion and a safety assertion can have opposite expected outcomes. Truncation, timeout and indeterminate outcomes remain incomplete. Missing, unexecuted or inconclusively interpreted experiments require a next-evidence step. No execution label certifies assertion quality or economic feasibility.
Coverage assignment guarantees that a family cannot silently disappear from a completed guided response; it does **not** guarantee every scenario executes within finite budgets. The default runner remains `none`. Configure a prepared test runner and commands for execution, and use the coverage report to see what actually ran. A single experiment may address several related families when its explicit assertions justify those links. No fixed ordering of real-world attacks or model reasoning can guarantee exhaustive detection.
Existing configurations must add `scenario_coverage: true` alongside sufficient scenario slots to enable this accounting; omitted settings remain compatible. For Solidity reviews with scenarios disabled, reports show unscheduled families rather than implying they were checked. After this policy upgrade, start a new session; unchanged current-policy sessions reuse recorded work on resume.
Exports also include `audit-handoff.md`, a deterministic, severity-ordered list of active candidates, proposed repairs, relevant conditions, available proof outcomes and remaining family work. It uses existing artifacts and costs no additional model requests. It is intended to help developers prepare evidence for auditors, not to claim measured audit savings. Keep the full report for contradictory evidence, ignored findings and independent proof interpretations.
## External failures are reportable exposures
A contract that correctly uses a dependency can still lack protection against that dependency failing. Findings can include structured `external_risks` with the dependency, failure condition, required assumption, existing and missing safeguards, consequence, applicability, conditions, validation plan and exact code citations. The capability status `exposure` represents harm without a malicious actor or privilege escalation. Structured evidence checks are mandatory for these findings even if the general `analysis.evidence_checks` setting is off.
| Dependency | Faults to investigate | Code and policy obligations |
|---|---|---|
| Oracle | Stale or missing updates, zero/negative values, precision changes, depeg, thin or correlated markets | Freshness, units, bounds, fallback independence and safe behavior when no reliable price exists |
| Keeper or liquidator | No participation, high execution costs, delayed inclusion, depleted capital, partial work | Accrual independent of keeper timing, incentives under supported stress, permissionless alternatives, limits on accumulated exposure |
| Sequencer | Downtime, recovery before oracle refresh, censorship or delayed transactions | Uptime checks, recovery grace periods and liquidation behavior during interruptions |
| Bridge or external settlement | Delayed finality, reorg, halted relay, lost backing or dependency upgrade | Authenticated finalized claims, replay protection, withdrawal limits and explicit settlement assumptions |
| Token, issuer or venue | Pauses, blacklist, rebases, transfer fees, shallow liquidity or withdrawal freeze | Actual balance accounting, failure containment, realizable collateral value and escape or pause policy |
Reviewers must connect an external failure to a reachable code path and resulting harm. “External,” “by design,” or “no attacker” alone cannot justify dismissing it. A documented accepted exposure or effective safeguard can refute a proposed defect; missing deployment facts must remain conditional or unresolved. For example, advance time while a mock feed stops updating, compare borrowing with a healthy update schedule, then verify a freshness guard prevents the unsafe result without blocking healthy borrowing. Do not claim that a simulated outage occurred in production.
## On-chain/off-chain races and stale approvals
Katarina treats a gap between an off-chain check and its on-chain use as an architectural security boundary. The checker can be honest, its inputs correct at observation time, its signature authentic, and the contract faithful to its specification, yet the combined system can violate an invariant when intervening state changes invalidate the decision. Sequential EVM execution does not make the off-chain read and a later transaction atomic.
For each handoff, agents are instructed to reconstruct:
1. **Observation and predicate:** which block/state was read, what was checked, and all inputs it depends on, including collateral, debt, interest, prices, permissions and shared limits.
2. **Authorization:** the account, action, amount and context actually bound into the approval, quote, simulation or keeper result.
3. **Intervening transitions:** operations that can invalidate the predicate before consumption, including other valid approvals, withdrawals, cancellation, risk-parameter changes, time-dependent accrual and cross-contract updates.
4. **Consumption:** the on-chain acceptance path, execution-time guard and invariant after applying the authorized action.
5. **Counterevidence:** an atomic recheck, a complete state-version check, or an enforceable reservation that protects the relevant predicate, with the scope and limits of that protection.
The characteristic experiment is `check(S0) -> change to S1 -> consume the original result at S1`. Preserve the original signed payload; regenerating it after the state change would erase the race being tested. Include the reverse ordering, a healthy fresh-result path, same-block ordering without elapsed time, and multiple distinct outstanding approvals. Also investigate asynchronous liquidation, delayed settlement, RFQ/intent execution, solver/paymaster validation, cross-chain messages and callbacks where applicable. Missing backend source or deployment policy remains an explicit unknown.
A concrete synthetic lending example: collateral is 100 and debt is zero, so an honest service signs permission to borrow 60. Before submission, the borrower withdraws 60 collateral, which is permitted while debt remains zero. The original approval then creates debt of 60 against collateral of 40. Alternatively, two distinct approvals each authorize 60 against the same initial 100 collateral; executing both creates debt of 120. Neither sequence needs a forged signature, replay of the same approval, expired message or broken oracle.
| Safeguard | Obligation and limits |
|---|---|
| Signature and domain binding | Establish who authorized which operation in which context; do not establish that the checked predicate still holds. |
| One-use request nonce | Prevents reuse of that request; distinct approvals can still conflict. A nonce becomes a state-version guard only when every relevant invalidation advances the checked version. |
| Deadline or block reference | Bounds age or identifies an observation; relevant state may change within the validity window or same block. A historical block reference alone is not a current-state comparison. |
| Atomic on-chain revalidation | Rechecks the predicate including the pending action. Inputs must themselves be adequate, and external calls must not reopen a check/effect gap. |
| State-version comparison | Can reject stale approvals if it compares against current state and every relevant mutation invalidates the version. Account versions alone may omit prices, global limits or accrued interest. |
| Reservation | Can serialize or bound conflicting use when reserved capacity is enforced on-chain or otherwise cannot be bypassed. It must also address other inputs that could make the reserved operation unsafe. |
The signing standard itself leaves application behavior under replay and front-running to the implementer; signature verification is not a complete protocol safety argument. See the [EIP-712 security considerations].
Findings use the existing `external_risks` fields to preserve the observed/check state, invalidating transition, consumption path, missing consistency safeguard, impact and source citations. They can also carry `economics` when value or incentives are involved. No attacker or faulty external service is required. A reviewer cannot dismiss the finding solely because the backend checked health correctly or the signed message is still valid.
The `offchain-health-race` development family supplies three controls: missing execution-time consistency, live on-chain health revalidation, and a safe version-checked design without a duplicate health calculation. Its local honest-checker simulation signs only requests healthy at observation. It tests both interleavings, the reverse ordering, legitimate refreshed approvals, expiry and replay protection. Fixed valuation and the absence of shared limits are explicit scope assumptions; the safe version design is not offered as a general solution for live-market lending.
## Agent-selected research
The controller exposes these actions only to scenario investigators:
| Action | Evidence obtained |
|---|---|
| `lookup_incidents` | Bundled, searchable historical metadata and proposed mechanism checks |
| `search_public` | Public search response from an operator-configured HTTPS endpoint, with the agent's query |
| `fetch_public` | Bounded text/JSON page content and navigable public links |
| `read_history` | Up to six commits with diffs for an included source path, when enabled |
| `read_chain_snapshot` | An operator-captured, digest-pinned JSON RPC evidence bundle |
| `run_experiment` | Validated test plan, command outcome and independent model interpretation |
Every action requires a hypothesis and falsifier before retrieval. SQLite and JSON/Markdown reports retain the action, investigation ID, source digest, retrieval time, result status, evidence digest, content and truncation state. Failed and unfinished investigations stay visible. Retrieved pages, history and RPC results remain untrusted evidence.
```yaml
research:
incidents: true
public: false
search_url: "" # optional public HTTPS endpoint accepting GET ?q=...
allowed_hosts: [] # optional exact hostnames, applied to redirects too
max_bytes: 32768
timeout_seconds: 20
request_cost_usd: 0 # operator-supplied reservation per public action
history: false
chain_snapshots: {}
```
To enable public research, set `public: true`. Supply `search_url` for search; page fetching works without it. The endpoint must return text, HTML or JSON and cannot require credentials. This is a generic GET adapter, not a subscription to a search service. If using `allowed_hosts`, include the search endpoint and desired primary-source hosts as well as `rekt.news`. Fetch URLs cannot contain query strings or credentials. PDF extraction and JavaScript-rendered browsing are not implemented.
Public actions count against `scan.max_calls` and reserve `request_cost_usd` against `scan.max_cost_usd`. Bytes and duration are bounded per action; navigation and research share the investigation's action count. Private, loopback, link-local and reserved addresses are refused, including after DNS resolution and redirects. Checked IP addresses are dialed directly to prevent DNS rebinding. The broker sends no provider credentials or cookies. Obvious copied source lines and configured provider keys are rejected in queries; this heuristic cannot identify every confidential natural-language detail. Enable public research only for a scope suitable for public queries.
The bundled index has 1,203 overlapping source entries, not unique confirmed incidents: 877 DeFiHackLabs listings and 326 Rekt leaderboard rows. The separate 37 mechanism mappings distinguish inspected accounts from unverified reproduction leads. Search can start from a mechanism such as keeper liveness or rounding; follow original disclosures and code before promoting a lead. Neither corpus is exhaustive, and an absent match says nothing about safety. See the [research package] and [source notices]. Refresh with `python3 scripts/sync-incident-corpus.py` after reviewing updates to the research documents.
### Pinned chain observations
Configure `chain_snapshots.NAME` with `path` (relative to the audited root, or absolute) and the exact lowercase SHA-256 digest of the file. The file records `chain_id`, `block_number`, `block_hash`, RFC3339 `captured_at`, a `finality` statement, and `calls` containing `method`, `params` and `result`.
Only read-only methods are accepted: `eth_call`, `eth_getBalance`, `eth_getCode`, `eth_getStorageAt`, `eth_getProof`, `eth_getBlockByHash`, and `eth_getLogs`. State calls require the EIP-1898 block selector `{"blockHash":"0x...","requireCanonical":true}` selecting the recorded hash. Block reads and log filters must select that same hash. `latest`, `pending`, number-only selectors, mismatched hashes and oversized partial bundles are rejected. Validation checks the bundle's structure and digest, not RPC honesty, actual finality or consistency with deployed code. Katarina does not issue live RPC requests, sign transactions or broadcast them through this action.
### Evaluation status
The [economic development suite] contains 42 synthetic component cases: vulnerable, repaired and benign variants of fourteen mechanisms. All 150 reference assertions produced their declared outcomes with Foundry 1.8.3 and Solidity 0.8.24. This verifies the reference fixtures, not Katarina's ability to discover their defects. The fixtures isolate accounting and policy; they do not model complete markets, price impact, production capital constraints or whole deployed protocols.
The offline benchmark rejects public research, the incident corpus, repository history and external snapshots to prevent answer leakage. No real-model comparative evaluation, historical reproduction promotion or held-out economic recall result is claimed. Tests written during discovery still require the existing isolated differential grader. For promotion criteria and broader historical coverage, use the research package rather than treating the current development suite as a comprehensive attack catalog.
The latest five synthetic families exercise combined price/depth stress with a delayed keeper and finite insurance, actual token receipts under transfer fees, enforceable automated-swap slippage bounds, deposit claims without a real token transfer, and same-block reward farming without holding-time contribution. These are scoped component models. Compiler-dependent protection is an explicit coverage obligation, but no historical compiler exploit has been reproduced; missing compiler/artifact/deployment evidence must remain unresolved.
Role and mutable-parameter hazards, structured assumption records, proof fidelity, observed economic measurements and primary-source practice comparisons are described in [audit methodology].
## Chaos Labs methodology and an economic simulation harness
Research date: 16 October 2026. The general campaign runner, local/SSH execution and agent adapter-generation interface are now implemented in [simulation execution]. The domain-specific calibration and full market adapters below remain design work; no Chaos Labs runtime is bundled.
### What the public work establishes
Chaos Labs' July 2023 GMX study combines historical state/behavior, adversarial and ordinary participant policies, market paths, and parameter exploration. It describes both a proprietary fast simulation environment and dedicated blockchain forks. The transferable idea is to explore economically plausible behavior and then validate important outcomes against contract execution; its performance claims do not apply to Katarina. [GMX methodology, chapter 3].
The Aave supply-cap study connects collateral-price declines with deteriorating exit liquidity and liquidator profitability. It examines borrower distributions, bad debt and sensitivity to stress severity, and acknowledges limits of its historical scenarios. This motivates measuring whether liquidation can actually happen, rather than assuming that a callable liquidation function guarantees solvency. [Aave supply-cap methodology].
The Avantis study examines stale-oracle arbitrage, trading costs, liquidity-dependent spreads and loss-protection behavior. Its assumptions and caveats are as useful as its parameter recommendations: calibration and participant responses must be recorded and challenged. [Avantis methodology].
There are public implementation references. [Maker-Simulations] separates agents, scenarios, observers and assertions, and says its scripts can be adapted to Hardhat/Foundry. It explicitly excludes Chaos Cloud's execution/data infrastructure and is archived. The archived [Chainlink oracle CLI] and [Uniswap oracle plugin] illustrate controlled local oracle behavior. Review compatibility and licenses before any reuse; this proposal copies no upstream code. The newer [chaos-agents-factory] concerns risk-oracle parameter-update contracts, not an LLM simulation-agent runtime.
### Proposed implementation boundary
Build a reusable campaign runner with a generated, project-specific adapter. Use the project's actual implementation and deployment fixtures. ABI discovery can scaffold calls, but cannot infer meaningful financial properties, correct initialization or market assumptions by itself. Reuse Foundry's stateful handlers and fork support instead of implementing another EVM. [Handler-based invariant testing], [pinned fork creation].
| Layer | Automation we should add | Evidence required before trusting the result |
|---|---|---|
| Project preparation | Identify compiler/build settings, proxies and initializers, existing fixtures, role setup and external dependencies; generate new test/adapter files. | Compile, discover tests, execute healthy deposit/trade/repay/exit paths, and verify deployed code and initial state against the source snapshot. Unresolved mappings block the affected experiment. |
| Actor adapter | Map legal protocol actions for borrowers, depositors, traders, LPs, liquidators, keepers and privileged operators, as applicable. | Source-cited permissions, budgets, allowances, delays, capital constraints and observations available to each actor. Include multiple accounts and coalitions where justified. |
| External environment | Separate executable market price/depth, oracle observations and keeper/off-chain scheduling. | Pinned data provenance, units, timestamps and explicit synthetic assumptions. An oracle-price edit alone does not establish affordable market manipulation. |
| Campaign execution | Replay fixed historical/synthetic paths, sweep parameters and seeds, search for counterexamples, then minimize and replay failing traces. | Independent trial state, bounded run/time/compute budgets, full action schedules and environment hashes. Identical cached requests are not new independent samples. |
| Measurement | Collect receipts, balances, liabilities, backing, exits, liquidation outcomes and losses by participant. | Quantities derived from execution or clearly marked modeled estimates; independent accounting and the existing proof-review requirements. |
The research agents should propose strategies, new action sequences, parameters and falsifiers. Simulation actors should normally run explicit seeded policies: a liquidator acts only if its modeled proceeds cover financing, gas and execution costs; a keeper observes a particular state version and delivers an action later. Using an LLM for every simulated trade would add cost and make behavior harder to reproduce. If LLM-driven actors are evaluated, retain their exact observations/decisions and label the experiment separately.
Start with direct contract execution for correctness. Introduce a faster approximate model only after it is checked against EVM traces over both ordinary and adverse states; reconfirm every security claim on the actual implementation. A fork supplies initial chain state, not future prices, competing traders, private order flow or keeper participation.
### Campaign contract
A proposed campaign artifact should identify source/build/environment digests, adapter and assertion hashes, initialization method, chain ID and pinned block number/hash when applicable, data/model provenance, actor policies, parameter ranges with units, seeds, schedule, resource limits and stop conditions. The run artifact should retain completed/failed/skipped trials, transaction traces, assertion outcomes, successful action counts, revert/discard rates, coverage gaps and measured quantities. The current accepted campaign fields and retained artifacts are documented in [simulation execution]; richer market provenance and automatic minimization remain extensions.
Keep environment setup powers separate from actor powers. Funding an initial account, setting a simulated external shock or advancing time must be recorded as an assumption; it must not secretly give the attacker unlimited capital, arbitrary storage writes or impossible price control. Oracle return values, timestamps, rounds, confidence/deviation behavior and sequencer availability need separate controls. Reorgs, cross-chain delivery and off-chain scheduling need explicit models; ordinary EVM transaction replay does not supply them.
Generated experiments can use the existing validated new-test-file workflow and configured commands. Generic JSON/MCP tools can inspect reports and traces. Mutating live/shared chains is not authorized by a read-only tool declaration; any future campaign-launch adapter must own an isolated disposable environment, explicit compute limits and cleanup. Tool calls and model budgets alone do not bound simulation CPU or storage costs.
Unhinted investigations retain neutral interfaces and their own experiments. Do not inject the guided stress list, incident answers, calibrated attack policies or peers' failing traces into their initial context. Guided agents can share completed results through the ledger. The same general runner should accept scenarios agents invent outside the initial catalog.
### Initial scenarios and acceptance criteria
| Scenario combination | Observation to require | Controls and realism checks |
|---|---|---|
| Price crash + thin liquidity + expensive/absent liquidators | Debt that cannot be repaid from executable collateral sales; time and cost to liquidate. | Healthy market and restored participation; liquidation bonus/close-factor sensitivity; finite liquidator inventory and market impact. |
| Oracle lag/divergence + delayed keeper execution | Unsafe state transition, stale settlement or missed liquidation through the production path. | Fresh observations, honest delays, grace periods and current-state revalidation; distinguish external outage from attacker-induced outage. |
| Off-chain health check + intervening withdrawal/borrow/price update | Approval made at one state version permits an unsafe later action. | Reverse order, refreshed approval, expiry/replay guards and changes to all relevant state, not only account-local fields. |
| LP withdrawals + open-interest skew + funding imbalance | Exit shortfall, pool insolvency or unintended loss transfer. | Ordinary profitable trading is not automatically a defect; account for fees, inventory and the stated risk contract. |
| Liquidation cascade + insurance depletion + socialization/ADL | Who bears losses, whether account splitting changes priority, and whether allocated losses reconcile. | Repaired mechanism, benign split accounts and explicit insolvency/loss-allocation obligations; no assumption that every haircut is unauthorized. |
| Donation/rounding/token behavior + repeated action cycles | Net realizable extraction after token receipts, fees and capital costs. | Healthy users, token-specific transfer behavior, cycle length and exact integer accounting. |
| Role or parameter error during stress | Reachable privileged change creates a disproportionate failure or defeats recovery. | Distinguish typo/sloppiness, compromised privilege and permitted governance choice; check units, bounds, timelocks and rollback paths. |
| Correlated shocks across collateral/venues/services | A failure absent from one-variable tests appears under combined stress. | Joint assumptions, alternative correlation/liquidity models and separate protocol versus environment losses. |
Report attacker net profit, victim/protocol loss, bad debt, available backing, liquidation shortfall, recovery time and loss distribution separately. Use exact on-chain amounts; label valuation prices and model-derived estimates. Adversarial counterexamples establish possibility under assumptions, not incident frequency. Random scenario frequencies estimate real risk only under a justified sampling model; adaptive search and chosen stress paths cannot be reported as calibrated probabilities or value-at-risk. Record uncertainty and test sensitivity on seeds/data not used to choose parameters.
Before calling an adapter useful, it must execute meaningful healthy actions, detect an intentionally introduced economic defect, reject a repaired/benign control and replay the same failing trace. Revert-only or no-op campaigns must be inconclusive. The initial milestones should be one lending adapter and one perpetual/LP adapter, followed by reuse on a different implementation without changing the generic runner. This tests whether we built reusable infrastructure rather than a protocol-specific demonstration.
EVMBench complements these campaigns but does not replace them. See [EVMBench assessment and integration plan].
Simulation campaigns and SSH execution
# Simulation campaigns and SSH execution
Katarina has its own reusable campaign runner. A project adapter maps actions and observations onto actual code; the runner handles seeds, explicit scenarios, fresh workspaces, deadlines, observations, controls and retained replay inputs. The interface is language-independent: market participants, transaction schedules, distributed-service retries and configuration changes can all use it. No Chaos Labs code or execution service is bundled.
The first implementation runs trials serially. It supports local execution and round-robin dispatch across operator-provided SSH machines. It does not provision those machines, install dependencies, calibrate market distributions, infer correct financial properties from an ABI, automatically minimize traces, or impose OS CPU/memory/disk quotas. Those remain separate work. A wall-clock timeout and an output cap are enforced; use a dedicated account/container/cgroup or disposable VM for stronger resource and filesystem/network isolation.
## Run a campaign
These commands run small, explicitly synthetic component fixtures shipped with the repository:
```sh
katarina simulate run --root examples/simulation/economic --manifest examples/simulation/economic/campaign.json --out /tmp/economic-run
katarina simulate run --root examples/simulation/retries --manifest examples/simulation/retries/campaign.json --out /tmp/retry-run
katarina simulate replay --run /tmp/economic-run --trial 3 --out /tmp/economic-replay
```
Use new output directories; the runner refuses to overwrite an existing run. Both examples require Python 3 and have healthy, defective, repaired and benign cases. They demonstrate the runner and controls; they do not reproduce a deployed protocol or establish Katarina's discovery performance. The same JSON interface can invoke Foundry, a service simulator, a history checker or another prepared executable through a project-specific adapter.
A campaign manifest is strict JSON:
```json
{
"version": 1,
"name": "project-property",
"files": ["tests/adapter.py", "src/implementation.py"],
"command": ["python3", "tests/adapter.py"],
"environment_id": "operator-pinned-toolchain-image",
"assumptions": ["Document initialization, external data and actor powers here."],
"seeds": [11, 29],
"cases": [
{"name": "healthy", "kind": "baseline", "parameters": {"delay_ms": "0"}, "expected": "holds"},
{"name": "delayed", "kind": "stress", "parameters": {"delay_ms": "500"}, "expected": "unknown"}
],
"max_trials": 4,
"timeout_seconds": 120,
"trial_timeout_seconds": 30,
"max_output_bytes": 65536,
"backend": "local"
}
```
`files` names explicit regular files relative to `--root`, including adapter, implementation and build fixtures. No directory expansion occurs. Traversal, symlinks, credential filenames and metadata such as `.git`, `.ssh`, `.aws` and `.katarina` are rejected. Ordinary build dotfiles may be included. Each file is hashed and copied without executable permission; invoke scripts through their interpreter. The bundle is capped at 128 MiB and 10,000 files. Toolchains and offline dependency caches must already exist on the execution host.
The adapter receives one JSON document on stdin with `version`, `seed` and `case`. It returns exactly one observation on stdout; extra diagnostics on stdout/stderr make the combined output invalid. Capture subprocess logs inside the trace or assertion evidence. Example:
```json
{
"successful_actions": 3,
"reverted_actions": 1,
"assertions": [{"name": "backing covers liabilities", "holds": false, "evidence": "backing=90; liabilities=100 after transaction 3"}],
"metrics": [{"name": "shortfall", "value": "10", "unit": "asset-base-units", "basis": "observed"}],
"trace": ["initialize recorded state", "execute action 1", "deliver observation", "execute action 3"]
}
```
Metric values are quoted exact decimals. `basis` is `observed` or `estimated`; valuation and external-market assumptions must be explicit. The runner validates structure, not the truth of adapter claims. The adapter must exercise actual implementation, retain enough actions and observations to explain the result, and provide independent assertions. A synthetic oracle change does not establish affordable manipulation; a random stress frequency is not a calibrated incident probability.
A successful process can report a violated property. A nonzero exit, timeout, truncated/malformed output, missing assertions or no successful actions is `inconclusive`, never a successful proof or a clean bill of health. Trial status is `holds`, `violated` or `inconclusive`; `expectation_met` compares that result with the declared control expectation. Campaign `completed` means every planned trial was attempted, not that every property held. Inspect all trials, especially inconclusive outcomes.
`controls_satisfied` requires an expected healthy baseline, an expected defect and an expected repaired/benign control, with complete interpretable observations and all declared expectations met. It is a calibration signal for the adapter, not a security verdict. Merely labeling a case `repaired` does not implement a repair. Use different implementation inputs or an actual repair fixture and inspect the evidence.
## Evidence, limits and replay
The output directory retains `manifest.json`, `snapshot.json`, `run.json` and per-trial `input-N.json`. The snapshot contains source bytes as well as their hashes; keep this directory private. `run.json` records source/manifest/request digests, case/seed, target environment, process outcome, observations and errors. The controller commits `started` before dispatch. On interruption, a saved `started` trial has unknown outcome and is not automatically retried. A fresh replay is an explicitly new run, not another independent sample.
Replay validates the retained manifest and snapshot identity and selects the original case/seed. It uses the retained source bytes rather than the current checkout, and the same selected SSH target when applicable. External toolchain/image IDs are operator declarations, not remote attestation; preserve the installed binaries, caches and external datasets as well. Automatic exact trace minimization and bit-for-bit execution determinism are not claimed.
Seeds and cases are each limited to 128; at most 1,024 trials can run. `max_trials` or a campaign deadline can leave planned trials unexecuted, reported as `incomplete`. Campaign time is limited to 86,400 seconds; each trial to 3,600 seconds. Output is capped at 1 KiB–4 MiB per trial. SSH transfer/response handling has a separate bounded grace period; it does not authorize a longer remote command deadline. Per-campaign serial execution does not limit concurrency across multiple audit jobs; `scan.workers` bounds those jobs. Model cost limits do not include machine costs.
## User-provided SSH machines
Install a matching Katarina binary and the required tools on dedicated execution machines. Configure an existing private key and verified known-hosts file on the controller. Katarina neither uploads keys nor auto-accepts host keys. Password prompts, agent forwarding and port forwarding are disabled; arbitrary user SSH configuration is not loaded.
Ordinary generated proofs and exploratory experiments can use SSH directly:
```yaml
tests:
runner: ssh
timeout_seconds: 180
max_output_bytes: 262144
allowed_paths: ["test/Katarina*.t.sol", "tests/**"]
commands:
solidity: [forge, test, --offline, --match-path, "test/Katarina*.t.sol", -vvv]
ssh:
- name: worker-a
host: audit-worker.example.net
user: katarina
port: 22
identity_file: /absolute/controller/path/id_ed25519
known_hosts_file: /absolute/controller/path/known_hosts
worker_path: /opt/katarina/katarina
environment_id: prepared-image-and-toolchain-digest
```
Up to 16 targets are allowed. Generated proofs route deterministically; simulation campaigns rotate targets by trial index. For a standalone remote campaign, set `backend` to `ssh` and add the same host objects under a top-level `ssh` array in its JSON manifest.
The controller sends only the validated execution bundle, command, input and limits over SSH stdin. `execution-worker` creates a private temporary workspace, strips inherited provider/cloud credentials from the child environment, enforces the command deadline, bounds output and cleans up after normal completion. The reply is bound to the request digest. Transport failures remain unknown outcomes and are not retried. If the connection disappears while the worker remains alive, its own deadline still bounds the child command. Host crashes, worker kills and detached malicious processes require operator-level cleanup/resource isolation; this is not a hostile-code sandbox. It does not terminate user-provided hosts.
## Let agents generate project adapters
Configure a campaign command and name it with `tests.simulation_command`:
```yaml
analysis:
experiment_requests: 3
scenario_investigations: 4
independent_percent: 50
tests:
runner: ssh
simulation_command: campaign
timeout_seconds: 240
max_output_bytes: 262144
allowed_paths: ["tests/**", "test/Katarina*.t.sol"]
commands:
campaign: [/opt/katarina/katarina, simulate, run, --manifest, tests/campaign.json, --root, ., --out, campaign-result]
# Add the ssh host list shown above.
```
The test writer and investigators receive the generic campaign/observation schema. They generate the adapter and manifest as new allowed test files, then use the existing `run_experiment` or proof workflow. Generated manifests should use `backend: local` inside the already selected remote workspace. Host selection and credentials stay in operator configuration. The outer test deadline still bounds the nested campaign. Source preservation, execution-intent recovery, review and investigation-ledger rules remain in force.
Unhinted investigators receive the interface without the guided economic/distributed catalogs or peers' traces. They choose their own cases. The runner accepts arbitrary case parameters rather than a fixed attack taxonomy. Supplied initial scenarios should be limited to guided work. If a project lacks fixtures or the required test hook, agents should record the gap rather than replace the real implementation with a convenient model.
For Solidity, start with a deployment/actor adapter that can execute healthy flows; separately control market depth, oracle observation time and keeper delivery. For regular software, map requests, state changes, faults and schedules into the same contract. Foundry JSON, sanitizer output and history-checker output need adapters that verify actual test discovery and translate genuine assertions; a zero process exit is insufficient. See [economic methodology] and the separate [EVMBench adapter].
Distributed-system reviews
# Distributed-system reviews
Katarina can review distributed architecture and run prepared evidence tools. Enable the distributed profile explicitly; it is independent of the source language. All scenario investigations, including the neutral first group, now work on ordinary software as well as Solidity.
```yaml
analysis:
distributed_systems: true
scenario_coverage: true
scenario_investigations: 6
independent_percent: 30
investigation_context_requests: 8
experiment_requests: 3
tool_requests: 4
```
Merge this fragment into your configuration and start a new session after this policy change. The six-slot example runs two unhinted investigations before four guided investigations. Independent agents receive included source, a bounded repository map and action contracts; they receive no distributed taxonomy, topology template, supplied design notes or other agents' findings. Their own requested research and tools can subsequently inform them. When no specific profile applies, guided slots conduct general invariant and dependency review.
The distributed flag adds guidance to ordinary scouting, architectural extraction, investigation, challenge/defense, assessment and proof review. It requires explicit assumptions about failure, consistency, durability and recovery. An eventual read is not a defect merely because it is stale; a timeout does not imply no committed effect; authentication does not establish freshness or continuing authority. Models still need a source-grounded violation of the declared contract.
## Architecture and coverage
Guided distributed investigations record a `topology` with components, state ownership, authority, failure domains, communication links, scoped guarantees and unknowns. Component and link claims require exact source citations, and links must reference known component IDs. Delivery, ordering, atomicity and authentication assumptions belong in each link's contract. Empty topology plus explicit missing evidence is valid; invented services and unsupported deployment claims are not.
Include service code, interface schemas, migrations, queue/database configuration, deployment manifests and relevant design contracts in the reviewed source root. Katarina still inventories one root. It does not automatically obtain other repositories, join their revisions, or discover a deployed cluster. Missing components or configuration remain report and audit-handoff gaps. Topology is a model interpretation, not a mechanically verified service graph.
With scenario coverage enabled, all twelve distributed families receive assignments:
| Family | Schedules to investigate |
|---|---|
| Ambiguous completion | Commit, lose the response, retry; vary identity, payload and receipt retention. |
| Message delivery | Duplicate/reorder delivery and crash around durable commit and acknowledgement. |
| Leases and fencing | Pause a leader, replace it, then resume its stale writes. |
| Replication | Delay replication around acknowledged writes, reads and failover. |
| Authorization | Consume an earlier permission decision after revocation or tenant changes. |
| Partial transactions | Fail between independent commits, event publication and compensation. |
| Durability and restore | Lose a process after acknowledgement; restore data, dedup state and epochs. |
| Partitions and membership | Split communication asymmetrically and change membership before healing. |
| Time and cancellation | Skew clocks, pause processes and let downstream work outlive deadlines. |
| Overload | Combine dependency delay, retries, queues and exhausted pools. |
| Mixed versions | Exercise both communication directions during upgrades, rollback and migration. |
| Global coordination | Concurrently consume a quota or reservation from separate nodes. |
Solidity-containing repositories retain the 20 economic families, giving 32 combined obligations when the distributed profile is enabled. The same six calls distribute these over four guided slots, at most eight per slot. Configuration validation reserves capacity for this combined scope: six slots and 30% independent work suffice. Larger responses, navigation and experiments can still increase spend. All existing call, token and cost limits apply. Budget exhaustion never implies a family was checked.
## Fault schedules and execution
Start with a deterministic schedule against the actual component implementation: healthy baseline, injected fault/interleaving, invariant observation, recovery, reverse ordering and repaired/benign control. A scheduler can pause transitions, delay message delivery and recreate volatile handlers while preserving explicit durable state. This is useful evidence about the modeled boundaries, not proof that a production database or network implements those boundaries.
Use [agent-selected tools] for prepared fault-testing harnesses and history checkers. The discovery catalog includes [Jepsen], which runs workloads with fault injection and checks operation histories, and [Porcupine], which checks histories against an executable sequential specification. These are discovery leads; neither is bundled or integrated through a dedicated cluster adapter. Agents may research other suitable tools. No live environment is targeted automatically.
Configured launchers can exercise isolated processes or prepared clusters, but Katarina does not manage a multi-node lifecycle, networking faults, storage faults or cluster teardown for you. Agent-mode tools remain local launchers, even with `tests.runner: ssh` or `ec2`; a launcher must provide any extra isolation and cleanup. New harness files use the existing validated generated-test workflow. `tests.runner: none` saves experiment plans without execution.
## Recorded histories
Test and tool output can carry a structured trace on a single line beginning with `KATARINA_HISTORY_V1 `, followed by JSON:
```json
{"name":"write-then-read","model":"linearizable-register","initial":"0","complete":true,"schedule":"acknowledge write; delay replication; perform strong read","operations":[{"id":"w1","client":"writer","kind":"write","value":"1","start":1,"end":2,"outcome":"ok"},{"id":"r1","client":"reader","kind":"read","value":"0","start":3,"end":4,"outcome":"ok"}]}
```
The example violates the declared register model: a completed write precedes a read that returns the earlier value. Values must come from the tested implementation. `start` and `end` are unique, globally ordered logical invocation/response positions from one recorder, not timestamps compared across unsynchronized hosts. An operation must end after it starts. Every operation has a unique ID and a client identity. Writes set the string-valued register and reads return its value. Encode other value types canonically before comparing them.
The controller derives `test_result.history_checks` from recorded output for generated tests, exploratory experiments and agent-selected tools. Raw stdout and `go test -json` output events are supported. It ignores a tool's claimed checker verdict and runs its own bounded search over operation orders that respect response-before-invocation precedence. Raw histories, evidence digests and derived outcomes survive export and resume.
| History status | Meaning |
|---|---|
| `valid` | A legal sequential order exists for this recorded single-register history. |
| `violated` | No legal order exists within the declared complete history and supported model. |
| `inconclusive` | Unsupported model/outcome, incomplete or malformed evidence, truncation, duplicate identity/name, or checker limit reached. |
The built-in checker handles only `linearizable-register`, 1–24 operations per history, at most 16 histories, at most 64 KiB per envelope and 100,000 search states. Ambiguous or unsuccessful operations remain inconclusive; they are not silently discarded or treated as noncommitting. Other consistency models require suitable external specification/checker work. A tool version, seed and complete fault/recovery schedule should accompany a reproducible experiment.
A checked trace is not a universal safety, liveness or durability proof. The recorder can be wrong, a generated harness can fabricate values, and the selected model can misrepresent the promised contract. Independent proof review must still inspect instrumentation, reachability, assertions and controls. Inconclusive emitted histories block a definitive proof interpretation. Missing traces cannot close distributed-family coverage. Only the replication family can currently close its history obligation using the built-in register checker plus independent proof interpretation; other distributed families retain a next-evidence obligation for the property-specific checker or human review, even after component tests run. Process execution, history status and model interpretation remain separate in reports.
## Benchmarks and remaining validation
`benchmark/cases/distributed-suite.yaml` contains 15 synthetic development cases across five families: ambiguous retries, stale leaders, acknowledgement/crash ordering, stale authorization and replica-read consistency. Every family has vulnerable, repaired and benign variants. Seventy-five declared reference outcomes include expected safety failures in vulnerable variants and expected absence-of-defect failures in controls. Source and oracle trees are separately pinned. The original default and economic suites are unchanged.
These are deterministic in-process component schedules, with restart represented by recreating a handler over retained durable state. They do not test real sockets, disks, replicated databases, process termination or cluster recovery. Replica-read cases emit actual observed register histories. The other families use property-specific reference assertions, not an inappropriate register specification.
The suite establishes reference behavior, not live-model detection quality or audit savings. Remaining evaluation includes larger histories against independent checkers, realistic multi-service integrations, fault/recovery coverage beyond these five families, false positives under intentionally weaker guarantees, and measured model cost/precision/recall. Real clusters still require a prepared isolated harness and explicit operational configuration.
For reusable seeded campaigns and user-provided SSH machines, see [simulation execution]. The campaign runner transports and executes adapters; a project-specific adapter still owns multi-node setup, fault injection and teardown.
Generated tests and execution
# Generated tests and execution
The assessor can choose `test` only when `tests.commands` is nonempty. The test writer returns a strict plan: summary, configured command key, new test files and the expected observation. Katarina validates it and writes actual test source under `SESSION/tests/FINDING_ID/attempt-N/`.
```yaml
tests:
runner: none
timeout_seconds: 180
max_output_bytes: 65536
allowed_paths: ["src/test/java/**", "test/Katarina*.t.sol", "**/*_test.go"]
commands:
java: [mvn, -B, -Dtest=KatarinaSecurityTest, test]
solidity: [forge, test, --match-path, "test/Katarina*.t.sol", -vvv]
go: [go, test, ./...]
```
`none` generates reviewable tests without running them. `local` enables local execution. `ec2` uses [disposable AWS infrastructure]. `ssh` uses [operator-provided machines]. With an execution runner enabled, Katarina runs the selected configured command whenever an assessed finding requests a test, without a separate confirmation prompt.
Execution is followed by an independent review of the test and observed output. The reviewer can request a concrete test revision; `max_iterations` limits the total plans/executions per finding (default 2, range 1–5). Every iteration has its own artifact directory, durable execution intent and result. Unchanged test content/command cannot be rerun by merely rewording the plan. `runner: none` generates one plan without execution review. See the [feedback-loop semantics].
## Plan restrictions
- Commands are selected by map key. The model cannot submit executable names, shell strings or arbitrary argv.
- Only new files matching `allowed_paths` are accepted. Existing implementation and test files cannot be overwritten.
- Absolute paths, traversal, hidden path components, duplicate files, credential filenames and NUL-containing paths are rejected.
- At most 12 files and 256 KiB of generated content are accepted.
- The original repository remains untouched; test overlays are written into a fresh copy.
Model prompts ask for assertions against the real implementation that observe the claimed defect and would fail after a repair. These are instructions, not proof that the generated test is sound. Review the actual assertion and run a negative control on the repaired implementation before calling a vulnerability confirmed.
## Shared tests
With `analysis.grouping: true`, related findings can share a plan when every member was individually selected for testing. A shared plan includes `covers` entries mapping every finding ID to an assertion excerpt in a generated file. Proof review records a separate interpretation for every member. Mixed outcomes remain separate, even though execution is shared. Tests are stored under `tests/GROUP_ID/attempt-N/`; individual tests retain `tests/FINDING_ID/attempt-N/`. See [grouping and shared tests].
## Local execution
Katarina copies included regular source files, verifies every SHA-256 digest, and overlays the generated tests. It excludes secrets, symlinks, dependency directories and other excluded inventory entries. No Git hooks or implicit Git checkout is needed.
The command runs in the copy, with a private temporary HOME, no inherited model/AWS keys, a timeout, bounded stdout/stderr and process-group termination. Temporary files are removed afterwards. The report keeps output, exit code, duration, truncation and runner type.
**Local execution is not an OS sandbox.** Code runs with your user privileges, can use the network, and could access other files available to that user. Use this mode for repositories and build tools you trust. Use EC2 for stronger separation. LSP servers and configured analyzer commands have the same local-host consideration.
The snapshot contains only included repository files. Go dependency downloads may require network access; Maven normally sees an empty HOME; Foundry libraries excluded by the scan are absent. Prepare dependencies using one of these approaches:
- Include vendored source dependencies you want analyzed/tested.
- Use a trusted prepared tool wrapper with explicit cache paths, such as `-Dmaven.repo.local=/opt/katarina/m2`.
- Use a prepared EC2 AMI containing the compiler, test tools and offline dependencies.
An example Maven configuration selects one test class. If the writer chooses a different class/file, the command may find no tests or fail: inspect the resulting plan and runner output. Set command naming conventions in your design notes.
## Interpreting results
| Status | Meaning |
|---|---|
| `passed` | The configured command returned exit code 0. Inspect assertions and test discovery. |
| `failed` | The command returned a nonzero exit status; it may be an assertion or setup failure. |
| `timeout` | The command or remote execution exceeded its timeout or was canceled. |
| `error` | Setup, process start, cloud submission or cleanup failed. |
| `indeterminate` | An execution intent exists without a committed result after interruption. |
None of these automatically changes a candidate into an independently confirmed vulnerability. Compilation failures, missing dependencies and “zero tests found” must never be presented as reproduced security issues.
## Rust and C/C++ test commands
These languages use the same validated test overlays and local/SSH/EC2 runners. Rust integration tests can usually be added under `tests/` without changing the crate. Record the crate's features, target and public API in design notes:
```yaml
tests:
runner: none
allowed_paths: ["tests/katarina_security.rs"]
commands:
rust: [cargo, test, --offline, --test, katarina_security]
```
Select `local`, `ssh` or `ec2` when ready to execute. The named test file must match the command. Dependencies and the selected toolchain must already be available for offline execution. Cargo projects with `autotests = false`, private-only APIs or explicit target lists may require an existing test hook; Katarina will not rewrite their manifest or production code. For a rustup installation, point PATH at the real toolchain binaries or use a trusted wrapper, as described in [navigation].
For C/C++, configure a project-owned command that compiles the newly overlaid test, links the actual implementation, runs it, and propagates failure. A trusted launcher can configure/build a disposable CMake directory and run a selected CTest target. `ctest` alone does not compile new source or register a new target. Existing CMake/Make build files cannot be overwritten by a generated plan, so prepare test discovery ahead of time. The default `tests/**` path allows C/C++ test sources; narrow it for your project. Sanitizer and fuzz commands use the same operator-configured command map and prepared toolchain.
For economic Solidity claims, see [economic scenario tests]. Reproduction tests should stop observing the defect on a repaired mechanism; permanent safety regression assertions should pass on the repair.
A persisted execution intent prevents an interrupted test from automatically running a second time. Start a fresh session or manually rerun the generated test after inspecting an indeterminate result. For EC2, first run the cleanup command printed in the AWS guide.
Proof-review interpretations are `supports`, `refutes`, `inconclusive` or `revise`. They do not overwrite the original disposition or convert command success into a confirmed vulnerability. Error/timeout/indeterminate execution cannot authorize revision, and incomplete/truncated output cannot support a definitive interpretation. When the revision limit or a budget is exhausted, remaining uncertainty stays visible.
## Agent-selected analyzers and other tools
Set `analysis.tool_requests` above zero to let scouts, investigators and review roles discover and select tools during their normal work, for any repository language. The default is zero, including in new init files. This is independent of Solidity scenario discovery and `tests.runner`. Existing `tools` entries without a `mode` still run as preflight commands; `mode: agent` makes a command available only on agent request.
```yaml
analysis:
tool_requests: 4
scan:
context_requests: 6
tools:
- name: slither-project
mode: agent
description: Analyze the configured Solidity project; compilation must succeed.
extensions: [.sol]
command: [slither, ., --json, "-"]
version_command: [slither, --version]
timeout_seconds: 300
max_output_bytes: 131072
- name: semgrep-local
mode: agent
description: Scan with the operator's pinned local rule bundle.
command: [semgrep, scan, --config, /opt/katarina/rules/security.yaml, --json, --metrics, "off", --disable-version-check, .]
version_command: [semgrep, --version]
timeout_seconds: 180
- name: project-properties
mode: agent
description: Run existing property tests with fixed seed and campaign limits; emit scope and reproduction details.
command: [/opt/katarina/bin/project-properties]
version_command: [/opt/katarina/bin/project-properties, --version]
timeout_seconds: 300
```
Install and prepare the selected tools, compilers, dependencies and rule bundles before starting. The paths above are examples, not shipped binaries or rules. Slither's stdout JSON option is documented in its [usage guide]. Semgrep supports local rule files and explicit metrics/version-check settings; inspect its [CLI reference] for your installed version. A wrapper can drive any language's analyzer, compiler checks, dependency checks, existing tests, sanitizers, fuzzers or symbolic execution. For newly generated harness files, keep using `tests.commands` and the validated test workflow.
The agent workflow is:
1. State an evidence question and its strongest falsifier. Request `discover_tools` with `query: auto`, `all`, or tool/language keywords. Discovery reports configured commands, executable existence and extension matches without executing a process. It returns a small, non-exhaustive catalog with primary documentation links. Extension matches are suggestions, not execution restrictions or build-compatibility guarantees.
2. Seek more suitable tools using `search_public` and `fetch_public` when [public research is configured]. Agents can search beyond the catalog. Compare actual language/framework support, build prerequisites, rule coverage, versions, licensing and network behavior; there is no universal best tool.
3. Request `run_tool` with `tool: semgrep-local` or another exact configured agent-mode name. No agent-provided arguments, working directories, installation commands or source edits are executed. Define separate named configurations for different targets, rules, build modes or seeds. A command must print its report to stdout/stderr, or a trusted wrapper must emit it; temporary output files are not exported.
4. Inspect raw diagnostics, source locations, coverage and setup errors. Candidates still require source validation and the ordinary challenge/defense/assessment workflow. If a suitable tool is missing, `propose_tool` records its documentation URL, rationale, suggested argv, setup and limitations in the report and audit handoff. Proposals do not install tools or authorize execution. Configure the reviewed proposal and start a new session to use it.
Unhinted agents receive only the generic action contract at the start, without catalog suggestions, configured tool descriptions or other agents' results. They see suggestions and results after choosing to request them. Their own requested research can naturally inform subsequent investigation.
`tool_requests` accepts 0–64 and counts discovery, execution and proposal requests; non-scenario agents' public research also uses this cap. Requests share existing context rounds, and their model calls/public requests retain global budget accounting. There are at most 64 configured tools. Each fixed-command agent tool executes at most once per session, with a recorded version probe. Interactive tools instead cache per investigation/operation/arguments; see [interactive tools]. Concurrent requests and resume reuse the saved result; an interrupted command without a result remains `indeterminate`. Repeating a fixed-command tool name never launches a new fuzz campaign. Output defaults to 65536 bytes (configurable 1024–1048576); execution timeout is 1–3600 seconds, plus at most 30 seconds for a version probe. Local CPU and tool licensing costs are not charged to the model USD budget.
Execution uses a fresh, hash-checked copy of included source and the cleaned local environment described above. **Agent-mode tools run locally regardless of whether `tests.runner` is `none`, `local`, `ssh` or `ec2`.** Their configuration is explicit authorization for local execution when tool requests are enabled. Use a trusted launcher into your own isolated environment when needed; this feature does not provide an additional container/remote runner or block network access. Repository build scripts and tool configuration may execute code. The model cannot expand the configured command, but the command itself retains local-user privileges.
Reports retain source/configuration digests, exact configured argv, optional version-probe output, exit status, duration, raw bounded output and truncation. A configuration digest does not pin the installed binary, external rules, database or wrapper contents: pin these in your prepared environment and print their identities in the version probe. For repeatable fuzzing, also fix and record seeds, budgets and input corpus. There is no generic automatic parsing of every analyzer's JSON/SARIF; agents inspect recorded output, and missing coverage stays unresolved. A `passed` process may still contain findings, while `failed` can mean either findings or setup failure.
The discovery catalog currently links Slither and Echidna for contracts; govulncheck for Go; Clippy for Rust; Clang Static Analyzer for native code; SpotBugs for Java; Bandit for Python; and Semgrep, CodeQL and OSV-Scanner for their supported languages/ecosystems. See the primary sources returned by discovery, including [Go vulnerability tooling], [Clang Static Analyzer], [CodeQL language coverage] and [Echidna]. Unknown languages can use custom configured tools and researched proposals. Catalog entries are discovery leads, not installed integrations or a completeness claim.
## Proof fidelity and quality gates
With `analysis.proof_quality: true`, both scenario experiments and final finding proofs require a declared production/dependency environment and independent review of discovery, triggering inputs, assertions and controls. Definitive interpretations require all five quality checks, with quotations from complete recorded output. These checks establish evidence provenance, not semantic correctness; generated output can lie. Potential severity remains separate from proof strength. See [proof contracts and economic measurements]. The existing [benchmark differential workflow] executes the same test overlay against vulnerable/repaired snapshots independently of discovery; inspect legitimate behavior as well before accepting a repair.
## Reusable simulation campaigns
Set `tests.simulation_command` to a configured campaign command to let investigators and test writers generate project adapters and seeded manifests. The same runner supports economics and regular software, with structured observations, controls and retained replay inputs. See [simulation campaigns and SSH execution].
Disposable EC2 test runner
# Disposable EC2 test runner
Katarina uses the AWS SDK directly, so the controller machine does not need the AWS CLI. Credentials come from the standard SDK chain: environment variables, shared AWS credentials/config files, SSO profiles or an assumed role. AWS credentials remain with the controller and are excluded from model worker requests.
## Create the stack
1. [Launch the Katarina stack in Asia Pacific (Seoul)].
2. Review the preloaded `katarina` stack and its [template YAML]. The launch link uses the [public S3 template] and selects `ap-northeast-2`.
3. Supply `OperatorPrincipalArn`: the existing IAM user or role allowed to assume Katarina's operator role. Review and acknowledge IAM creation in AWS.
The website and this manual open CloudFormation's review page directly with the template selected. The same YAML is embedded in Katarina for offline export or manual template upload:
```sh
katarina aws template --out katarina-bootstrap.yaml
```
### Prefilled quick-create links
CloudFormation's `templateURL` uses the S3 HTTPS endpoint; the website URL remains a convenient download. To print the same launch link, or choose a different target region, run:
```sh
katarina aws link --template-url https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml --region ap-northeast-2
```
The command prints a console URL opening the quick-create review page with the stack template preloaded. Sign in to AWS, select the operator principal and acknowledge IAM creation to create the stack. Credentials are configured separately using a profile or environment variables as described below; the link and stack outputs contain no secret keys. See the [official quick-create documentation].
The stack creates a dedicated VPC/public subnet, a security group with no inbound access, an encrypted private S3 artifact bucket, a restricted EC2 instance role/profile, and an operator role. The runner manages instances through SSM, without SSH access.
## Configure credentials and outputs
Use the `OperatorRoleArn` stack output with an AWS profile:
```ini
# ~/.aws/config
[profile katarina]
role_arn = arn:aws:iam::123456789012:role/YOUR-STACK-OperatorRole-...
source_profile = default
region = ap-northeast-2
```
Your existing `default` identity must be allowed to assume that role. Alternatively use your organization’s SSO/role process, or supply `AWS_ACCESS_KEY_ID`, `AWS_SECRET_ACCESS_KEY` and, for temporary credentials, `AWS_SESSION_TOKEN`. The stack's `CredentialsConsole` output links to the relevant IAM role page.
Copy these outputs into `katarina.yaml`:
```yaml
tests:
runner: ec2
timeout_seconds: 180
commands:
java: [mvn, -o, -B, -Dmaven.repo.local=/opt/katarina/m2, -Dtest=KatarinaSecurityTest, test]
allowed_paths: ["src/test/java/**"]
aws:
region: ap-northeast-2
profile: katarina
subnet_id: subnet-...
security_group_id: sg-...
instance_profile: YOUR-STACK-InstanceProfile-...
image_id: ami-YOUR-PREPARED-IMAGE
instance_type: t3.small
bucket: YOUR-STACK-artifacts-...
ttl_minutes: 30
```
Instance types permitted by the template are `t3.small`, `t3.medium` and `t3.large`. Update the template and configuration together for other types. TTL is 5–120 minutes. Allow enough TTL for boot, SSM registration, test timeout and cleanup. The code stops waiting one minute before the launch deadline.
## Prepare the test AMI
Use an x86_64 Amazon Linux 2023-compatible image with:
- An enabled Amazon SSM Agent and AWS CLI (`aws`).
- `bash`, `tar`, `gzip`, `timeout`, `unshare`, `runuser` and `useradd`.
- Your JDK/Maven/Gradle or Solidity/Foundry toolchain, available on `/usr/local/bin:/usr/bin:/bin`.
- Offline dependency caches readable by the unprivileged test user.
- A root volume at `/dev/xvda` compatible with the configured 20 GiB encrypted gp3 mapping.
Build a toolchain image containing the required tools and dependencies, then pin its ID in `aws.image_id`. Each test uses that configured image. If the AMI uses a different device layout or requires larger volumes, adjust the runner before use. Project dependencies must be available offline because the test's network namespace cannot reach external services.
## Lifecycle and boundaries
1. Persist a resource intent and idempotent EC2 client token in SQLite.
2. Copy/hash-check included source, overlay the generated tests, archive regular files, and upload to an encrypted private `sessions/` S3 object. The uncompressed snapshot cap is 128 MiB.
3. Launch one instance with IMDSv2 required, encrypted disposable storage, no inbound access, and Katarina ownership/expiry tags.
4. At boot, schedule shutdown after the configured TTL. `InstanceInitiatedShutdownBehavior=terminate` makes that shutdown terminate the host.
5. Wait for SSM Online, then submit the test command once. An ambiguous SSM submission is not retried automatically.
6. The root SSM setup downloads the archive, then the test runs as an unprivileged user in a separate network namespace. It cannot reach IMDS, SSM or external services through that namespace. This is host separation, not a formal proof against kernel escape.
7. Capture the command result. Request instance termination and delete the source object on success, failure or cancellation. Persist cleanup completion.
SSM inline output has AWS-imposed limits (24,000 stdout / 8,000 stderr characters); Katarina also enforces its own byte limit. Do not rely on the inline output for huge test logs. See [GetCommandInvocation].
## Recover and clean up
```sh
katarina aws cleanup --config katarina.yaml --state ./project/.katarina SESSION
```
The command uses durable client tokens to find instances after a lost launch response. Resume also attempts cleanup before additional EC2 work. Cleanup failures remain visible in `outstanding_resources`; they are not silently treated as successful testing.
If the controller crashes or cannot reach AWS, the in-instance shutdown timer remains. A failed boot, disabled shutdown service or unavailable control plane can defeat that timer; termination is not an absolute guarantee. For an explicit sweep of expired tagged instances in the configured region:
```sh
katarina aws reap --config katarina.yaml
```
The `reap` command requests termination only for instances tagged `ManagedBy=Katarina` with a parseable expired `ExpiresAt` tag. Schedule it through existing operations tooling if periodic cleanup is needed. Model budgets do not cap EC2, EBS, S3 or public IPv4 costs; AWS billing is separate.
The S3 bucket expires session objects after one day and is retained on stack deletion to avoid accidental loss. Empty/delete it explicitly when no longer needed. Stack deletion does not automatically terminate instances launched independently of CloudFormation; run cleanup/reap first.
Validation coverage includes local template checks and mocked runner lifecycle tests. Deployment and live EC2 test execution have not been validated; verify them in a dedicated evaluation account and target region before using the runner for reviews.
Evidence reports and recovery
# Evidence reports and recovery
Each session has a stable ID and lives under the selected state directory:
```text
.katarina/
controller.lock
state.db
state.db-wal # may exist while the database is open
state.db-shm
sessions/SESSION/
config.json # effective configuration, without API keys
inventory.json # included/excluded files, hashes and chunks
report.json # complete report contract
audit-handoff.md # prioritized developer work list and gaps
report.md # full findings and review arguments
report.sarif # SARIF 2.1.0
events.jsonl # ordered export of committed events
composition.json # bounded capability graph, lineage and deferred coverage
security-knowledge.json # combined source-cited claims, when available
investigation-plan.json # configured/generated questions, when planned
investigations.json # question answers and incomplete records
finding-groups.json # nonempty shared-validation groups
tests/FINDING_ID/attempt-N/... # generated test sources per iteration
tests/GROUP_ID/attempt-N/... # shared tests, with per-member coverage
```
SQLite is authoritative. File exports are snapshots, written atomically at normal completion or a handled interruption. A hard process kill may leave exports stale. Regenerate them from committed state:
```sh
katarina report --state /path/to/.katarina SESSION
```
Do not copy a live SQLite database without its WAL or a SQLite-aware backup. Stop the session first if copying the directory conventionally. The store uses schema version 1 and fails on unsupported versions rather than guessing a migration.
## Contracts
| Artifact | Contract |
|---|---|
| Full report | `schemas/report.schema.json` |
| Assessed finding | `schemas/finding.schema.json` |
| Event record | `schemas/event.schema.json` |
| Generated test plan | `schemas/test-plan.schema.json` |
| File/chunk inventory | `schemas/inventory.schema.json` |
| Shared security knowledge | `schemas/security-knowledge.schema.json` |
| Investigation plan | `schemas/investigation-plan.schema.json` |
| Investigation records | `schemas/investigations.schema.json` |
| Finding groups | `schemas/finding-groups.schema.json` |
| Capability composition | `schemas/composition.schema.json` |
| Investigation ledger | `schemas/investigation-ledger.schema.json` |
| Worker request/response | `proto/worker.proto` |
| Native pi bridge | `internal/piffi/bridge.h` |
JSON Schemas use Draft 2020-12. Exports use `schema_version: 1.12.0`; the schemas also accept 1.0.0 through 1.11.0 reports. New analysis fields are optional for earlier reports. SQLite uses storage version 1; family-budget and analysis-artifact tables are added when the database is opened if absent. Go validates model output before accepting it, including citation provenance and relationships between group members that cannot be fully expressed by JSON Schema. The report includes:
- Source and configuration digests and session completion status.
- Included/excluded file counts and completed/expected scouting jobs.
- Separate deep-scout coverage, so sampled stronger review is distinguishable from baseline coverage.
- Separate knowledge and question coverage, shared source-cited claims, the committed investigation plan, and completed or incomplete question records. Combined artifacts may be absent when their stage has not finished; completed model jobs still retain their accepted outputs.
- Candidate locations, CWE strings, severity, claim, evidence, prerequisites, impact and remediation.
- Optional structured `finding.economics`: actors, assumptions, strategy sequence, capital, net payoff, constraints, violated invariant and validation plan. All fields are required when this object is present; economic findings need not have a CWE mapping.
- The challenge, independent defense, rebuttal and assessor decision.
- Optional review `checks` and decision `assessment`, with evidence verdict, cited obligations, next evidence, capability analysis and deployment applicability. Quotation matching verifies source provenance, not the correctness of the model's reasoning.
- Optional finding `group_id` and `shared_test_id`, group membership and required assertions. Shared test plans have `covers`; shared proof verifications have per-finding `members`. All individual findings and decisions remain available.
- “By design” evidence, ignored dispositions and uncalibrated model confidence.
- Generated test plans, execution results and output.
- All `test_attempts` with plan, result and optional model verification. Top-level `test_plan`/`test_result` retain the latest attempt for compatibility.
- Job attempts, result text, token usage and estimated-usage flags.
- Ordered events, conservative spend reservations and outstanding cloud resources.
- `model_families` with each configured cap, cumulative reserved tokens, observed input/output usage and an estimated-usage flag. A cap of zero means unlimited. Sessions created before family accounting was introduced have no family ledger; their usage is not reconstructed retroactively.
A failed or canceled scan is `incomplete`, even if some stages have finished. An empty findings array is not meaningful without the coverage and job status fields. Tool exits are captured rather than converted to clean scans. A successful model scan means scheduled stages completed, not that the software is secure.
## Audit handoff
Give auditors `report.md`, `report.json`, `inventory.json`, the exact source revision and generated tests. Ask them to review unresolved candidates, highest-impact findings, assumptions accepted as intended design, and coverage gaps. Keep ignored findings available so the rationale can be challenged.
SARIF keeps the same finding IDs and file locations for code-scanning consumers. Model-recommended ignores are emitted as external suppressions **under review**, not auditor-approved dismissals. Results carry the assessor disposition, rationale, optional economic/evidence assessment and group/shared-test references in properties. Shared execution and individual member interpretations remain in test attempts. A SARIF upload is an operator action; Katarina does not upload reports automatically.
## Sensitive data
Reports can contain proprietary source excerpts, vulnerability details, test output and design documents. The state directory/files are created with private permissions. Existing state directories must have mode 0700, and state.db must be a regular file. Known provider keys are redacted from model/tool text and not included in effective configuration, but this is not a universal secret detector. Exclude confidential files you do not want sent to your configured model provider. A filename blacklist cannot detect credentials embedded in arbitrary code.
## Session compatibility
The configuration digest includes model choices, commands, budgets and the binary's review-policy version. API-key values are excluded, so credentials can be rotated without invalidating a session. Resume requires the same inventory and effective configuration to keep evidence from different review conditions separate.
If an upgrade changes the review policy, start a new session to use it. To continue existing work, use the original binary and configuration. Reports from existing sessions can still be exported without rerunning the review.
Policy `5-source-coverage-and-proof-history` reserves primary chunk context before supplementary material and rejects test revisions that repeat any earlier attempt. New sessions are required to apply these fixes; completed jobs from earlier policies are not retroactively counted as having received the corrected context.
## Limits of recovery
An in-flight model completion can be billed twice if its response was lost. Reservations are retained. Completed jobs are reused. Navigation rounds have separate job IDs and their accepted outputs are reused. A model that repeatedly exhausts its context budget requires a fresh session with adjusted limits.
Test execution has a durable intent before launch. A missing result is `indeterminate` and never silently repeated. EC2 resource intents and client tokens support cleanup after interrupted API calls; verify outstanding resources in AWS when cleanup reports an error. See [AWS recovery].
Economic discovery adds `explorations`, `observations`, and expected/completed exploration counts. Each exploration retains its independent/guided origin, source seed and final scenarios (or an explicit incomplete state). Observation IDs link actions, hypotheses, falsifiers, retrieval metadata, evidence and test interpretations to their investigation. `finding.external_risks` survives JSON, Markdown and SARIF. Capability `exposure` permits supported external harm without an attacking principal.
Scenario ledgers are predicted values; command results and model interpretations remain separate. A public page digest covers the fetched bounded byte prefix before HTML conversion/redaction, not the full remote document when truncated. Chain snapshot digests cover the entire accepted file. Public sources can change after retrieval.
Schema 1.5 adds `scenario_coverage`, guided exploration `families`, and result `coverage` assessments. Review labels are model assessments; execution labels are derived from linked controller results. Absent or unfinished assignments remain visible, including when budget caps stop a session. `audit-handoff.md` is generated from the same artifacts without another model call and retains unresolved work even when a command ran. It is not an audit-cost estimate or proof of complete coverage.
Schema 1.6 adds `discover_tools`, `run_tool` and `propose_tool` actions and optional `observation.tool_result`. Tool results retain command/configuration/source provenance, version-probe output when configured, and bounded process results. They are separate from generated-test results and do not satisfy scenario execution obligations by themselves. Proposals retain suggested argv and setup without authorizing execution. Markdown, JSON, SARIF observation properties and the audit handoff retain this evidence; process success does not establish a clean security scan.
Schema 1.7 adds optional exploration `topology`, `test_result.history_checks`, and family `history_status`. Histories are controller-derived from recorded output and retained separately from process success and independent interpretation. Unsupported, malformed and incomplete traces remain inconclusive. Source-cited topology is a model interpretation; architecture unknowns remain in the audit handoff. See [distributed review semantics].
Schema 1.8 adds finding `operational_risks`, exploration `assumptions`, test-plan `environment`, verification `quality` (including observed/estimated measurements), finding `practice_review`, related investigation `parent_finding_id`, and report `pipeline`, `followup_deferred`, `practice_deferred` and `practice_pending`. Candidate stages come from saved jobs; they cannot identify a never-discovered bug or certify a dismissal without independent ground truth. Practice evidence names recorded page observations with URL, retrieval time and content digest; it does not override severity. Markdown, audit handoff and SARIF retain the corresponding evidence. See [audit methodology].
Schema 1.9 adds `investigation_ledger` and `investigation-ledger.json`, retaining source/job identity, immutable claim/update history, lease times, attempts, blockers, peer-reported outcomes, cited observations, revisit reasons and committed discovery results. Markdown, audit handoff and SARIF preserve this history. Ledger outcomes are not finding dispositions: `failed`/`blocked` never mechanically becomes `refuted`. SQLite storage version remains 1; additive ledger tables are created when opened. Per-dispatch snapshots and explicit responses are saved atomically in SQLite for consistent replay, rather than recomputed from later peer work. See [collaboration and isolation].
Schema 1.10 adds report `composition`, finding `composition` provenance, investigation origin `composition`, and proof-environment `scope`/`boundary_cases`. Intermediate composition checkpoints are exported even when a run stops. Scope describes the proposed experiment; it does not attest platform execution. See [capability composition].
Tool observations may include `preflight`, `input_digests` and `environment_digest`. Preflight failures block analysis and remain evidence gaps. Dependency graph/advisory CLI output has its own `1.0.0` schema and is retained as tool output when configured; component matches are not automatically promoted to findings. See [dependency audits].
Interactive tool observations add `interaction` (transport, operation, arguments, capability-catalog digest). They retain the ordinary source/configuration/environment and input hashes. See [interactive tools].
## Simulation and external benchmark artifacts
Standalone simulation campaigns retain their own `manifest.json`, `snapshot.json`, `run.json` and per-trial inputs in the chosen output directory, separate from the audit SQLite store. Nested campaigns requested as tests retain the generated files and captured command output through the normal proof/observation records; temporary workspace files are not automatically exported. See [simulation evidence].
The EVMBench Detect adapter writes an incremental `submission/audit.md` containing only retained assessed findings, plus a private run directory with its task contract, provenance and full reports. That submission intentionally excludes ignored/pending candidates and debate text; normal audit reports continue to preserve them. See the [integration guide]. Neither format is an official benchmark score.
Development, packaging and evaluation
# Development, packaging and evaluation ## Build Development requirements: - Go 1.24 or later. - Rust `nightly-2026-07-05` (pinned by `ffi/pi-bridge/rust-toolchain.toml`). - A C compiler/linker and platform build tools for cgo and pi's native dependencies. - Network access on the first build to fetch Go and Rust modules. ```sh rustup toolchain install nightly-2026-07-05 --profile minimal make build bin/katarina version ``` `make build` builds the static Rust bridge using Cargo.lock, then links it into `bin/katarina` with the Go `pi` build tag. The first build downloads and compiles pi's dependency graph and can require several minutes and substantial memory and disk space. Subsequent builds reuse the Go and Cargo caches. The linked pi feature set is documented in [architecture]. Linux and macOS are the intended host platforms; build on the target OS/architecture with the corresponding C/Rust toolchains. A single executable does not mean universal libc compatibility: Linux binaries inherit the baseline of the build host. Build releases on the oldest supported target distribution and test them there. Windows users should use WSL; Windows controller locking is explicitly unsupported in this implementation. The application runs from a single executable containing the pi runtime and embedded SQLite. Project tests and optional analyzers/language servers require their own tools. `make build-go` produces `bin/katarina-go`, a Go development build with the `direct` provider engine and synthetic `demo` engine. That build rejects `engine: pi` because it does not include the Rust bridge. ## Tests ```sh go test ./... go test -race ./... go vet ./... python3 -m unittest discover -s scripts/tools -p 'test_*.py' # After make ffi: go test -tags pi ./internal/piffi ./internal/provider ``` Tests cover provider request shapes and refusal/truncation handling; typed IPC framing; source chunk coverage and symlink/drift rejection; credential precedence/redaction; concurrent budget reservations and restart recovery; the full scout/debate/judge/test pipeline; language-server protocol exchanges; generated test-path restrictions; local command timeout/output bounds; and mocked EC2 lifecycle/cleanup. FFI tests call the actual linked pi Agent with a deterministic Go provider callback. They exercise success, token accounting and provider failure without paid model calls. AWS lifecycle tests use a mock backend, not real EC2 instances. Live provider and AWS tests require explicitly configured credentials and should be run in a dedicated evaluation account/project. Economic/native-language tests verify that review guidance reaches every triage stage, economic evidence survives SQLite and report export, and mixed Rust/C/C++ LSP requests carry the correct language IDs. Optional local compiler tests reproduce an authorization defect in C, C++ and Rust, then check a repaired negative control using the actual implementation. They skip only when the relevant compiler is unavailable and need no third-party packages. LSP protocol tests use a stub server; they do not establish successful indexing of a real project by rust-analyzer or clangd. Investigation tests verify concurrent agents under the worker limit, recovery of a cheap-scout miss by independent deeper scouting, execution-feedback-driven revision, and resumption without repeating executed attempts. Budget tests race multiple claims against one family cap, check rollback of rejected claims, retain reservations across reopening, and aggregate usage across retries/roles. CLI tests cover `--max-agents`, repeated family budget overrides and the generated resume command. See [comparative evaluation] for the separate security-quality tests still required. Shared-analysis tests cover questions recovering baseline misses, selected shared context versus independent deeper scouting, role inheritance and family accounting, exact citation checks, economic obligations, grouping membership, assertion mappings and mixed member interpretations. An integration test closes/reopens SQLite after an interrupted shared proof review and checks that the execution and completed model calls are reused. Artifact tests reject changed immutable data; replayed assessments preserve committed proof evidence. These use synthetic model/runner fixtures and establish orchestration behavior, not detection quality. To export the richer integration fixture for independent JSON Schema validation, set `KATARINA_SCHEMA_REPORT` to a temporary output directory while running `go test ./internal/engine -run TestSecurityAnalysisSharedProofAndRecovery -count=1`. Validate the resulting report and additional analysis artifacts against their matching Draft 2020-12 schemas. Interactive-tool tests use real fixture child processes to check MCP initialization, paginated catalogs, schema enforcement, operation results, deadlines, bounded diagnostics and separate task sessions. Adapter tests navigate a SARIF fixture and exercise the Ghidra wrapper with a fake headless executable; they do not compile the Java script or validate a Ghidra installation. Agent-tool tests drive discovery and execution through ordinary software and Solidity scouting, preserve diagnostics through triage/export, check concurrent reuse and interrupted execution, and exercise the request cap and unhinted start. A separate test runs the real Go compiler on a copied source snapshot and rejects source drift. The fake diagnostic fixtures establish orchestration, not Slither/Semgrep accuracy. Set `KATARINA_TOOLS_REPORT` when running `go test ./internal/engine -run TestAgentToolLoopForSoftwareAndSolidity -count=1` to export a tool-bearing report for schema validation. These tests do not install optional analyzers or contact live public search services. Regenerate protobuf types when changing the worker contract: ```sh go install google.golang.org/protobuf/cmd/protoc-gen-go@v1.36.6 protoc --go_out=. --go_opt=module=katarina.fyi/katarina proto/worker.proto ``` Generated protobuf Go code is checked in, so normal builds do not require protoc. JSON Schema regeneration uses the development helper `python3 scripts/generate-schemas.py`; it is not a runtime dependency. ## Package ```sh make release RELEASE_VERSION=0.1.0-preview.1 ``` This builds the native pi executable and generates `web/downloads/katarina-VERSION-OS-ARCH.tar.gz`, `web/downloads/katarina-VERSION-source.tar.gz` and `web/downloads/SHA256SUMS`. `web/downloads/` is Git-ignored. The packager runs `katarina version` and requires the requested version and linked pi support; it does not substitute a direct-only build for a native release. The source archive includes tracked and non-ignored new source files from the working tree, without Git history, build output, private session directories or download archives. Each archive includes `BUILD.json`, a source-file checksum manifest, dependency metadata, pi's license/rider and collected dependency notices. Notice collection uses installed Go/Cargo metadata and local license files; where a crate omits its license file, it fetches the upstream notice at the crate's recorded Git revision. For declarations offering Apache-2.0 without a packaged notice, it includes the canonical Apache license text and records the declaration/repository. This can require network access. The Rust dependency listing is a conservative resolved-graph inventory, including build/platform dependencies, not a claim that every package survives linking. `BUILD.json` records the version, native target, build tools/settings, source identity, base Git revision and whether local changes were included. A dirty working tree is packaged explicitly as a source snapshot, not falsely identified as a clean Git release. Archive members have deterministic ordering, modes and timestamps. The generated unsigned SHA-256 manifest checks download integrity; it is not a publisher signature. Pin and validate target environments before claiming wider platform support. On Linux, the manifest also records the build host's libc and linked system libraries. To repackage an already built, matching native executable: ```sh go run ./cmd/bundle --version 0.1.0-preview.1 --binary bin/katarina ``` Run native macOS releases on macOS with the corresponding C/Rust tools, then smoke-test them there. Cross-building a Go-only executable would omit pi and is not the release format. Developer ID signing/notarization requires the maintainer's Apple signing setup; no signed or notarized macOS package is claimed by the current Linux preview. Keep downloadable versions and platform availability in `web/index.html`, `docs/installation.md` and README consistent when preparing another release. ## Website The public website files are `web/index.html`, `web/style.css`, generated `web/manual.html`, `web/katarina-bootstrap.yaml` and the generated `web/downloads/` directory. It uses static HTML and CSS with system fonts; the red high heel is Unicode Braille text in a `<pre>` element. Preserve its characters, spacing and line breaks when editing the artwork. Preview the embedded site with: ```sh bin/katarina serve --listen 127.0.0.1:8787 ``` `make docs` renders the manual as escaped text with clickable documentation, download and external links, and copies the embedded deployment template to `web/katarina-bootstrap.yaml`. Rebuild Katarina to update the embedded pages and template. The preview server defaults to loopback. Download archives are deliberately not embedded recursively inside the executable; download links target the public website, and a plain static server can preview the entire upload directory including downloads. Upload the public files and the complete `downloads/` directory to the root of `https://katarina.fyi/`, preserving names and subdirectories. `web/embed.go` is a Go build file and is not needed by the static host. Set ordinary content types for HTML/CSS, YAML and gzip archives; the artifacts need to be downloadable without authentication. The generated file permissions are readable by a static uploader. Upload matching archives and `SHA256SUMS` together; check published checksums before announcing a release. No credentials or application state belong in `web/`. ### Connect the hosted AWS template The public download is `https://katarina.fyi/katarina-bootstrap.yaml`. The launch buttons open CloudFormation's review page for stack `katarina` in `ap-northeast-2`, using `https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml` as the template. To reproduce the link: ```sh katarina aws link --template-url https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml --region ap-northeast-2 ``` Publish the generated `web/katarina-bootstrap.yaml` both with the website and as object `katarina-bootstrap.yaml` in the `katarina-bootstrap` S3 bucket. Keep those copies identical to `deploy/katarina-stack.yaml`; uploading the website does not necessarily update the separate bootstrap bucket. The S3 object must be publicly readable through its HTTPS endpoint before the launch link can create a stack. If the endpoint or launch region changes, update the AWS buttons in `web/index.html` and the manual generator, and the launch link/examples in `docs/aws.md`. Run `make docs`, rebuild and repackage so the source and embedded manual agree. Creating a CloudFormation stack still requires the operator principal, IAM acknowledgment, credentials and a prepared test AMI. ## Evaluate security quality Do not infer security quality from infrastructure tests. Build a versioned benchmark of repositories and known issues you are allowed to analyze: 1. Include vulnerable and repaired versions, with ground-truth issue locations and exploit prerequisites. 2. Include benign designs that resemble vulnerabilities, particularly intentional admin powers, tenant boundaries and Solidity economic assumptions. 3. Run fixed model configurations against the same source snapshots. 4. Measure candidate recall, assessor precision, duplicated findings, false-positive dismissals, test quality, token/cost reservations and human triage time. 5. Check that the test distinguishes vulnerable and repaired implementations while exercising the same property. A proof that asserts the defect occurs should stop succeeding after repair; a safety regression assertion should fail on the defect and pass after repair. Do not accept compilation errors or missing tests as proof. 6. Compare against your existing static analyzers and human audit notes. Tune prompts/models using a training set and retain a separate evaluation set. Use the [comparative evaluation protocol] to assess model routing and review strategies under matched budgets. Measure audit costs and reviewer effort alongside detection quality; orchestration test results alone cannot establish those outcomes. ## Known implementation limits - A bounded, file-oriented review is not whole-program formal verification. Context can be partial; large files/lines and dependencies may be excluded. - Baseline non-Go symbol extraction is heuristic. Java/Solidity/Rust/C/C++ semantic queries need the selected LSP server and a correctly imported project. - Economic review records strategy and payoff assumptions but is not an equilibrium solver or a calibrated live market simulation. The reusable runner executes explicit project adapters, with synthetic examples and separate observations/controls. Finding quality and sensitivity to prompt/model choices need benchmark evaluation. - The LSP subset does not implement an entire editor client or guarantee server indexing has finished when every query is made. - Candidate fingerprints are deterministic. Optional model-proposed grouping preserves all findings and uses bounded windows, so cross-window duplicates may remain. - Local tools/tests and SSH execution are not a hostile-code sandbox. SSH uses operator-provided hosts; EC2 isolates hosts and test networking, with operator-prepared toolchains. - Model confidence is uncalibrated. A passing generated test is execution evidence, not independent vulnerability confirmation. - API compatibility targets text Chat Completions and Claude Messages; provider-specific APIs/auth extensions need additional adapters. - Cost reservations depend on operator rates and exclude AWS/tool charges. Interrupted upstream calls may be billed again. - Validation on live providers, large Java/Solidity projects, target-platform releases and AWS deployments is pending. Family-coverage integration tests check that all catalog families are assigned within the existing job count, neutral agents finish before guided work, supplied hints/taxonomies do not enter neutral prompts, fabricated execution links are rejected, and partial/disabled runs expose gaps. Set `KATARINA_COVERAGE_REPORT` to a temporary directory with `go test ./internal/engine -run TestEveryFamilyAssignedWithoutHintingIndependentAgents -count=1` to export a schema-validation fixture and audit handoff. These deterministic provider tests do not measure model detection quality. Distributed tests verify language-independent unhinted discovery, both 12-family software and 32-family mixed coverage, topology provenance, guidance through triage, and history-checker counterexamples/unknowns. Set `KATARINA_DISTRIBUTED_REPORT` with `go test ./internal/engine -run TestDistributedCoverageAndUnhintedDiscovery -count=1` to export a topology-bearing schema fixture. See the [distributed benchmark] for the separate pinned reference schedules. ## Keep user documentation current Binary bundles include documentation, schemas, examples and integration launchers; rebuilding docs alone does not update an existing executable or published archive. When defaults, workflow stages, commands or artifact contracts change, update the [Solidity workflow], [product specification], relevant reference guide and [starter configuration] in the same change. Distinguish fresh-init defaults from omitted fields in older configurations and from optional prepared infrastructure. Keep the architecture stage order aligned with `Engine.Run`. Rebuild the embedded manual with `make docs`; verify local links and run `doctor`/`index` plus a no-provider demo smoke with changed complete configuration examples. A valid demo checks usability and orchestration, not vulnerability detection. Repository docs and an older downloadable release need not describe the same capabilities; publish matching artifacts deliberately.
Integration references
# Integration references The following references document the integration interfaces and research background used by Katarina. The integration references were reviewed in September 2026. ## Runtime, providers and tools - [pi Rust SDK], [SDK source] and [upstream license]. - [OpenAI Chat Completions]. - [Claude Messages]. - [DeepSeek Chat Completions]. - [OpenRouter API overview]. - [Eclipse JDT Language Server]. - [Nomic Foundation Solidity language tools]. - [Slither] and [CLI usage]. - [Language Server Protocol]. - [AWS CloudFormation quick-create links]. - [AWS SSM SendCommand] and [GetCommandInvocation]. - [Microsoft MDASH announcement]. These establish integration contracts and background, not measured Katarina security performance. Model availability, prices, provider schemas and AWS behavior can change; validate the configuration used for each release and evaluation. ## Economic review and native-language tools - [Ethereum MEV documentation]: transaction-ordering background for protocol review. - [rust-analyzer configuration]: initialization options, Cargo project loading, build scripts and procedural macros. - [clangd installation and project setup]: compilation databases and compile_flags.txt limitations.