How TrueVectors works

Per file, end to end. The pipeline is intentionally short — every stage has a single responsibility, and every finding carries an audit trail back to the stage that produced it.

Why this is a neuro-symbolic architecture

The loop below is neuro-symbolic in the precise sense: a neural proposer (the LLM) is wrapped by a symbolic layer that both grounds it and can override it. The symbolic layer parses code into an Abstract Syntax Tree — a discrete, logic-based symbol structure — and applies explicit rules over it. The facts it proves are injected into the prompt as ground truth, and a deterministic adjudicator merges and overrides the model's output.

The symbolic layer is implemented at two depths. The default depth is rule-based AST analysis (Python ast, plus tree-sitter for JS/TS). The deeper, opt-in depth is a falsification engine: property-based testing (Hypothesis) and symbolic execution (CrossHair driving Z3), which can either return a concrete counterexample or prove an invariant over a whole input domain. The one boundary still on the roadmap is dataflow/taint analysis (Semgrep/CodeQL). The term describes the architecture; the depth is stated plainly.

The pipeline

Step 1

Detect

Deterministic detectors scan only the lines you changed and produce proven facts — no guessing.

Step 2

Ground

Those facts are handed to the model as evidence, so the review reasons from what is verifiably true, not from a hunch.

Step 3

Audit

A constrained review checks the change against a fixed catalog of failure modes — the same diff yields the same vocabulary every time.

Step 4

Verify & fuse

Every finding is re-checked deterministically and stamped with its evidence tier — proven, corroborated, or model opinion.

Step 5

Persist & learn

Results and reviewer feedback are saved, so precision improves with every run.

Optional · for a claim that reduces to a rule over inputs, an opt-in sandbox executes the code — either breaking the claim with a concrete counterexample or proving it holds across the whole input domain.

Closed taxonomy, not free-form labels

The differentiator is not a prompt or instruction file — it is a closed failure-mode taxonomy defined in code plus the deterministic verification layer. Free-form LLM audits drift: a diff that yields "swallowed exception" on one run might yield "silent error" on the next, and "missing error handling" on a third. The Auditor forbids that:

• The taxonomy is the source of truth — a code-defined label space, not prose the model is told to follow. mode_id is enumerated, not free text, and unknown ids are rejected at parse time.
• .truevectors/audit_intent.md is per-workspace calibration (severity thresholds, what to flag) — configuration, not a model-steering script.
• The LLM proposes findings at temperature 0 with a pinned model; a post-parse normaliser maps synonyms and near-misses back onto the canonical id before the finding is persisted.

The downstream effect is that two runs of the same diff produce the same vocabulary, even if the prose differs — so precision by mode is trackable over time. The verdict that matters, though, is the one the deterministic layer proves or disproves.

Diff-scoping (why noise is low)

Detectors run only against the changed line numbers in the diff. The swallowed-exception detector won't flag legacy except: pass that you didn't touch in this PR; it will only flag a swallowed exception inside a hunk you actually modified. The same scope is applied to LLM findings during adjudication, so the two layers compare apples to apples.

Evidence-tier fusion (the moat)

After the LLM returns its findings, the adjudicator does the join:

LLM raised it?	Detector confirmed it?	Resulting evidence tag
Yes	Yes	corroborated
Yes	No (or not checkable)	llm
No	Yes	deterministic
Yes	Detector refutes it (sound, all-instances check)	refuted
—	Counterexample found / property proved (opt-in sandbox)	counterexample / property_checked

This is where the moat compounds. Frontier LLMs commoditize the llm-only column for everyone. The deterministic and corroborated columns — and the accumulating corpus of verified results plus reviewer feedback — are what stays differentiated.

The falsification engine (opt-in per repo)

For claims that can be reduced to a property over inputs, the Auditor goes past static analysis and executes:

• The LLM compiles an intent/claim into a typed property specification.
• Hypothesis samples inputs to hunt for a violating case; CrossHair drives Z3 to either return a concrete counterexample or prove the property over the whole declared input domain (an exhaustion is a sound proof, not a sample). A pandera + metamorphic data-contract harness checks a transform's output schema and relations the same way.
• Everything runs in a resource-capped sandbox (CPU/memory/wall-clock limits, network blocked). It is gated two keys: the global TV_ENABLE_COUNTEREXAMPLE switch and a committed .truevectors/counterexample.toml allowlist naming the exact callables allowed to run. Nothing executes by surprise.

Claims verification (cheapest sufficient verifier)

Agents don't just produce code — they make claims about it ("added retries with backoff", "all tests pass"). The Auditor parses agent-session transcripts into typed claim records and routes each one to the cheapest verifier that can actually settle it:

1. a deterministic detector, if the claim maps to one;
2. a counterexample target, if it reduces to a property over inputs;
3. an artifact invariant, if it is about a pipeline's realized output;
4. otherwise it stays llm and is surfaced as an unverified_claim.

A claim the evidence disproves becomes a deterministically refutedclaim_delivery_mismatch — the agent said one thing and shipped another. A claim nothing can check is reported as exactly that: unverified, never silently accepted.

Triage: the proved tier comes first

Every surface answers the same question first — what is actually proved? The proved tier (deterministic, corroborated, refuted, counterexample, property_checked) is the default view in the CLI JSON summary, the dashboard findings list, and the PR comment. The llm tier is one flag (--all), one toggle, or one expandable section away, and its count is always visible — shown honestly, just never mixed in by default. In PRs, inline review comments are posted only for proved-tier findings, so comment volume is bounded by what the math established.

Generic outcome-invariant auditor

Beyond auditing source, the Auditor can audit a pipeline's realized output against declared invariants — "propose-and-dispose":

• A deterministic Tier-0 checker reads an output artifact (CSV / JSON / Parquet / DataFrame) and evaluates each declared invariant, emitting violated / satisfied / unverified — an unchecked invariant is never green-stamped.
• An optional, gated LLM step reads config/code and proposes candidate invariants in a small DSL; it never decides whether they hold. It is off by default and fails loudly (never fabricates) when its key is missing.

The rules are domain-agnostic — five universal contracts over any tabular output, whatever produced it:

Kind	The law it proves
bound	An aggregate stays inside a threshold (a budget cap, a margin floor).
conservation	Parts sum to the whole (no double-counting, no silent drops).
cardinality	Keys are unique, counts match, references resolve (no duplicated rows, no omitted population).
monotonicity	An ordered relationship holds (more discount never means a higher price).
distribution	Values stay in range, no nulls, probabilities sum to one.

A violation names the offending rows and carries a deterministic evidence tag — the same evidence standard as the static detectors, applied to the outcome.

Behavioural auditing of agent runs (same checker, no LLM)

An agent run is a stream of events, not a table — so an adapter flattens the recorded trajectory into one, derives 0/1 policy columns, and the identical deterministic checker proves the run's declared policies. One front door, three input shapes:

tv invariants --workspace .                    # a pipeline's output artifact
tv invariants --session run.json               # one recorded agent session
                                               # (ATIF auto-detected)
tv invariants --agentlens-run runs/x           # a whole agent-lens / Harbor
                                               # run dir, policy from its
                                               # own config.yaml

The policy is declared data lifted from the run's own config — an allow-list of tools becomes a distribution law (every call flagged that is off the list, named in the receipt); a max_budget_usd becomes a bound over the realized cost. The adapter runs no agent and decides nothing; a run that declares no checkable policy returns "nothing to check" with a reason, never a fabricated pass. No LLM and no API key anywhere on this path.

What an audit requires (and what it won't pretend to do)

The Auditor proves declared rules against a real artifact. Pointing it at a bare folder or repo is the start — a verdict is earned only when the inputs a lens needs are actually present. The deterministic triage step detects which (if any) apply and tells you what's missing; it never invents a passing grade.

Lens	What must be present	What it proves
Data outcome	a realized output file (CSV / JSON / Parquet) and declared invariants in .truevectors/invariants.yaml (with artifact.yaml naming the file)	the output obeys its declared totals, counts, caps, and ranges
Agent behavior	a recorded session / trajectory (ATIF or an events JSON) that declares a policy — a tool allow-list and/or a per-run budget cap	the run stayed inside its declared tool and spend policy
Source code	source files to scan (ideally including AI-written tests); an LLM key for the proposer	risks, gamed tests, and unsupported claims in the changed code

Two honesty rules follow from this:

• No declared rule, no verdict. A repo with no invariants, no recorded session, and nothing changed to scan is reported as nothing checkable here — with a note on what to add — not waved through as "passed".
• Reproducible from a cited artifact. A published audit earns its row only from a real, public artifact anyone can re-check with no API key. Targets without one stay queued — no verdict shown until that artifact exists.

Read more

• Overview — the platform and two products.
• TrueVectors Auditor — prove what an agent did.
• TrueVectors Hub — durable system of record.
• Delivery and evaluation — authorized CI-first delivery and access.
• Architecture — the tiers a request flows through.