How Jelleo finds bugs before they become exploits.

The four pillars

Jelleo composes four interlocking pillars. All four run today — the engine source is public, so every claim below maps to code you can read.

How the pillars compose during a hunt cycle

Every cycle walks the same sequence. Pillar P1 watches mainnet for divergence; on a confirmed bug from any pillar, P2 propagates the pattern across the corpus; P3 closes the loop with a verified fix bundle; P4 records the cycle's verified invariants on-chain. The pillars are not phases — they run continuously, in parallel, and feed one another.

Ten stages · L0–L6.

Every engagement walks the same ten verification stages between a repository and a signed report. Each stage is independently invocable; hunt orchestrates them end to end and fires the propagation, fix-bundle, and attestation hooks.

Fix-bundle authoring (P3) and attestation (P4) run alongside the verifier stages, not as extra layers. The stage numbering is canonical to the engine source — cli.py documents the same L0–L6 scheme.

How Jelleo fits inside STRIDE.

Solana Foundation launched STRIDE on April 6, 2026 — a tiered, foundation-funded program covering eight security pillars across the ecosystem. STRIDE is the framework; Jelleo's signed artifacts map onto its smart-contract integrity pillar.

STRIDE's eight pillars span both opsec/threat-monitoring (Tier 1 surface) and smart-contract integrity (Tier 1 + Tier 2 deep verification). Jelleo's four pillars produce the artifacts that map onto the smart-contract integrity surface:

Jelleo does not compete with STRIDE — it is complementary. STRIDE evaluates programs holistically; Jelleo produces the depth artifacts protocols use to demonstrate the smart-contract integrity pillar at higher tiers.

Hypothesis library scoping

The hypothesis library is the engine's source of truth for "what to test." It compounds with every confirmed finding — meaning at scale (the bundled class libraries alone carry 814 hypotheses across 14 libraries) precision matters. Each hypothesis must declare exactly which protocols it applies to, under what conditions, and which generalized bug class it represents. Below is the schema.

Schema · per-hypothesis frontmatter

Every hypothesis is a YAML entry under hypotheses: in a hypotheses.yaml file (per workspace, per target). The required and optional fields:

id

Unique short identifier (e.g. H1-residual-conservation). Stable across cycles. Used as the cross-DB key.

class

One of: invariant_property, state_transition, authorization, arithmetic_overflow, implicit_invariant. Determines which L2 PoC strategy and L3 formal harness the hunt loop selects.

claim

The falsifiable claim in plain English. Phrased so a clean negative result strengthens the disclosure.

severity

One of: Critical, High, Medium, Low, Info. Sets the floor on auto-derived severity (see §06).

applies_to (scoping field)

List of protocol names this hypothesis applies to. Used by the loader to filter which hypotheses run against which target. Wildcard ['*'] matches all protocols. Example: [percolator, drift, mango].

scope_conditions (optional)

Predicate(s) that must be true for the hypothesis to be relevant. E.g. has_insurance_pool, uses_pyth_oracle, perpetual_funding.

bug_class (required · the propagation key)

Generalized class identifier for cross-protocol propagation (§05). When this hypothesis confirms TRUE on protocol A, Jelleo dispatches the same generalized class against every other protocol where applies_to matches.

target_file, relevant_constants, relevant_instructions

Anchor fields used by the recon agent to focus its initial reading window. Loader does not filter on them.

Example · F7 hypothesis with full scoping

- id: H1-residual-conservation
  class: invariant_property
  claim: >
    The post-haircut residual cash on a market
    (vault - cash_locked_in_orderbook - claimable_pnl - insurance_counter)
    is conserved by every internal accounting helper. If any helper shrinks
    the insurance counter, it MUST also debit the vault by the same amount.
  severity: Critical
  applies_to: [percolator, drift, mango, marginfi]
  scope_conditions: [has_insurance_pool, has_haircut_accounting]
  bug_class: insurance-counter-vault-divergence    # the propagation key
  target_file: src/percolator.rs

Loader semantics

When audit-pipeline hunt runs against target T with conditions C (derived from workspace.json), the loader applies a 3-step filter to every hypothesis in hypotheses.yaml:

1. applies_to filter: hypothesis loads only if T ∈ applies_to or '*' ∈ applies_to.
2. scope_conditions filter: hypothesis loads only if every predicate evaluates true under target conditions.
3. severity floor: if invoked with --min-severity High, hypotheses below that floor are skipped.

The result: at scale, a target only ever sees the hypotheses that actually apply to it. The library can grow to thousands of entries without any single cycle being polluted by irrelevant claims.

Engineering reference: the canonical schema spec — including the full predicate vocabulary, validation rules, and migration plan — lives at docs/HYPOTHESIS_SCHEMA.md in the platform repo. The JSON Schema at src/audit_pipeline/schemas/hypothesis.schema.json is consumed by the loader and by editor tooling.

Auto-learning across the cluster.

Bug classes recur. F7's "shrink insurance counter without debiting the vault" pattern probably exists in any protocol with insurance accounting; CatchupAccrue's "advance the clock without touching the accounts" pattern probably exists in any protocol with multi-instruction settlement. Jelleo's propagation engine is how we find them — every customer benefits from every other customer's findings.

Trigger

Whenever a hypothesis H on protocol A moves to status confirmed (PoC fired or debate-promoted), the propagation engine fires. The engine takes H's bug_class, looks up every protocol in the corpus whose applies_to includes H's class generalization, and dispatches the same hypothesis class — in parallel — against every matching protocol.

Pipeline

// the moment a finding moves to status=confirmed, this loop fires
1. Confirmed finding on protocol A · cycle K
2. Extract bug_class signature (regex set + structural pattern)
3. Walk the corpus (15+ protocols, indexed)
4. For each candidate file in each protocol:
     - signature match score = count(distinct signatures hit)
     - if score >= MIN_SCORE: emit candidate
5. Top candidates dispatched to Layer 1 (recon agent)
6. Layer 1 verdicts feed back into the per-protocol findings DB
7. Customer of every affected protocol gets:
     - email notification (immediate, on confirmed propagation)
     - dashboard update
     - 24h report row
8. Cluster-level metric: bug-class hit rate, time-to-detect, false-positive rate

Customer notification on cross-protocol re-test

If your protocol gets re-tested because a bug class confirmed on someone else's protocol, you receive an immediate email of the form:

Subject: [Jelleo] Cross-protocol re-test · <your-protocol> · bug_class=X

We confirmed bug class <X> on <other-protocol> on <date>.
We re-tested <your-protocol> against the same class.

Result: PASS · <n> hypotheses dispatched, all green
        OR
        REVIEW · <n> candidates flagged for Layer-2 escalation

Full report: https://jelleo.com/customer/<your-token>/

This is the "auto-learning" property: the cluster's collective coverage compounds. Every confirmed bug class adds permanent re-test coverage across every applicable protocol.

Implementation

The corpus is initialized once with audit-pipeline propagate init-corpus (15 popular Solana programs by default — Drift, Mango, Marginfi, Kamino, Phoenix, OpenBook, Orca, Meteora, Raydium, Marinade, Anchor, SPL, plus the engine under audit). Each protocol is shallow-cloned for fast indexing. The search itself is audit-pipeline propagate search -c <corpus> -s '<sig1>' -s '<sig2>', with intentionally simple regex matching to keep the indexer fast and language-agnostic. Top hits escalate to a Layer-1 agent for deep verification.

Five tiers · formal definitions

Severity is what the customer sees first. The rubric is stable, auditable, and consistent across cycles. Every finding gets a tier; tiers are derived, not negotiated.

Auto-derivation

If the hypothesis YAML declares an explicit severity:, that becomes the floor. Otherwise the severity is derived from (class, verdict, poc_fired, debate_promoted) per:

1. PoC fired AND class is invariant_property or authorization  →  Critical
2. PoC fired (any other class)  →  High
3. Verdict TRUE + debate-promoted (no PoC yet)  →  High
4. Verdict TRUE (no debate, no PoC)  →  Medium
5. Verdict NEEDS_LAYER_2_TO_DECIDE  →  Low
6. Otherwise  →  Info

Source: severity.derive_severity() in the platform package. The same function is used by the report generator and the dashboard so the customer's view never disagrees with the on-disk record.

State machine · eight states, restricted transitions

Every finding is a row in the SQLite findings DB with a status column. Transitions are restricted so the audit trail is honest — you cannot jump from a brand-new finding to "fixed" without walking the chain. Every transition is logged in an append-only transitions table.

Source: lifecycle.py · VALID_TRANSITIONS. Invalid transitions raise InvalidTransition at the DB layer, before the row is touched. The full per-finding history is retrievable via db.transitions_for(finding_id).

Signed receipts · Ed25519.

Every audit cycle produces a signed receipt. Customers can verify the receipt against the published Jelleo public key without trusting us: domain-separated Ed25519 signatures and per-cycle Merkle roots off-chain, plus an on-chain Anchor registry live on Solana devnet since 2026-05-29 — mainnet follows an external audit of the program itself.

What gets signed

• The cycle report — HTML and PDF — for every hunt cycle
• The per-cycle Merkle sidecar (merkle.json): findings rooted at a commit SHA
• The per-finding disclosure package (when a finding moves to disclosed)
• The hourly heartbeat, hash-chained to the previous beat
• The weekly / monthly rollup PDF

Receipt format

-----BEGIN JELLEO SIGNATURE-----
Algorithm: Ed25519
Schema: jelleo-sign/v2
Domain: report
Signed-At: 2026-06-05T17:01:54+00:00
Signed-File: cycle.html
Signed-Bytes: 102207

<base64 signature>
-----END JELLEO SIGNATURE-----

Verification

The Jelleo Ed25519 public key is published at api.jelleo.com/keys/jelleo.ed25519.pub. Signatures are domain-separated — a report signature cannot be replayed as a heartbeat or bundle signature. To verify:

$ curl -sO https://api.jelleo.com/keys/jelleo.ed25519.pub
$ audit-pipeline sign verify <file> <file>.sig --pubkey jelleo.ed25519.pub
✓ VALID signature on cycle.html

A valid signature confirms (a) the file's bytes have not been altered since signing, and (b) the file was signed by the platform key — meaning the cycle ran in a Jelleo workspace with a private key matching the published public key. The on-chain registry extends this: the same Merkle roots, published to the chain.

On-chain registry (live on devnet)

P4 publishes each cycle's Merkle root on-chain via a hardened Anchor program — 72TF95FUNttvDDsQSFzWEqY7Vu6Xm5h81fFNgoeRYPTk, deployed to Solana devnet on 2026-05-29 with real attestation transactions. The Merkle leaves are per-finding hashes; the root binds the cycle's findings to the audited commit SHA. Mainnet deployment is deliberately gated behind an external audit of the program itself.

Three cadences · one urgency channel

Customers do not wait for a report cycle to find out about a critical bug. The cadence reports are summaries; urgent findings push immediately.

Cadence

Trigger semantics for the immediate channel

The immediate email fires when a finding's status moves from new or triaged to confirmed, AND severity is Critical or High. There is no batching, no daily digest. The customer's primary on-call gets the email; their team alias gets a CC. The same event fires the dashboard alert pulse and (if configured) the Slack webhook.

Customer dashboard

Each customer accesses their dashboard via a token-gated portal at jelleo.com/customer/. The token resolves to a per-customer view that pulls live state from the findings DB via a static-JSON snapshot and refreshes on a configurable interval (default 60s). Status pills, severity bars, recent cycles, recent findings, daemon health. The universal demo token is demo.

What's signed, what's not

Every PDF rollup (24h / weekly / monthly) ships with a Jelleo Ed25519 signature alongside (§07). The dashboard view itself is not signed — it is a live mirror of state. Customers who need a signed point-in-time snapshot request a rollup at any moment via audit-pipeline report cycle --cycle-id <id> followed by sign sign <file>.

Disclosure embargo

Reports include findings in the disclosed state in summary form (severity, bug-class, embargo countdown) but withhold reproduction details until the embargo lifts. Defaults: 30 days for High, extensible to 90 days; Critical findings get maximum embargo flexibility while a fix is in flight. Full policy and timeline at jelleo.com/security.html.

F7 · the inaugural finding

F7 is the proof that the methodology works on real code. It was the first hypothesis to confirm against Anatoly's Percolator engine, in April 2026 — disclosed in PR #39, closed without merge, with the regression suite landing on main at a1afd2e approximately one month later.

Bug class

insurance-counter-vault-divergence — the helper use_insurance_buffer shrinks the insurance counter without correspondingly debiting the vault. The post-haircut residual cash on the market grows by the absorbed amount, and the K/F-winning side claims it. A self-trade nets (ΔK − IM) · N and captures the insurance fund.

Each pillar's contribution to F7

1. Hypothesis library: H1-residual-conservation (class invariant_property) declared the conservation property that use_insurance_buffer violated.
2. Layer-1 recon (P2-adjacent): Multi-agent code review converged on the helper as the failing point.
3. Layer-1.5 debate: An adversarial second-opinion agent flipped an early "epoch-staleness" lead that was REFUTED, and re-anchored the hunt on the residual-formula bug — which proved correct.
4. Layer-2 PoC (P3 scaffold): Auto-generated cargo test fired against the engine helper, demonstrating the residual delta. cargo test PASS.
5. Layer-4 LiteSVM (P3 escalation): BPF-level reproduction in LiteSVM at commit 43cdcd8 — the PoC test exists in PR #39's test suite.
6. P4 attestation: The cycle was signed (Ed25519); the verification key is published.

What was disclosed

PR #39 contained: (a) the LiteSVM reachability test demonstrating the drain, (b) the suggested fix (debit the vault concurrently with the counter shrink), (c) the Markdown writeup explaining the bug-class. The PR was closed without merge — the maintainer landed an A1 regression suite on main at a1afd2e independently. The fix verified locally across 277 unit tests with zero regressions.

Cross-protocol propagation status

F7's bug_class (insurance-counter-vault-divergence) is a candidate for cross-protocol propagation against any indexed protocol with insurance accounting. The propagation engine re-runs this class automatically whenever a related finding confirms. The initial sweep against the corpus found no immediate hits — the signature is structurally specific to Percolator's helper geometry. The pattern matcher remains armed.

Same four pillars · four languages.

The four-pillar architecture (Detection · Propagation · Fix Bundle · Attestation) is language-agnostic. What changes per language is the adapter layer: which symbolic verifier runs at L3, which runtime harness runs at L4, and which test runner produces the L2 abort signal. All four are live — Solana (BPF / Rust), Aptos (Move), Solidity, and C — and a fifth rendering path covers TypeScript and generic targets at the report layer.

Worked example · Aptos cycle 20260513-191318 (osec-aptos-small)

The Mutatis Aptos benchmark (small tier) ran end-to-end through the four pillars:

• 40 hypotheses dispatched from the Aptos hypothesis class library (authorization, arithmetic, accounting, capability handling, event auditability, oracle freshness).
• 7 PoC fires at Layer 2 (test aborted in target module with custom error code).
• 4 STRONG after Layer 2.5 triage filtered 1 SOFT (wrong invariant) and 2 FALSE (stdlib / setup abort, not target).
• 2 root causes after the clustering rule collapsed 3 STRONG fires hitting transfer_admin in access_control.move into one finding.
• 2 Critical findings published:
  • Missing auth check on transfer_admin — covers APT1 / APT4 / APT5 hypotheses.
  • Permissionless emergency_drain drains the vault — APT38.
• $11.62 total LLM spend, 2m 16s wall-clock.

Per line of code.

Continuous audit, billed per line of in-scope code — the same engagement structure top firms use, just continuous instead of one-shot. We count in-scope program code only: never tests, comments, generated code, or dependencies. Engagement length is open-ended and renews annually.

Year 1 is the onboarding scan plus continuous coverage — $12/LOC all-in — then $5/LOC/yr thereafter. A 14,000-LOC program runs ~$168K in year one and ~$70K/yr after, anchored against what one exploit costs and what re-hiring a firm for every release costs. Every engagement includes: signed cycle receipts (§08), 24h / weekly / monthly reports (§09), live dashboard, immediate notification on Critical/High (§09), operator-authorized disclosure filing on confirmed findings, formal proofs on Critical/High, P3 fix bundles, and access to the cross-protocol propagation channel (§05).