# Symbolic Execution + Fuzzing Tools Landscape

> Architecture expansion research for fold. Generated 2026-05-27.

Maps the symbolic execution, model checking, abstract interpretation, and
fuzzing tools relevant to fold's multi-language expansion across C++, Rust,
Swift, and binary targets. For each tool: approach, IR level, language
support, false-positive profile, maturity, and concrete integration pattern
for fold.

## Table of contents

1. [Taxonomy](#taxonomy)
2. [Symbolic execution engines](#symbolic-execution-engines)
3. [Model checkers & verifiers](#model-checkers--verifiers)
4. [Abstract interpreters](#abstract-interpreters)
5. [Fuzzing engines](#fuzzing-engines)
6. [Binary analysis frameworks](#binary-analysis-frameworks)
7. [Integration pattern catalog](#integration-pattern-catalog)
8. [Architecture expansion recommendations](#architecture-expansion-recommendations)

---

## Taxonomy

| Approach | What it does | fold already does it? |
|----------|-------------|----------------------|
| **Symbolic execution** | Tracks symbolic values along paths, queries SMT at branches | Yes — Z3 BV-64 encoder, per-sink SAT queries |
| **Concrete fuzzing** | Mutates byte inputs, runs target natively, reports crashes | Yes — libFuzzer/AFL++ via `fold fuzz-run` |
| **Concolic execution** | Concrete execution + parallel symbolic shadow store, negate branches | Planned — M31 Phase 3 (LibAFL+symcc-rt) |
| **Model checking** | Encode full program + property as SMT formula; prove or find counterexamples | No — fold is per-function, not whole-program BMC |
| **Abstract interpretation** | Fixed-point over abstract domains (intervals, octagons, polyhedra) | Partial — interval pre-pass, no AI fixpoint engine |
| **Binary analysis** | Disassemble + lift to IR for pattern/heuristic detection | Yes — R2Backend for strings/symbols/calls/xrefs |

---

## Symbolic execution engines

### KLEE

| Dimension | Detail |
|-----------|--------|
| **Approach** | Full symbolic execution |
| **IR level** | LLVM IR (bitcode) |
| **Languages** | C, C++ (any language that compiles to LLVM IR) |
| **Solver** | KLEE's own constraint solver + Z3 backend |
| **FP rate** | Low — explores actual paths. Missing code produces false negatives, not false positives. |
| **Maturity** | Very high. 15+ years. Active maintenance (KLEE 3.1, 2024). SV-COMP participant. |
| **License** | GPL-2.0 (with LLVM exception for the ucKLEE variant) |
| **Key capability** | Bottom-up path exploration from a harness entry point. Produces high-quality test inputs for every covered path. Symbolic filesystem, POSIX environment models. |

**How it works:**

KLEE interprets LLVM bitcode symbolically. Memory is a flat symbolic array with
byte-level granularity. At branches, KLEE forks the state and adds the branch
condition to each path's constraint set. When a path terminates, KLEE concretizes
the symbolic input to produce a test case. KLEE's constraint solver layer
(KQuery → STP/Z3) optimizes for the pattern-matching checks common in path
exploration.

**Integration pattern for fold:**

The license mismatch (GPL-2.0 vs fold's planned GPL-3.0) is noted in
`docs/internal/m31-phase3-concolic.md` and is the primary reason fold deferred
KLEE adoption. Architectural mismatch too: KLEE owns the process (its own
interpreter loop), while fold orchestrates child processes via `posix_spawn`.

If fold's license posture changes, a useful integration would be:

```
fold scan → findings with Z3 witnesses
    ↓
fold fuzz-prep → emit KLEE harness (.c file calling target function)
    ↓
klee --libc=uclibc --posix-runtime harness.bc
    ↓
fold fuzz-ingest ← KLEE test cases → ConcreteWitness promotion
```

KLEE's strength — exhaustive bounded path coverage from an entry point —
complements fold's per-sink SAT approach. KLEE could confirm that a
fold-flagged sink is actually reachable from a program entry point, closing
fold's "SAT under our encoding but maybe unreachable" gap.

**Relevance to fold:** Medium. The license barrier is real. The architectural
mismatch (KLEE as interpreter, fold as orchestrator) means integration would be
a side-by-side pipeline, not an embedded pass. Worth reconsidering if fold
adds a verification tier (e.g., CBMC-style whole-module bounded verification)
where KLEE's path coverage complements fold's bottom-up scan.

---

### Haybale

| Dimension | Detail |
|-----------|--------|
| **Approach** | Symbolic execution |
| **IR level** | LLVM IR (via `llvm-ir` crate) |
| **Languages** | Any language with LLVM bitcode (practically: C, C++, Rust via `--emit=llvm-ir`) |
| **Solver** | Boolector (default), Z3 (optional backend) |
| **FP rate** | Very low — full path exploration, well-defined memory model. |
| **Maturity** | Research-grade. Last major release 2021. Trail of Bits project, not actively maintained. |
| **License** | MIT / Apache-2.0 |
| **Key capability** | Pure Rust symbolic execution for LLVM IR. Clean API for programmatic path exploration, hookable function models, and SMT query callback. |

**How it works:**

Haybale is a Rust library that loads LLVM bitcode and provides a symbolic
execution engine. It uses Boolector (a bitvector SMT solver, also from the
Boolector/STP/KLEE lineage) for constraint solving. The API is designed for
embedding: you write a Rust program that uses Haybale to explore specific
functions. Haybale handles memory as a flat byte-addressable array, models
LLVM instructions symbolically, and provides hooks for modeling library
functions.

**Integration pattern for fold:**

Haybale's Rust-native design and permissive license make it the most
architecturally natural symbolic execution backend for fold's Rust expansion.
Integration shape:

```
fold scan --mode rust <crate>
    ↓
fold-rust extract → NDJSON (IR + findings)
    ↓
fold-concolic (Rust crate) → Haybale Project::from_bc_path()
    ↓                            ↓
target_fn.bc ← rustc --emit=llvm-ir    symbolically_execute_fn()
    ↓
path constraints → Boolector/Z3 → new seeds → libFuzzer corpus
```

Haybale could serve as fold's Rust-native answer to the C++ side's
symcc-rt + LibAFL concolic bridge. Because Haybale is a library (not a
process), it avoids the subprocess IPC overhead. It also avoids the
license problem KLEE has.

**Relevance to fold:** High for the Rust frontend specifically. Haybale
provides symbolic execution for LLVM IR from a Rust host — exactly what
a `fold-concolic` Rust crate would need to do path exploration on
Rust-generated bitcode. The lack of active maintenance is a risk, but
for fold's bounded-model use case (not full-system symbolic execution),
the existing codebase may be sufficient. Evaluate in a spike: can Haybale
load and symbolically execute the bitcode from a `fold-rust extract`
target in under 100 lines of integration code?

---

## Model checkers & verifiers

### Kani

| Dimension | Detail |
|-----------|--------|
| **Approach** | Bounded model checking (CBMC-based) |
| **IR level** | Rust MIR → GOTO intermediate representation → SMT |
| **Languages** | Rust |
| **Solver** | CBMC's built-in SMT pipeline (Z3, MathSAT, CVC5 backends) |
| **FP rate** | Very low (sound for the bound chosen). Properties are proved, not guessed. |
| **Maturity** | High. AWS-backed, active development (2024 releases). Growing adoption in safety-critical Rust. |
| **License** | MIT / Apache-2.0 |
| **Key capability** | Verify Rust programs against user-written `#[kani::proof]` harnesses. Prove absence of panics, overflows, and user-specified assertions within a bounded unrolling depth. |

**How it works:**

Kani compiles Rust MIR into CBMC's GOTO intermediate representation, then
runs CBMC's bounded model checker on the result. Users write proof harnesses
annotated with `#[kani::proof]` and `kani::assume()`/`kani::assert()`.
Kani then verifies (proves or finds counterexamples for) those harnesses.
The result is either a proof (no property violation within the unrolling
bound) or a concrete counterexample trace.

Kani is verification, not scanning: it proves properties of specific harnesses,
not "find all bugs in this codebase."

**Integration pattern for fold:**

Kani occupies a different niche than fold (verification vs scanning), but
they compose well:

```
fold scan --detectors security → findings for Rust unsafe blocks
    ↓
For each high-confidence finding:
    ↓
fold emit-kani-proof → generate #[kani::proof] harness for the flagged function
    ↓
cargo kani --harness <name>
    ↓
    ├─ VERIFIED → fold finding downgraded to "Kani-proved unreachable"
    └─ FAILED  → Concrete counterexample → fold promotes to ConcreteWitness
```

Fold adds bottom-up scanning ("find plausible bugs") and Kani adds
top-down verification ("prove this specific property"). Fold's per-sink
SAT queries find candidates; Kani's whole-program BMC confirms or refutes
them with higher confidence.

The integration is straightforward because both tools work with Rust's
MIR (fold-rust via `rustc_driver` → HIR; Kani via `kani-compiler` →
GOTO). A `fold emit-kani-proof` command that generates Kani harnesses
from fold's Rust findings would be a ~200-line addition to
`tools/fold-rust/`.

**Relevance to fold:** High for the Rust expansion's confidence pipeline.
Kani provides the verification tier fold's Rust side currently lacks
(all Rust findings are `Heuristic` today). A fold→Kani bridge would
promote some findings to "verified unreachable" and others to
"concrete counterexample" — the same closed loop the C++ side achieves
with Z3→libFuzzer→ConcreteWitness.

---

### Rudra

| Dimension | Detail |
|-----------|--------|
| **Approach** | Static analysis (pattern-matching + dataflow) |
| **IR level** | Rust MIR (via `rustc` plugin, now deprecated) and HIR |
| **Languages** | Rust |
| **FP rate** | Low for unsafe-API patterns; moderate on send/sync inference. |
| **Maturity** | Research project (Georgia Tech, 2020-2021). Deprecated as of 2023 — the `rustc` plugin API it used is removed. |
| **License** | MIT |
| **Key capability** | Found 76 CVEs and 112 RustSec advisories in the Rust ecosystem. Pioneered systematic unsafe-block auditing at ecosystem scale. |

**How it works:**

Rudra ran as a `rustc` plugin (before the plugin API was removed) and analyzed
Rust MIR for three classes of bugs: (1) unsafe API misuse (e.g., `Vec::from_raw_parts`
with untrusted lengths), (2) incorrect `Send`/`Sync` implementations leaking
interior mutability, and (3) panic safety violations in unsafe code. The analysis
was primarily pattern-matching over MIR combined with limited dataflow.

**Why Rudra is listed even though deprecated:**

Rudra's detector catalog — the specific patterns it flagged — is a design
blueprint for fold-rust's security detectors. Rudra proved these patterns
have high yield in real-world Rust code (112 advisories). fold-rust can
re-implement the same patterns as HIR visitors in `tools/fold-rust/src/`.

**Integration pattern for fold:**

Rudra is a source of detector ideas, not a runtime to integrate:

```
Rudra's detector catalog → fold-rust HIR visitors:
    Send/Sync inference ↓
    unsafe API patterns ↓
    panic safety      ↓
    → fold-rust finding_kind: rust-unsafe-api
```

fold-rust already has the `rust-unsafe-api` and `rust-unchecked-index`
finding kinds (`include/fold/report/finding.hpp`). Rudra's specific
patterns (e.g., "`Vec::from_raw_parts` with untrusted `capacity`") should
be added as rules under those kinds. This is a detector-authoring task
within fold-rust, not a tool integration.

**Relevance to fold:** Medium (as a detector catalog). Rudra's 112-advisory
track record makes it the strongest source of real-world Rust unsafe
patterns. fold-rust's `DerefHunter` covers raw-pointer derefs; adding
Rudra's send/sync and unsafe-API patterns would make fold-rust a
genuine Rust SAST rather than a single-detector tool.

---

### MIRAI

| Dimension | Detail |
|-----------|--------|
| **Approach** | Abstract interpretation |
| **IR level** | Rust MIR |
| **Languages** | Rust |
| **FP rate** | Moderate — abstract interpretation over-approximates; many "maybe" results. |
| **Maturity** | Research project (Facebook/Meta, 2019-2023). Not actively maintained as of 2024. |
| **License** | MIT |
| **Key capability** | Taint tracking, integer overflow detection, unreachable code detection. Abstract domain with widening on MIR. |

**How it works:**

MIRAI runs as a `rustc` driver (similar to fold-rust's architecture) and
lifts Rust MIR into an abstract interpreter. It tracks integer ranges
(via intervals + widening) and taint, flagging potential panics,
overflows, and unreachable code. Unlike Kani (which does bounded model
checking), MIRAI does abstract interpretation: it computes a fixpoint
over abstract domains and reports when the abstract state indicates a
possible problem.

**Integration pattern for fold:**

MIRAI's abstract interpreter is conceptually similar to fold's interval
pre-pass (`src/symbolic/` interval analysis), but applied at the MIR
level for Rust. Direct integration is impractical (MIRAI is unmaintained
research code). However, the architectural lesson is valuable:

```
MIRAI-style abstract domain → fold-rust MIR visitor (future)
    Interval domain      → refine Heuristic findings with range constraints
    Taint domain         → feed fold's taint-track detector on Rust
    Layout domain        → prove pointer provenance at compile time
```

fold-rust currently operates at the HIR level (via `rustc_driver` +
`rustc_hir`). To match MIRAI's precision, fold-rust would need a MIR
visitor for the abstract domains. The existing HIR infrastructure
(`DerefHunter`) works for syntactic patterns; MIR adds type resolution
after monomorphization, which is necessary for range analysis.

**Relevance to fold:** Medium (architectural lesson). MIRAI proves that
abstract interpretation on Rust MIR is practical and can find real bugs.
fold-rust should plan a MIR visitor layer for future precision upgrades
(RF-3b already calls this out: "move to MIR + monomorphization context").
MIRAI is the prior art that demonstrates it works.

---

### Miri

| Dimension | Detail |
|-----------|--------|
| **Approach** | MIR interpreter (concrete execution, not symbolic) |
| **IR level** | Rust MIR |
| **Languages** | Rust |
| **FP rate** | Essentially zero — detects actual UB at runtime on concrete inputs. False *negatives* possible (input-dependent). |
| **Maturity** | Very high. Official Rust project, shipped via `rustup +nightly component add miri`. Actively maintained. |
| **License** | MIT / Apache-2.0 |
| **Key capability** | Detects undefined behavior in Rust (including unsafe code) by interpreting MIR with UB checks. Stacked Borrows model for pointer provenance. |

**How it works:**

Miri interprets Rust MIR directly instead of compiling to machine code.
During interpretation, it checks for UB: out-of-bounds accesses, use-after-free,
data races, invalid pointer dereferences, and violations of the Stacked Borrows
aliasing model. Miri is a concrete interpreter — it runs a single execution path
with concrete inputs. It does not do symbolic execution or path exploration.

**Integration pattern for fold:**

Miri is a runtime checker, not a static analyzer, but it's fold's most natural
Rust validation tier — analogous to ASan on the C++ side:

```
fold scan --mode rust → findings (Heuristic confidence)
    ↓
fold fuzz-prep → generate Rust harness with concrete seeds
    ↓
MIRIFLAGS="-Zmiri-disable-isolation" cargo +nightly miri test
    ↓
    ├─ UB detected → fold finding promoted to ConcreteWitness
    └─ Clean run   → finding remains Heuristic (unconfirmed)
```

The integration is simpler than Kani: fold's `fuzz-prep` already generates
C harnesses (for libFuzzer+ASan). A Rust variant would generate `#[test]`
functions with `miri` cfg-gating, and fold's runner would shell out to
`cargo +nightly miri test` instead of compiling + running a libFuzzer binary.

Miri also integrates with cargo-fuzz: `cargo fuzz` targets can run under
`cargo +nightly miri run` for fast UB detection on small inputs before a
full fuzzing campaign. fold's Rust fuzz-prep could emit fuzz targets that
are Miri-compatible from day one.

**Relevance to fold:** Very high for Rust validation. Miri is the Rust
ecosystem's gold standard for UB detection, comparable in authority to
ASan+UBSan for C++. Every fold Rust finding that passes through a Miri
check and produces a UB trace is a `ConcreteWitness` with the same
authority as an ASan crash on the C++ side.

---

## Swift tools

### SWAN (Swift ANalysis)

| Dimension | Detail |
|-----------|--------|
| **Approach** | Static analysis framework |
| **IR level** | Swift SIL (Swift Intermediate Language) |
| **Languages** | Swift |
| **FP rate** | Depends on detector. SWAN is a framework; individual analyses vary. |
| **Maturity** | Research project (University of Bremen, 2018-2023). SWAN 2.0 added SIL support. Not actively maintained. |
| **License** | MIT |
| **Key capability** | Taint analysis framework for Swift. SIL-level analysis with configurable sources/sinks, framework for writing custom detectors. |

**How it works:**

SWAN is a static analysis framework built on top of the Swift compiler.
It operates at the SIL level and provides taint analysis infrastructure:
users define taint sources, propagation rules, sanitizers, and sinks.
SWAN then computes TaintFlows through the program. Initially operated
on the AST; SWAN 2.0 shifted to SIL for better precision.

**Integration pattern for fold:**

SWAN is directly relevant to `tools/fold-swift/` (Task 73 in the current
sprint). The integration pattern:

```
Swift .swift → swiftc -emit-sil → .sil file
    ↓                                   ↓
fold-swift → parses SIL            SWAN → TaintFlows
    ↓                                   ↓
fold-swift detectors:              fold-swift taint detector:
  - unsafe cast patterns     ←     - taint config from SWAN's source/sink catalog
  - force-unwrap detection          - flow paths from SWAN's propagation model
  - raw pointer derefs
    ↓
NDJSON findings → fold RustBackend → SARIF/JSON report
```

SWAN provides two things fold-swift needs:
1. **A proven taint framework for SIL** — the source/sink/sanitizer model
   already works for Swift.
2. **A detector catalog** — SWAN ships with detectors for common Swift
   security patterns (sensitive data leaks, injection, path traversal).

fold-swift can either:
- (A) Shell out to SWAN as a subprocess (SWAN → TaintFlow JSON → fold finding),
  matching fold-rust's subprocess model.
- (B) Re-implement SWAN's taint propagation in fold-swift's own SIL visitor
  (more work, but avoids an external dependency).

Option A is preferred for speed; option B for long-term maintenance. The
immediate path: shell out to SWAN for taint, add fold-swift's own SIL
visitors for pattern-matching detectors (unsafe casts, force-unwrap,
raw pointer access).

**Relevance to fold:** High for the Swift frontend. SWAN is the only
existing open-source taint framework for Swift SIL, and it's MIT-licensed.
It fills the taint-tracking gap fold-swift would otherwise have to build
from scratch.

---

## Fuzzing engines

### AFL++

| Dimension | Detail |
|-----------|--------|
| **Approach** | Coverage-guided greybox fuzzing |
| **IR level** | Source-level instrumentation (compiler pass) OR binary-level (QEMU, Unicorn) |
| **Languages** | C, C++, Rust (via cargo-afl), any binary |
| **Solver** | None — pure mutation-based with coverage feedback |
| **FP rate** | Near-zero — crashes are real. But false negatives (missed bugs) are inherent in fuzzing. |
| **Maturity** | Very high. Primary fuzzing engine in the AFL lineage. Active maintenance (2025 releases). |
| **License** | Apache-2.0 |
| **Key capability** | Industry-standard fuzzer. Custom mutators, persistent mode, binary-only fuzzing, LibAFL framework for custom fuzzing pipelines. |

**How it works:**

AFL++ instruments the target (at compile time or binary level) to track
edge coverage. It maintains a corpus of interesting inputs and repeatedly
mutates them, keeping inputs that discover new coverage edges. Forkserver
mode (or persistent mode) avoids process startup overhead. Binary-only
mode uses QEMU user-mode emulation with coverage instrumentation.

**Integration pattern for fold:**

fold already uses AFL++-adjacent patterns via libFuzzer and is planning
LibAFL adoption for M31 Phase 3. Specific integration points:

```
fold fuzz-run currently: libFuzzer + ASan
    ↓
fold fuzz-run future:   LibAFL + libFuzzer (configurable backend)
    ↓
fold binary-fuzz-prep:  AFL++ QEMU mode for Mach-O/ELF binaries
    ↓
fold binary-fuzz-run:   AFL++ -Q (QEMU mode) or LibAFL binary-only
```

For fold's binary analysis path (`R2Backend`), AFL++ is the primary
fuzzing runtime. fold's `docs/internal/binary-fuzz-corpus.md` already
documents the dlopen harness pattern; AFL++'s QEMU mode would allow
fuzzing binaries without source access — a natural complement to
fold's r2-based binary string/symbol detectors.

**Relevance to fold:** High. AFL++ (via LibAFL) is fold's planned concolic
runtime (M31 Phase 3). AFL++ QEMU mode fills the binary fuzz gap
currently occupied by the unimplemented `fold binary-fuzz-prep` path.
AFL++ custom mutators could consume fold's Z3-derived dictionaries
(already emitted by `src/fuzz/dict_miner.cpp`).

---

### libFuzzer

| Dimension | Detail |
|-----------|--------|
| **Approach** | Coverage-guided in-process fuzzing |
| **IR level** | Source-level (compiled with `-fsanitize=fuzzer`) |
| **Languages** | C, C++ (LLVM toolchain) |
| **Solver** | None — mutation-based |
| **FP rate** | Near-zero for crashes; coverage gaps are false negatives |
| **Maturity** | Very high. Part of LLVM. Stable and well-documented. |
| **License** | Apache-2.0 (LLVM) |
| **Key capability** | In-process, fast, tightly integrated with ASan/UBSan/MSan. Data-flow-guided mutations (`-use_value_profile=1`). |

**How it works:**

libFuzzer is an in-process, coverage-guided fuzzer. The user writes
`LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size)` and links
with `-fsanitize=fuzzer`. libFuzzer takes over `main()`, maintains a
corpus, mutates inputs (with coverage feedback), and reports crashes
to ASan. It's single-process and uses `fork()` only when requested.

**Integration pattern for fold:**

fold's tightest integration is with libFuzzer — it's already shipped
in M31 Phase 1+2 (`src/fuzz/`):

```
fold fuzz-prep → emits:
    ├─ harness.c       (LLVMFuzzerTestOneInput calling target function)
    ├─ seed_corpus/    (Z3-derived witness bytes)
    ├─ dictionaries/   (libFuzzer dict from Z3 model constants)
    └─ param_schema.h  (struct layout for parameter passing)

fold fuzz-run → compiles harness + runs libFuzzer → ingest crashes → ConcreteWitness
```

fold's harness emitter (`src/fuzz/harness_emitter.cpp`) already
generates libFuzzer-compatible harnesses. The fuzz runner
(`src/fuzz/runner.cpp`) shells out to clang for compilation and
orchestrates libFuzzer campaigns.

**Relevance to fold:** Already integrated. libFuzzer is fold's
primary fuzzing backend. The M31 Phase 3 plan may supplement it
with LibAFL for concolic tracing, but libFuzzer remains the
default for simple coverage-guided fuzzing.

---

### cargo-fuzz

| Dimension | Detail |
|-----------|--------|
| **Approach** | Coverage-guided fuzzing (wraps libFuzzer) |
| **IR level** | Rust source → LLVM IR → libFuzzer |
| **Languages** | Rust |
| **Solver** | None |
| **FP rate** | Near-zero for crashes |
| **Maturity** | High. Official Rust fuzzing tool. Maintained by rust-fuzz team. |
| **License** | MIT / Apache-2.0 |
| **Key capability** | `cargo fuzz init` scaffolds a fuzz target; `cargo +nightly fuzz run` builds + runs. Integrates with ASan, `cargo-fuzz` also supports structure-aware fuzzing via `arbitrary`. |

**How it works:**

`cargo fuzz` is a Rust build-system wrapper around libFuzzer. It generates
fuzz targets (Rust source files with `fuzz_target!()` macro), compiles them
with `-fsanitize=fuzzer` via the Rust compiler's LLVM backend, and runs
the resulting binary. It also manages corpora, artifacts, and coverage
reports.

**Integration pattern for fold:**

fold already references cargo-fuzz in `src/cli/fuzz_prep_runner.cpp:462`
(RF-8: "when running in Rust mode, generate cargo-fuzz-style harnesses").
The integration plan:

```
fold scan --mode rust → Rust findings with Z3 witnesses
    ↓
fold fuzz-prep --mode rust → emits:
    ├─ fuzz/fuzz_targets/target_fn.rs   (cargo-fuzz target)
    ├─ fuzz/corpus/target_fn/           (Z3-derived seeds)
    └─ fuzz/dictionaries/target_fn.dict (libFuzzer dict)
    ↓
fold fuzz-run --mode rust → cargo +nightly fuzz run target_fn
    ↓
ingest crashes → ConcreteWitness promotion
```

The key difference from C++ fuzz-prep: Rust harnesses compile via `cargo
fuzz`, not direct `clang++`. The harness generator needs to emit Rust
source (not C), with `arbitrary::Arbitrary` derives for structured input
generation. The runner invokes `cargo +nightly fuzz run` instead of
`clang++ -fsanitize=fuzzer`.

**Relevance to fold:** High for Rust validation. This is the Rust-side
equivalent of fold's existing C++ fuzz-prep→fuzz-run pipeline. The
infrastructure is already planned (RF-8). Implementation requires:
(1) a Rust harness emitter, (2) `cargo fuzz` project scaffolding, and
(3) runner invocation via `cargo` instead of direct `clang++`.

---

## Binary analysis frameworks

### rev.ng

| Dimension | Detail |
|-----------|--------|
| **Approach** | Binary lifting + decompilation + symbolic execution |
| **IR level** | QEMU TCG → LLVM IR (via rev.ng's own lifter) |
| **Languages** | Binary (x86-64, ARM64, MIPS) → lifted LLVM IR |
| **FP rate** | Depends on analysis. Lifting introduces approximation; decompilation is best-effort. |
| **Maturity** | Active development. Commercial offering (rev.ng S.r.l.) with open-source components. LLVM 19 support as of 2025. |
| **License** | GPL-2.0 (open-source core) + proprietary (commercial extensions) |
| **Key capability** | Lift binaries to LLVM IR, then apply LLVM-based analysis (including libFuzzer fuzzing via dlopen harnesses). |

**How it works:**

rev.ng lifts machine code to LLVM IR through a multi-stage pipeline:
(1) disassemble and recover functions, (2) lift to QEMU TCG (Tiny Code
Generator), (3) translate TCG to rev.ng's intermediate representation,
and (4) lower to LLVM IR. The resulting LLVM IR can then be analyzed with
any LLVM-based tool (optimizers, static analyzers, fuzzers). rev.ng also
includes a decompiler that produces C-like output from the lifted IR.

**Integration pattern for fold:**

rev.ng is referenced in `docs/internal/binary-fuzz-corpus.md` for the
dlopen harness pattern. Two integration modes:

**Mode A — Lift-then-fuzz (binary→LLVM IR→libFuzzer):**

```
Mach-O / ELF binary → rev.ng lift → LLVM IR (.bc)
    ↓
fold binary-prep → function list (from exported symbols)
    ↓
emit dlopen harness (C source, calls dlsym → target function)
    ↓
clang++ harness.c lifted_module.bc -fsanitize=fuzzer,address → harness.fuzz
    ↓
libFuzzer + ASan → crash artifacts → fold ConcreteWitness
```

This is a substantial capability upgrade: it allows fold's full
libFuzzer+ASan pipeline to run on binaries without source code.
The lifted LLVM IR preserves function boundaries and basic-block
structure, so libFuzzer's coverage instrumentation works.

**Mode B — Lift-then-analyze (binary→LLVM IR→fold detectors):**

```
Binary → rev.ng lift → LLVM IR
    ↓
rev.ng decompile → C-like output
    ↓
fold scan --compile-db ... → Z3-powered detectors on lifted code
```

This mode is speculative — lifted LLVM IR is not the same as
source-level Clang AST output, and fold's detectors expect
source-level constructs (function declarations, types, CFG
from Clang). However, for simple functions (no inlining,
no optimization artifacts), the lifted→decompiled path could
enable fold's Z3 detectors on binary-only targets.

**Relevance to fold:** Medium. rev.ng's lift → LLVM IR pipeline is
the cleanest path for applying source-level analysis techniques to
binaries. However, the GPL-2.0 license and commercial split create
the same friction as KLEE. fold's binary path today uses r2 for
heuristic extraction — rev.ng would upgrade that to symbolic-quality
analysis, but at significant integration cost.

---

## Integration pattern catalog

Summary of integration patterns relevant to fold's architecture.

### Pattern 1: Subprocess + NDJSON (already shipped)

Used by: fold-rust (today), fold-swift (planned), fold's own fuzz orchestrator.

```
fold binary → posix_spawnp("tool", [args...]) → NDJSON stdout → fold parser → findings/summaries
```

**Where it works:** When the tool is a standalone binary with a stable output format.
**Where it doesn't:** When the tool requires an in-process API (KLEE, Haybale).

### Pattern 2: Cargo/Rust crate dependency (planned)

Used by: fold-concolic (M31 Phase 3 planned), fold-rust.

```
tools/fold-concolic/Cargo.toml:
    [dependencies]
    libafl = "..."
    haybale = "..."  (if chosen for Rust symex)

fold binary → fork+exec(fold-concolic) → stdin/argv → findings
```

**Where it works:** When the tool is a Rust library and fold can add a Rust crate.
**Where it doesn't:** When the tool is C/C++ only (KLEE, SWAN).

### Pattern 3: LLVM pass plugin (not yet adopted)

Used by: symcc-rt (C++ concolic), rev.ng (binary lifting).

```
fold scan --concolic → clang++ -fpass-plugin=fold_concolic.so → instrumented binary
```

**Where it works:** When the tool is an LLVM pass and fold controls the compiler invocation.
**Where it doesn't:** When every LLVM release requires pass rewrites (the symcc lesson).

### Pattern 4: Harness generation + external runner (shipped)

Used by: fold fuzz-prep, fold emit-kani-proof (proposed).

```
fold fuzz-prep → emits harness.{c,rs} + seeds + dict → external runner compiles + runs
```

**Where it works:** When the analysis tool takes a harness/entry point as input.
**Where it doesn't:** When fold needs runtime feedback during analysis (needs Pattern 1 or 2).

### Pattern 5: Detector catalog import (not runtime integration)

Used by: Rudra (patterns → fold-rust detectors), Clippy (lint catalog).

```
External tool's detector catalog → re-implement as fold detector.
```

**Where it works:** When the tool is a research prototype whose detectors are the valuable artifact.
**Where it doesn't:** When the tool's analysis engine is the valuable artifact (KLEE, Kani, Miri).

---

## Architecture expansion recommendations

Based on the landscape analysis, fold's architecture expansion should follow
these priorities:

### Tier 0 — Ship what's already scoped (current sprint)

| Item | Tool | Pattern | Status |
|------|------|---------|--------|
| Rust MIR validation via Miri | Miri | Harness gen + external runner | Scoped as RF-8 in `fuzz_prep_runner.cpp:462` |
| Swift SIL scanning | SWAN | Subprocess + NDJSON | Scoped as Task 73 (tools/fold-swift/) |
| Concolic execution | LibAFL+symcc-rt | Rust crate dependency | Scoped as M31 Phase 3 |

### Tier 1 — High-impact, low-risk additions (next 2-3 sprints)

1. **Rust Kani bridge.** `fold emit-kani-proof` command that generates
   Kani harnesses from fold-rust findings. Kani verifies (proves or
   counterexamples) the flagged functions. ~200 lines of Rust in
   `tools/fold-rust/`, leveraging fold-rust's existing `rustc_driver`
   infrastructure.

2. **Haybale spike for Rust symex.** Evaluate whether Haybale can
   load and symbolically execute LLVM bitcode from fold-rust targets.
   If viable, Haybale could be the Rust-side counterpart to the C++
   side's Z3 encoder — providing `Proved` confidence (not just
   `Heuristic`) for Rust findings without crossing the language
   barrier.

3. **AFL++ QEMU mode for binary fuzz.** Extend `fold binary-fuzz-prep`
   (currently documented in `docs/internal/binary-fuzz-corpus.md` but
   unimplemented) to emit dlopen harnesses and run AFL++ QEMU mode
   against Mach-O binaries. This closes the binary fuzz gap without
   requiring source code or LLVM bitcode.

### Tier 2 — Medium-impact, medium-risk (next 6 months)

4. **Rudra detector catalog import.** Add Rudra's top-10 highest-yield
   patterns (send/sync, unsafe API, panic safety) to fold-rust as HIR
   visitors. Target: fold-rust finds at least 50% of what Rudra found
   (56 advisories out of 112) via HIR pattern matching alone.

5. **MIRAI-style MIR visitor for fold-rust.** Add a MIR visitor layer to
   `tools/fold-rust/` that performs interval analysis and taint tracking
   on monomorphized MIR. This would upgrade fold-rust from "mostly HIR
   pattern matching" to "has path-sensitive analysis" — closing the
   precision gap between fold-rust and fold's C++ encoder.

6. **rev.ng lift-then-fuzz spike.** Evaluate the "lift binary to LLVM IR
   then fuzz with libFuzzer" pipeline on a small Mach-O fixture. If the
   lifted IR is stable enough for coverage-guided fuzzing, this unlocks
   fold's full Z3+libFuzzer pipeline for binary-only targets.

### Tier 3 — Strategic, high-risk (long-term)

7. **KLEE integration.** If fold's license posture changes to accommodate
   GPL-2.0 (or if KLEE adopts GPL-3.0 or a later-compatible exception),
   KLEE would provide exhaustive bounded path coverage from entry points,
   complementing fold's per-sink SAT approach. This is the verification
   tier fold currently lacks for C++.

8. **SWAN taint integration for fold-swift.** Beyond the SIL pattern
   matching covered in Task 73, integrate SWAN's taint analysis framework
   as a subprocess to add `taint-track` findings to the Swift frontend.

### Decision rules by language target

| Language | Scan-time analysis | Validation/confirmation | Concolic/symex |
|----------|-------------------|------------------------|----------------|
| **C++** | Z3 encoder (shipped) | libFuzzer+ASan (shipped) | LibAFL+symcc-rt (planned) |
| **Rust** | HIR visitors (shipped MVP) | Miri + cargo-fuzz (planned) | Haybale spike (Tier 1) |
| **Swift** | SIL visitors (Task 73) | ASan via fuzzing (future) | SWAN taint (Tier 3) |
| **Binary** | r2 heuristics (shipped) | AFL++ QEMU (Tier 1) | rev.ng lift-then-analyze (Tier 2) |

### What NOT to pursue

- **Prusti, Creusot, Verus (Rust deductive verifiers).** These are
  verification tools requiring user-written specifications in separation
  logic or Rust-specific assertion languages. fold's value is bottom-up
  scanning without user annotations. They are complementary, not
  integrable.
- **SymCC pass port (Option A from M31 Phase 3).** The maintenance
  burden of owning an LLVM pass across releases was explicitly rejected
  in `docs/internal/m31-phase3-concolic.md`. LibAFL+symcc-rt (Option B)
  is the chosen path.
- **CodeQL for fold's own detectors.** CodeQL is a CPG query engine,
  not a symbolic execution tool. fold already has superior arithmetic
  reasoning via Z3. CodeQL's strengths (interprocedural dataflow,
  declarative queries) overlap with fold's taint-track detector and
  are not a differentiator.

---

## References

### Tool homepages

| Tool | URL |
|------|-----|
| KLEE | https://klee.github.io/ |
| Kani | https://model-checking.github.io/kani/ |
| Rudra | https://github.com/sslab-gatech/Rudra |
| MIRAI | https://github.com/facebookexperimental/MIRAI |
| Miri | https://github.com/rust-lang/miri |
| Haybale | https://github.com/trailofbits/haybale |
| AFL++ | https://github.com/AFLplusplus/AFLplusplus |
| LibAFL | https://github.com/AFLplusplus/LibAFL |
| libFuzzer | https://llvm.org/docs/LibFuzzer.html |
| cargo-fuzz | https://github.com/rust-fuzz/cargo-fuzz |
| rev.ng | https://rev.ng/ |
| SWAN | https://github.com/S2-group/swan |

### fold internal docs

| Doc | What it covers |
|-----|---------------|
| `docs/internal/binary-fuzz-corpus.md` | Mach-O binary → ABI inference → dlopen harness pattern |
| `docs/internal/swift-sil-z3-corpus.md` | Swift SIL operations, Z3 API reference, detector map |
| `docs/internal/rust-frontend.md` | fold-rust architecture, subprocess wire format, known limits |
| `docs/internal/m31-phase3-concolic.md` | LibAFL+symcc-rt concolic execution plan |
| `docs/internal/library-expansion-matrix.md` | Z3 and Clang feature adoption scorecard |
| `docs/positioning.md` | fold vs peer tools, confidence tiers, when to choose fold |
| `docs/research/prior-art.md` | Key papers grounding fold's design |
| `docs/research/frontier.md` | Optimization and validation tiers (T0-T4 + future) |

### Key papers

| Paper | Relevance to this landscape |
|-------|---------------------------|
| Cadar et al. (2008) *KLEE: Unassisted and Automatic Generation of High-Coverage Tests* | KLEE architecture and design rationale |
| Poeplau & Francillon (2020) *SymQEMU: Compilation-based symbolic execution for binaries* | Binary-level symbolic execution; alternative to rev.ng |
| Fioraldi et al. (2020) *AFL++: Combining Incremental Steps of Fuzzing Research* | AFL++ architecture; LibAFL design |
| Jung et al. (2020) *Stacked Borrows* | Miri's pointer provenance model |
| Astrauskas et al. (2019) *Leveraging Rust Types for Modular Specification and Verification* | Prusti architecture; why deductive verifiers are outside fold's scope |
| Vanhatalo et al. (2021) *Automatic Rust Unsafe Code Analysis* (Rudra) | Rudra's detector design and ecosystem impact |
| Toman & Grossman (2021) *Concrat: Symbolic Execution for Rust* | Rust-specific symbolic execution; relevant to Haybale evaluation |