How We Use a Second AI Agent to Review Investment Research

Why are formal proof systems becoming a product category?

Formal verification means stating a claim in precise mathematical terms and checking that every step needed to establish it follows from explicit assumptions. Systems such as Lean produce proof objects that a small independent kernel can check. That is a different kind of assurance from a plausible explanation, a confidence score, or a test suite that covers only selected cases.

The current wave extends that machinery beyond theorem proving. Pramaana Labs turns rules from domains such as tax, law, and clinical safety into machine-checkable logic; Harmonic's Aristotle formalizes and proves problems in Lean; and Imandra applies automated formal verification to trading venues and financial algorithms. The products differ, but they share a premise: in high-stakes work, an AI output should be checked against an explicit specification and leave an artifact that another system can inspect.

Itoflow applies that premise to the workflow around investment research, with an important limit. Our DSL is not a general-purpose theorem prover, and an evidence obligation is not a mathematical proof that an investment conclusion is true. The contract and its deterministic validators can establish exact facts about structure, constraints, provenance, calculations, and required evidence. They cannot establish that the contract captured the user's intent or that the research method and evidence were adequate.

Where does formal proof stop?

Consider a user who asks an agent to build a market-neutral portfolio while keeping every position below a client-approved limit, but never supplies the limit. In one of our tests, the agent inferred 12.5% from the current portfolio and continued. The client later supplied the real number: 15%. The guess sounded conservative, but it changed which portfolios were feasible and which one the agent preferred.

In this article, Itoflow means the complete quantitative-research system, not a single model. The system combines a Research Agent, a Guardian Agent, their instructions, tools, data and permissions, a written research contract, and deterministic checks that govern progress. We call that surrounding system a research harness.

Before research begins, the Research Agent writes a research contract: a structured plan that records what it believes the user wants, the constraints it will respect, the data and methods it expects to use, and the evidence it promises to produce. We express the contract in a domain-specific language (DSL), a structured format designed for this research workflow. Deterministic checks validate the exact parts of that plan before work can proceed, so a constraint stated at the start of a conversation cannot quietly disappear later.

That contract is effective where one answer can be verified: plan structure, data references, arithmetic, portfolio feasibility, and safety constraints. The 12.5% guess exposed the boundary. Software could confirm that a limit existed, but not that the user had chosen it. Nor could it reliably decide whether twenty nearby regressions represented a serious method search or whether new evidence should change the plan.

We initially tried to encode more of those judgments as formal rules. The result was longer instructions, more contract fields, and more repair loops. In a 14-day production sample, 685 failed plan checks later passed. The median repair took 14.9 seconds, and 96.6% of intervening tool calls edited or revalidated the plan instead of gathering research. Some repairs corrected real defects; many translated existing prose into the validator's required shape.

How does the two-agent review work?

Our solution is to use two agents: the Research Agent does the work, and the Guardian Agent reviews it. Itoflow launches the review automatically and controls its instructions, evidence, and scope, so the Research Agent cannot select the version of its work that receives scrutiny.

Why the Verifier Agent fell short

Before the Guardian Agent, Itoflow had an independent Verifier Agent. It could inspect files, recompute results and reject weak work. It caught real defects, and we retained the strongest parts of its review instructions. The problem was where it sat in the process.

1. The Research Agent launched it. The agent being reviewed decided when review happened.
2. The Research Agent framed the assignment. An agent that had already narrowed the problem could ask the verifier to validate that narrower interpretation.
3. It arrived late. By the time review began, the plan, code and analysis already reflected the Research Agent's assumptions.

The Verifier Agent also became entangled with contract bookkeeping. The Research Agent packaged claims into machine-shaped evidence records so the workflow could close, improving the record more often than the research. The deeper problem remained: the Research Agent managed the reviewer it was supposed to satisfy.

What we borrowed from Codex Auto-review

OpenAI's Codex can automatically pause before a risky computer action and ask a separate model to review it. This feature is called Auto-review. The software—not the coding agent—chooses when review happens and what evidence the reviewer sees. OpenAI's alignment write-up and public Guardian policy template separate the task-completion role from the review role and ask the reviewer to interpret the user's intent, not merely match an exact command string.

We adapted that pattern in three ways for quantitative research.

• Review commitments, not shell commands. Itoflow reviews the Research Agent's plan and its proposed final answer.
• Give the Guardian Agent the underlying evidence. It can inspect the plan, code, data, calculations, results, and sources through read-only tools.
• Keep the same Guardian Agent across repairs. It remembers earlier concerns and can distinguish a correction from an argument for accepting the old work.

When does the Guardian Agent review the work?

The Guardian Agent reviews the work twice: before research begins and before the final answer is released. Itoflow launches both reviews automatically, so the Research Agent cannot skip them or narrow their scope.

The Guardian Agent either accepts the work or asks for a specific revision. A revision request blocks that stage. If the Guardian Agent itself fails repeatedly, Itoflow records the failed review and lets research continue rather than trapping the user in a loop; deterministic safety and portfolio constraints still apply.

The Guardian Agent has read-only workspace access and approved research tools. It cannot edit files, trade, ask the user, or launch more agents. Plan review receives the request, the Research Agent's visible work, and the complete plan. Answer review adds the draft answer and supporting code, data, calculations, and sources, so the Guardian Agent can judge the research as a whole rather than merely check whether it followed the original plan.

Why the Chat Agent and Strategy Agent need different review

The Research Agent operates in two settings in this article. The Chat Agent works interactively and can ask the user to resolve an ambiguity; the Strategy Agent operates under a standing investment mandate and must often decide without waiting for a reply. Applying one policy to both would make the Chat Agent too presumptuous or the Strategy Agent too indecisive.

For the Chat Agent, the Guardian Agent favors asking when a missing decision changes feasibility, the objective, or the meaning of the answer. It asks the Chat Agent to pose the smallest useful question, not follow a fixed questionnaire.

The Strategy Agent is judged against its mandate and previous decisions. When the mandate allows discretion, it can make a reasonable choice and continue. When a missing decision would exceed that authority, it must take a narrower action or make no change. The evidentiary standard stays consistent; the decision policy changes with the authority granted to the agent.

What changed in the research traces?

We judged the change primarily from traces: what the Guardian Agent challenged, how the Research Agent repaired the work, and whether the repair improved the research. Scores provide a second check.

An invented client constraint

In a market-neutral allocation task, the user required every position to remain under a client-approved concentration limit but did not disclose the number. The Research Agent inferred 12.5% from the current portfolio. The plan passed every exact check. The Guardian Agent rejected the unsupported assumption.

The simulated client answered 15%. The Guardian Agent then caught a materially underspecified estimator, incomplete factor-risk accounting, and a historical validation claim that used descriptors not shown to exist at the time. On the benchmark's 0-to-1 scale, the reviewed run scored 0.915; the run without review kept the 12.5% guess and scored 0.552.

Survivorship bias inside historical validation

A historical test must rebuild its eligible investment universe using only information available at each point in the past. In a drawdown-aware allocation task, the Research Agent selected assets using information from outside each test period. Future availability therefore influenced which assets survived into the test, introducing survivorship and look-ahead bias. The Guardian Agent required the Research Agent to repeat selection and optimization independently inside each period.

The wrong optimization problem

In a portfolio-transition task, the Research Agent said it could reuse an existing regression function and optimizer. Inspection showed that the regression function did not exist. The optimizer also solved a different problem: it minimized distance from target weights using cash, while the user had asked to maximize expected return relative to a benchmark after asset-specific costs and portfolio limits. The repair removed the nonexistent function, solved the requested objective directly, and recomputed every constraint.

Across the seven tasks, the mean rose from 0.568 without review to 0.693 with review: an absolute gain of 0.125 points, or 12.5 percentage points on the 0-to-1 scale. Medians were 0.552 and 0.783, respectively. The traces show what changed: unsupported user constraints became questions, historical tests stopped using future information, nonexistent library functions were removed, and optimizers were redirected to the user's stated economic objective.

What did this let us simplify?

The Guardian Agent let us remove contract fields that consumed attention without producing better research. We introduced the review first, then removed one requirement at a time and reran tasks that depended on it.

• Custom quantitative code no longer needs a large structured justification. The Guardian Agent checks whether the Research Agent searched the existing library and whether new code is proportionate.
• Possible approaches no longer need to fit a compulsory formal graph. The Guardian Agent checks whether the Research Agent considered meaningfully different methods before committing.
• Qualitative claims no longer need separate machine-shaped evidence records solely to close the workflow. Deterministic checks still retain exact identities, feasibility, and quantitative comparisons.

In one cross-asset rerun, required evidence records fell from twenty to two while the Guardian Agent still caught a horizon mismatch, weak validation, and a heuristic described as an optimizer. The aim is not fewer controls. It is to keep exact rules in software and reserve contextual judgment for independent review.

Where did the Guardian Agent make the result worse?

The relative-value task is the counterexample. The Guardian Agent surfaced missing client constraints, required sensitivity tests across recovery, impairment, volatility paths and dependence, and challenged an unsupported claim that the search was exhaustive. The Research Agent still chose a 100% cash solution. It was feasible but economically weak; the run without review chose a four-name equity sleeve and scored 0.726 points higher on the 0-to-1 scale.

Our claim is therefore limited. The Guardian Agent improved six of seven matched scores and corrected identifiable research failures, but it did not guarantee a better investment conclusion. An independent reviewer can reduce a class of failures; it cannot make a stochastic system deterministic.

What could this design review next?

We started with the plan and the final answer because they mark two commitments: “this is the work I intend to do” and “this work is complete.” The same pattern may help at other high-risk moments: after substantial quantitative code, before a portfolio transition reaches the user, or when a long-running Strategy Agent appears to depart from its mandate. Routine actions do not justify the cost or delay of independent review.

The division of responsibility is now clearer. The research contract records stable commitments; deterministic checks enforce what software can verify exactly; the Guardian Agent reviews whether the plan fits the request and whether the evidence supports the answer. Our earlier article on formal research contracts explains the first layer. We will move more judgment to independent review only when traces show that it works better.

How did we test and source this?

• Lean, “Introduction” — the distinction between a machine-checked proof and an unverified reasoning trace.
• Pramaana Labs — a current verification system that translates rules from high-stakes domains into machine-checkable logic and proof artifacts.
• Harmonic, “Aristotle” — an AI system that formalizes English problems and constructs proofs in Lean.
• Imandra Markets — automated formal verification applied to trading venues and financial algorithms.
• OpenAI, “Auto-review” — the Codex reviewer design that inspired our automatic review pattern.
• OpenAI Alignment, “Auto-review: A safety layer for agentic systems” — the case for separating the task-completion role from the review role, and the limits of stochastic review.
• OpenAI Codex, public Guardian policy template — review of whether a proposed action matches the user's intent and the available evidence.
• Itoflow, “How Itoflow Turns Investment Intent into a Machine-Checked Contract” — the written research-plan design that the Guardian Agent now complements.
• Itoflow, “Async Critique Agents” — our earlier work on independent, temporally separated agent review.
• Itoflow, “What Our Quant-Research Agent Actually Does” — the research process whose quality the Guardian is designed to protect.

What should you take away?