Problem: docs/positioning.md claimed four confidence tiers (there are
five, including Latent) and defined Proved as any Z3 SAT, which
contradicts soundness.md's exact-model requirement. It claimed "fold
scans a 100k-LOC codebase in minutes" with no committed benchmark (the
audit measured 2 files in 5.9 s at 407 MB RSS). It described CBMC as
asking Z3/MathSAT (its default back end is SAT) and as scaling poorly
past a few thousand lines, without support. It claimed a scan-to-fuzz
loop "no other open-source analyzer covers" and "no commercial vendor
ships" (directed and hybrid fuzzers such as AFLGo and SAVIOR cover
related ground, and prior-art.md cites that line of work). It said most
analyzers "stop at SAT", ignoring the Clang Static Analyzer's Z3
refutation.
Fix: five tiers with Latent defined; Proved requires an exact bounded
model; the CBMC comparison describes the method and fold's real scope
(per-sink, mostly intraprocedural, unroll 5) instead of speed; the
uniqueness claims now describe the loop without exclusivity; CSA's Z3
refutation is acknowledged. The README is left for a separate docs pass.
Add a "What fold reliably catches vs what's noise" section informed
by recent real-codebase usage. Two concrete claims now in the doc:
1. On tight, well-typed codebases most security findings are FPs
because the bounded symbolic model can't carry domain invariants
the codebase enforces elsewhere.
2. The reliable signal is the CLI-input → arithmetic-hole pattern.
Where untrusted input flows into integer math or pointer
arithmetic without a bounds check, fold catches it; the fix is
usually a one-line defensive check at the boundary.
Plus a four-step triage heuristic users can apply when reading a
report: filter by input reachability; trust ConcreteWitness;
triage Proved against reachability; heavily filter Heuristic.
Recommends `--detectors security` (which includes taint-track) as
the mechanical version of the input-reachability check.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Two long-pending docs:
- docs/positioning.md: sales-free comparison of fold against
clang-tidy, commercial SAST, CodeQL/Joern, CBMC/ESBMC, and
KLEE/SymCC/S2E. Tells engineers when to choose fold and
when not to. Closes task #88.
- docs/m31-phase3-concolic.md: scoping for the closed-loop
symbolic execution piece of M31 Phase 3. Compares
vendoring SymCC's LLVM pass (Option A) vs the LibAFL +
symcc-rt bridge (Option B). Recommends Option B for
maintenance leverage; stages P3.1 (plumbing), P3.2
(LibAFL harness), P3.3 (promotion path).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
