Skip to content
thehalleyyoungPublic

About

No description, website, or topics provided.

Resources

Stars

7 stars

Watchers

0 watching

Forks

Latest commit

 

History

48 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

A3: Advanced Automated Analysis for Python

A3 is a static bug finder for Python. It combines non-LLM static analysis with optional LLM triage:

  1. Static analysis first: bytecode analysis, guard detection, barrier-style suppression patterns, and Z3-backed symbolic execution produce a list of candidate bugs and suppress candidates that look guarded.
  2. LLM triage second (optional): an LLM agent reads the code around each remaining finding (files, guards, callers, tests) and labels it TP or FP.

See Evaluation status for what has and has not been measured. In short: the only reproducible measurement is on a small self-written benchmark; there is no held-out real-bug evaluation, and the accuracy of LLM triage has not been measured.

Python 3.11+ PyPI

Quick Start

Install

pip install a3-python

Requires Python ≥ 3.11. The only core dependency is z3-solver (installed automatically).

For CI features (GitHub Actions workflows, LLM triage, SARIF output):

pip install a3-python[ci]

Scan a project

a3 scan . --output-sarif results.sarif

On a directory, A3 runs a seven-step pipeline (call graph, crash summaries, code objects, bug-type coverage, guard detection plus barrier-pattern suppression, DSE, production/test split) and reports the remaining candidates.

Scan + agentic triage (end-to-end, single command)

a3 scan . --triage

That's it — one command. A3 scans, writes SARIF, then auto-detects your API key (OPENAI_API_KEY, ANTHROPIC_API_KEY, or GITHUB_TOKEN) and launches an agentic triage where the LLM explores the codebase using tools (reading files, searching for guards, checking callers and tests) before classifying each finding. Findings the LLM labels as false positives are dropped from the output.

You can also specify the provider explicitly:

a3 scan . --triage openai --output-sarif results.sarif
a3 scan . --triage github                # uses GITHUB_TOKEN
a3 scan . --triage anthropic              # uses ANTHROPIC_API_KEY

Using GitHub Models locally (no separate API key)

If you have the GitHub CLI installed and authenticated (gh auth login), you can use GitHub Models for triage locally — no API key signup required:

export GITHUB_TOKEN=$(gh auth token) && a3 scan . --triage github --verbose

This exports your existing GitHub CLI token and uses it to access GitHub Models for agentic triage. In CI (GitHub Actions), GITHUB_TOKEN is already available automatically.

Or run scan and triage as separate steps:

a3 scan . --output-sarif results.sarif
a3 triage --sarif results.sarif --provider openai --agentic --verbose

Directory scans vs. single-file scans

A directory target always runs the fixed seven-step pipeline described in How It Works. For directory targets the analysis flags (--interprocedural, --dse-verify, --deduplicate, --no-kitchensink, --context-depth, --functions, ...) and the matching .a3.yml analysis: keys are accepted but have no effect; --min-confidence is only passed to triage. Those flags apply to single-file targets:

# Single file: kitchensink portfolio (default)
a3 scan path/to/module.py

# Single file: interprocedural crash/taint analysis
a3 scan path/to/module.py --interprocedural --min-confidence 0.3

Output SARIF for GitHub Code Scanning

a3 scan /path/to/project --output-sarif results.sarif

Upload the SARIF file to GitHub's Code Scanning dashboard, or use the built-in CI integration (see below).


Evaluation status

What has been measured, as of October 2026:

  • Synthetic benchmark (py_synthetic/, 44 self-written files with planted DIV_ZERO, BOUNDS, NULL_PTR and ASSERT_FAIL bugs; 38 buggy, 6 safe). Re-run with the current code: 35 TP, 5 FP, 1 FN, 1 TN, 2 errors; precision 0.875, recall 0.972. A file counts as detected if any bug is reported. Only 1 of the 6 safe files is classified as safe. Details in py_synthetic/README.md.
  • Test suite: 2138 tests collect. In a full run (2 workers, 120 s per-test timeout) 1988 passed, 87 failed, 29 skipped, 19 xfailed, 16 xpassed; fixing stale module names in four CLI test files turned 5 of the failures into passes, leaving about 82 failures. There is no CI job that runs the test suite.
  • Large-repo run time: a directory scan of DeepSpeed at upstream HEAD (about 1,100 Python files) did not finish within 45 minutes on a heavily loaded machine (stopped at about 29% of 6,773 functions). No timing figure is claimed.

What has not been measured:

  • Real-bug recall or precision. BugsInPy was used to drive LLM-written patches to the analyzer, and a3_python/ contains detectors written for individual BugsInPy bugs (see comments such as "black#6 pattern", "keras#1 pattern"), so it is not a held-out test set. No BugsInPy results are committed.
  • False-positive suppression. The "Proven FP" count printed by directory scans includes findings suppressed by heuristic patterns (confidence >= 0.6), not only proofs. How many real bugs these patterns hide is unknown.
  • LLM triage accuracy, one-shot or agentic.
  • Comparison with other tools (CodeQL, Bandit, Pyright, Semgrep).

The per-repository write-ups in docs/true_positives/ and the DeepSpeed notes in docs/ are manual reviews of earlier scans; the scanner output they are based on is not in the repository, and the DeepSpeed totals in different notes disagree (2,638, 4,261 and 16,049 raw findings).


Continuous CI with Agentic Triage

A3 ships with GitHub Actions workflows that continuously scan every push and every PR using a two-phase approach:

  1. Non-LLM static analysis scans the repo and suppresses candidates that look guarded
  2. Agentic LLM triage investigates the remaining findings: the LLM reads source files, searches for guard patterns, checks callers and tests, then classifies each finding. In GitHub Actions it uses the built-in GITHUB_TOKEN, so no extra API key is needed

Every GitHub Actions runner already has a GITHUB_TOKEN, which gives access to GitHub Models. That's all the agentic triage needs.

Add to a repo

cd your-repo/
pip install a3-python[ci]
a3 init . --copilot
git add .github/ .a3.yml .a3-baseline.json
git commit -m "ci: add a3 static analysis"
git push

That's it. Every push to main/master and every PR that touches Python files will now be scanned, triaged by an agentic LLM, and checked against the baseline. Results appear in GitHub's Code Scanning dashboard (Security → Code scanning alerts).

What a3 init --copilot creates

File What it does
.github/workflows/a3-pr-scan.yml On every push & PR: scans the repo → agentic LLM investigates each finding (reads files, searches patterns, checks callers) → blocks if new bugs found → uploads SARIF
.github/workflows/a3-scheduled-scan.yml Weekly (Monday 6 AM UTC): full-repo scan → agentic triage → auto-files GitHub Issues for new TPs → updates baseline
.a3.yml Analysis configuration (what to scan, confidence thresholds, etc.)
.a3-baseline.json Known-findings baseline for the ratchet (starts empty)

How it works end-to-end

push to main/master — or — PR opened (touches .py files)
  │
  ├─ 1. Non-LLM static analysis scans the repo
  │     • Bytecode analysis + Z3 symbolic execution
  │     • Suppresses candidates that look guarded
  │     • Outputs SARIF with the remaining findings
  │
  ├─ 2. Agentic LLM triage (multi-turn tool-use)
  │     • For each surviving finding, an LLM agent:
  │       - Reads the flagged function's source code
  │       - Searches for guard checks, callers, tests
  │       - Follows imports and explores related files
  │       - Calls 'classify' with verdict + rationale
  │     • Uses GITHUB_TOKEN → GitHub Models (zero config)
  │
  ├─ 3. Baseline ratchet check
  │     new bugs not in baseline → ❌ CI fails
  │     all bugs already known   → ✅ CI passes
  │
  └─ 4. SARIF uploaded to GitHub Code Scanning dashboard
        findings appear under Security → Code scanning alerts

Example: What the workflow file looks like

When you run a3 init . --copilot, it creates .github/workflows/a3-pr-scan.yml. Here's the key steps:

# .github/workflows/a3-pr-scan.yml
# Triggers on: push to main/master, all PRs touching .py files

- name: Get changed files
  id: changed
  run: |
    git diff --name-only --diff-filter=ACMR "$BASE"...HEAD -- '*.py' > changed_files.txt

- name: Run a3
  run: |
    a3 scan . \
      --output-sarif a3-results.sarif

- name: Agentic triage
  env:
    GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}  # provided by GitHub Actions
  run: |
    a3 triage \
      --sarif a3-results.sarif \
      --output-sarif a3-triaged.sarif \
      --repo-root . \
      --provider github \
      --model gpt-4o \
      --agentic \
      --verbose
    mv a3-triaged.sarif a3-results.sarif

- name: Check baseline
  run: a3 baseline diff --sarif a3-results.sarif

- name: Upload SARIF
  uses: github/codeql-action/upload-sarif@v3
  with:
    sarif_file: a3-results.sarif

The agentic triage step gives the LLM tools to explore the repo — read_file, search_codebase, get_function_source, get_imports, list_directory — so it can check callers, find tests, verify guards, and understand context before classifying each finding.

The ratchet: incremental adoption for large codebases

The baseline file records all accepted findings. On each PR:

  • New findings not in baseline → CI fails. The author must fix the bug or explicitly accept it.
  • Findings that disappear → auto-pruned. The codebase is getting healthier.
  • Pre-existing issues → ignored. You're never blocked on legacy debt.
# Check for new findings (exits 1 if any are new)
a3 baseline diff --sarif results.sarif

# Accept current findings into baseline
a3 baseline accept --sarif results.sarif

Two Usage Patterns

Scenario A: Whole-Repo Scan

Scan every Python file in one pass. Best for first-time adoption, weekly audits, or establishing a baseline.

# Scan the entire repository
a3 scan . --output-sarif results.sarif

# Agentic triage (optional — filters remaining false positives)
a3 triage --sarif results.sarif --provider github --agentic \
  --output-sarif triaged.sarif

# Lock current findings as the baseline (ratchet start)
a3 baseline accept --sarif triaged.sarif
git add .a3-baseline.json && git commit -m "ci: establish a3 baseline" && git push

The scheduled workflow (a3-scheduled-scan.yml) repeats this automatically every week.

Scenario B: Incremental — Auto-Invoke on Every Python File Change

After a3 init . --copilot, the generated a3-pr-scan.yml triggers whenever a .py file is added or modified:

on:
  push:
    branches: [main, master]
    paths:
      - "**.py"               # triggers only when .py files change
  pull_request:
    paths:
      - "**.py"

Example — adding a new file:

cat > src/payments.py << 'EOF'
def charge(amount, discount):
    return amount / discount   # DIV_ZERO: discount could be 0

def refund(amount, count):
    if count > 0:
        return amount / count  # SAFE: guarded by count > 0
    return 0.0
EOF

git add src/payments.py
git commit -m "feat: add payment processing"
git push   # CI triggers because a .py file changed

What happens automatically:

  1. Push triggers a3-pr-scan.yml (path filter matches **.py)
  2. Workflow lists changed files via git diff --name-only; if any .py file changed, it runs a3 scan . on the whole repository (the changed-file list is only used to decide whether to run)
  3. The scan reports DIV_ZERO in charge() (DSE finds a reaching input) and counts the division in refund() as guarded (checked with a3 0.1.23 on this exact file)
  4. Baseline diff: a finding not in the baseline makes CI fail until the bug is fixed or accepted

Non-Python changes (docs, configs, images) do not trigger the workflow at all.


Using a different LLM provider (optional)

If you prefer Claude or GPT-5 via your own API key instead of GitHub Models (the default provider for a3 triage is github):

# Anthropic (Claude)
export ANTHROPIC_API_KEY=sk-...
a3 triage --sarif results.sarif --provider anthropic --output-sarif triaged.sarif --agentic

# OpenAI (GPT-5)
a3 triage --sarif results.sarif --provider openai --model gpt-5 --agentic

# GitHub Models (via GITHUB_TOKEN; subject to GitHub Models rate limits)
a3 triage --sarif results.sarif --provider github --agentic

For third-party providers in GitHub Actions, add the API key as a repository secret:

- name: LLM triage (Anthropic)
  env:
    ANTHROPIC_API_KEY: ${{ secrets.ANTHROPIC_API_KEY }}
  run: a3 triage --sarif a3-results.sarif --provider anthropic --output-sarif a3-triaged.sarif --agentic

Configuration

Create a .a3.yml in your repo root (or use a3 init to generate one):

analysis:                      # these keys only affect single-file scans
  interprocedural: true
  # kitchensink: true by default (symbolic execution portfolio)
  dse-verify: true
  min-confidence: 0.3
  deduplicate: true

ci:
  fail-on-new-bugs: true
  baseline-file: .a3-baseline.json
  llm-triage: true             # enabled by default with --copilot
  llm-provider: github         # uses GITHUB_TOKEN — no extra API keys
  llm-model: gpt-5
  sarif-upload: true

scan:
  exclude:
    - "tests/**"
    - "docs/**"
    - "**/test_*.py"

When a config file is present, a3 scan reads it automatically — no flags needed.


CLI Reference

a3 scan

Run static analysis on a file or project.

a3 scan <target> [options]
a3 <target> [options]           # legacy syntax, same behavior

Analysis flags (single-file targets only; ignored for directories):

Flag Description
--interprocedural Cross-function analysis with call graph and summaries
--no-kitchensink Disable symbolic execution portfolio (enabled by default)
--dse-verify Verify bugs with Z3-backed symbolic execution
--deduplicate Deduplicate findings by type + location
--min-confidence N Filter by confidence score (0.0–1.0, default: 0.7)
--no-concolic Disable concrete execution (pure symbolic/static analysis)
--max-dse-steps N DSE step budget per function for --dse-verify (default: 100)
--no-intent-filter Report all bugs regardless of intent classification
--functions Treat each function as a tainted entry point (security mode)
--all-functions Analyze every function as an entry point
--context-depth N k-CFA context sensitivity (0, 1, 2, …)
--check-termination Detect non-terminating loops
--synthesize-invariants Generate inductive loop invariants

Output flags:

Flag Description
--output-sarif PATH Write SARIF 2.1.0 JSON
--triage [PROVIDER] Run agentic triage after scan (auto-detects API key, or specify: openai, anthropic, github)
--triage-model MODEL LLM model for integrated triage (default: provider-appropriate)
--triage-api-key KEY API key for integrated triage (default: from env var)
--save-results PATH Write results as JSON (default: results/<name>_results.json)
--verbose Detailed step-by-step output
--config PATH Path to .a3.yml

Exit codes: 0 = no bugs, 1 = bugs found, 2 = unknown, 3 = error.

a3 init

Bootstrap a repository with CI workflows and config.

a3 init [repo_path]             # default: current directory
a3 init . --copilot             # enable Copilot triage (recommended)
a3 init . --llm-triage          # enable triage with Anthropic/OpenAI
a3 init . --overwrite           # replace existing files

a3 triage

Classify findings via agentic LLM investigation.

a3 triage --sarif results.sarif --provider github --agentic     # GitHub Models (default provider)
a3 triage --sarif results.sarif --provider anthropic --output-sarif triaged.sarif --agentic
a3 triage --sarif results.sarif --provider openai --model gpt-5 --agentic
a3 triage --sarif results.sarif --verbose --agentic

The --agentic flag enables multi-turn tool-use: the LLM can read files, search for patterns, inspect callers, check tests, and explore the repo before classifying each finding. Without --agentic, a simpler one-shot prompt is used.

Providers: github (uses GITHUB_TOKEN), anthropic (uses ANTHROPIC_API_KEY), openai (uses OPENAI_API_KEY). Pass --api-key to override.

a3 baseline

Manage the findings baseline (ratchet).

a3 baseline diff --sarif results.sarif        # check for new bugs
a3 baseline accept --sarif results.sarif      # update baseline
a3 baseline diff --sarif results.sarif --auto-issue  # file GitHub issues

Bug Types

The registry in a3_python/unsafe/registry.py defines unsafe-state predicates for 84 bug types. Having a predicate does not mean a type is detected reliably; the only benchmarked types are DIV_ZERO, BOUNDS, NULL_PTR and ASSERT_FAIL (see Evaluation status). Some names are carried over from C/Rust-style taxonomies (USE_AFTER_FREE, DOUBLE_FREE, UNINIT_MEMORY, SEND_SYNC) and model Python analogues such as use of closed resources.

Core crash types (19)

ASSERT_FAIL · DIV_ZERO · FP_DOMAIN · INTEGER_OVERFLOW · BOUNDS · NULL_PTR · TYPE_CONFUSION · STACK_OVERFLOW · MEMORY_LEAK · NON_TERMINATION · ITERATOR_INVALID · USE_AFTER_FREE · DOUBLE_FREE · UNINIT_MEMORY · DATA_RACE · DEADLOCK · SEND_SYNC · INFO_LEAK · TIMING_CHANNEL

Exception types (17, plus PANIC)

VALUE_ERROR · RUNTIME_ERROR · NOT_IMPLEMENTED · FILE_NOT_FOUND · PERMISSION_ERROR · OS_ERROR · IO_ERROR · IMPORT_ERROR · MODULE_NOT_FOUND · NAME_ERROR · UNBOUND_LOCAL · TIMEOUT_ERROR · CONNECTION_ERROR · UNICODE_ERROR · LOOKUP_ERROR · SYSTEM_ERROR · ENVIRONMENT_ERROR

Security types (47)

Injection: SQL_INJECTION · COMMAND_INJECTION · CODE_INJECTION · PATH_INJECTION · LDAP_INJECTION · XPATH_INJECTION · NOSQL_INJECTION · REGEX_INJECTION · HEADER_INJECTION · COOKIE_INJECTION · LOG_INJECTION · UNSAFE_SHELL_COMMAND_CONSTRUCTION

Web: REFLECTED_XSS · SSRF · PARTIAL_SSRF · URL_REDIRECT · CSRF_PROTECTION_DISABLED · FLASK_DEBUG · INSECURE_COOKIE · JINJA2_AUTOESCAPE_FALSE · STACK_TRACE_EXPOSURE · INCOMPLETE_URL_SUBSTRING_SANITIZATION · UNTRUSTED_DATA_TO_EXTERNAL_API

Crypto: WEAK_CRYPTO · WEAK_CRYPTO_KEY · BROKEN_CRYPTO_ALGORITHM · WEAK_SENSITIVE_DATA_HASHING · INSECURE_PROTOCOL · INSECURE_DEFAULT_PROTOCOL

Deserialization / XML: UNSAFE_DESERIALIZATION · XXE · XML_BOMB

Secrets: CLEARTEXT_LOGGING · CLEARTEXT_STORAGE · HARDCODED_CREDENTIALS

Files / network / auth: TAR_SLIP · INSECURE_TEMPORARY_FILE · WEAK_FILE_PERMISSIONS · BIND_TO_ALL_INTERFACES · MISSING_HOST_KEY_VALIDATION · CERT_VALIDATION_DISABLED · PAM_AUTHORIZATION_BYPASS

Regex: REDOS · POLYNOMIAL_REDOS · BAD_TAG_FILTER · INCOMPLETE_HOSTNAME_REGEXP · OVERLY_LARGE_RANGE


How It Works

Phase 1: Non-LLM static analysis

For a project directory, a3 scan prints seven steps. No LLM is involved, but several steps use heuristics:

  1. Call graph from all .py files
  2. Crash summaries: bytecode disassembly to find divisions, possible None dereferences, indexing, taint flows and other unsafe operations
  3. Code objects for DSE
  4. Bug-type coverage report
  5. Guard detection and barrier-pattern suppression: findings protected by if, try/except, assert or isinstance checks are marked guarded; the remaining ones go through 8 barrier patterns (a3_python/barriers/deep_barrier_theory.py). A finding is suppressed if any pattern returns a certificate with confidence >= 0.6. Several patterns are heuristics (for example, one fires on function names containing get_, load or parse; another fires when a function contains any STORE_FAST), so a suppressed finding is not proven safe, even though the CLI prints "Proven FP"
  6. DSE: Z3-backed directed symbolic execution reports a finding as reachable (with a witness) or unreachable
  7. Classification into production code and test code

Single-file scans use a different path (symbolic execution with the kitchensink portfolio, which runs a sequence of re-implemented verification techniques). Each reported candidate falls into one of these groups:

Group Meaning
Suppressed Guarded, matched a barrier pattern, or DSE found it unreachable
Candidate Not suppressed; reported (and sent to LLM triage if enabled)
DSE-witnessed DSE found an input that reaches the unsafe operation

Phase 2: Agentic LLM triage (optional)

For findings that survive static analysis, A3 launches an agentic investigation — a multi-turn conversation where the LLM has access to tools:

Tool What it does
read_file Read any source file (with optional line range)
search_codebase Grep for regex patterns across the project
get_function_source Look up any function by name
get_imports See what a file imports
list_directory Explore project structure
classify Submit final TP/FP verdict with confidence + rationale

The agent decides which tools to call and then calls classify with its verdict. Without --agentic, a one-shot prompt is used instead. The accuracy of either mode has not been measured.


Examples

Quick Demo: Detecting Real Bugs

# examples.py

def authenticate_user(username, user_database):
    """Look up user credentials from database."""
    user_record = user_database.get(username)
    return user_record['password_hash']  # NULL_PTR: user_record could be None

def calculate_completion_rate(completed, total):
    """Calculate completion percentage."""
    return (completed / total) * 100  # DIV_ZERO: total could be 0

def get_database_host(config):
    """Extract database host from config."""
    return config.database.host  # NULL_PTR: config or database could be None

def get_latest_transaction(transactions):
    """Get the most recent transaction."""
    sorted_txns = sorted(transactions, key=lambda t: t.date, reverse=True)
    return sorted_txns[0].amount  # BOUNDS: sorted_txns could be empty

def extract_email_from_csv(csv_line):
    """Parse email from third column of CSV."""
    fields = csv_line.split(',')
    return fields[2].strip()  # BOUNDS: might not have 3 columns

def calculate_roi(profit, cost):
    """Calculate return on investment."""
    return (profit / cost) * 100  # DIV_ZERO: cost could be 0

def get_product_total_price(inventory, product_id):
    """Calculate total price including tax."""
    product = inventory.lookup(product_id)
    return product.base_price * (1 + product.tax_rate)  # NULL_PTR: product could be None

Run a3 (output from a3 0.1.23 at this commit, Python 3.12; banner lines omitted):

$ a3 scan examples.py --interprocedural

============================================================
INTERPROCEDURAL ANALYSIS RESULTS
(High-confidence TPs only, threshold=0.7)
============================================================
Total bugs found: 5

BOUNDS (2)
  [BUG] BOUNDS (line 16)
  - examples.get_latest_transaction
    examples.py:16
    Confidence: 0.76
  [BUG] BOUNDS (line 21)
  - examples.extract_email_from_csv
    examples.py:21
    Confidence: 0.76

DIV_ZERO (2)
  [BUG] DIV_ZERO (line 26)
  - examples.calculate_roi
    examples.py:26
    Confidence: 0.84
  [BUG] DIV_ZERO (line 8)
  - examples.calculate_completion_rate
    examples.py:8
    Confidence: 0.84

NULL_PTR (1)
  [BUG] NULL_PTR (line 3)
  - examples.authenticate_user
    examples.py:3
    Confidence: 0.76

Exit code 1. Five of the seven planted bugs are reported. The two attribute-access cases (get_database_host, get_product_total_price) are not reported, even with --min-confidence 0.1.

Guard Detection: Safe vs Unsafe Code

The same functions with guards added:

# examples_safe.py

def authenticate_user(username, user_database):
    """SAFE: Checks if user exists."""
    user_record = user_database.get(username)
    if user_record is not None:
        return user_record['password_hash']
    return None

def calculate_completion_rate(completed, total):
    """SAFE: Checks for zero before division."""
    if total != 0:
        return (completed / total) * 100
    return 0.0

def get_database_host(config):
    """SAFE: Validates nested attributes."""
    if config is not None and config.database is not None:
        return config.database.host
    return "localhost"

def get_latest_transaction(transactions):
    """SAFE: Checks if list is empty."""
    sorted_txns = sorted(transactions, key=lambda t: t.date, reverse=True)
    if len(sorted_txns) > 0:
        return sorted_txns[0].amount
    return 0.0

def extract_email_from_csv(csv_line):
    """SAFE: Validates column count with length guard."""
    fields = csv_line.split(',')
    if len(fields) >= 3:
        return fields[2].strip()  # SAFE: len(fields) >= 3 guards fields[2]
    return None
$ a3 scan examples_safe.py --interprocedural

============================================================
INTERPROCEDURAL ANALYSIS RESULTS
(High-confidence TPs only, threshold=0.7)
============================================================
Total bugs found: 0

All five guarded functions are reported clean (exit code 0). The guards are recognised by A3's guard detection; this example does not show which component (AST guard analysis, bytecode guard detection or Z3) did so.

To triage remaining findings with an LLM:

a3 scan examples_safe.py --interprocedural --output-sarif results.sarif
a3 triage --sarif results.sarif --provider github --output-sarif filtered.sarif --agentic

Scanning a project

# Directory scan (seven-step pipeline)
a3 scan . --output-sarif results.sarif

# Agentic triage of the remaining findings
a3 triage --sarif results.sarif --output-sarif triaged.sarif --provider github --agentic --verbose

# Baseline ratchet check
a3 baseline diff --sarif triaged.sarif --auto-issue

Architecture

a3_python/
├── cli.py         # CLI with subcommands (scan, init, triage, baseline)
├── analyzer.py    # Core analysis engine
├── frontend/      # Python loading, bytecode compilation
├── cfg/           # Control-flow graph + call graph construction
├── semantics/     # Symbolic bytecode execution, crash summaries
├── z3model/       # Z3 value/heap modeling
├── unsafe/        # Bug type predicates (84 types in registry.py)
├── contracts/     # External call modeling, taint sources/sinks
├── dse/           # Concolic execution (Z3-backed)
├── barriers/      # Barrier patterns (8, mostly heuristic) and kitchensink re-implementations
└── ci/            # CI integration
    ├── sarif.py           # SARIF 2.1.0 serializer
    ├── baseline.py        # Ratchet / baseline management
    ├── triage.py          # One-shot LLM classification
    ├── agentic_triage.py  # Multi-turn agentic triage with tool-use
    ├── config.py          # .a3.yml loader
    ├── init_cmd.py        # `a3 init` bootstrapper
    └── templates/         # GitHub Actions workflow YAMLs

Development

git clone https://github.com/thehalleyyoung/a3-python.git
cd a3-python
pip install -e ".[dev,ci]"
pytest

The full suite has 2138 tests and takes tens of minutes. About 82 tests currently fail (see Evaluation status).

License

The repository does not currently include a licence file, and the PyPI package declares no licence.

About

No description, website, or topics provided.

Resources

Stars

7 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages