How Itoflow Turns Investment Intent into a Machine-Checked Contract

Why are formal proof systems becoming a product category?

Formal verification starts by expressing a claim in precise mathematical terms. A prover then constructs a proof, and a small checker verifies that every step follows from the stated definitions, assumptions, and prior results. In systems such as Lean, the result is a proof object that another machine can check independently. That is a stronger artifact than a confidence score, a reasoning trace, or a test suite that samples only some possible cases.

AI is turning that established discipline into a broader product category. Pramaana Labs translates rules from domains such as tax, law, and clinical safety into machine-checkable logic. Harmonic's Aristotle converts English problems into Lean statements and proofs. Imandra applies automated formal verification to trading venues and financial algorithms. Their products differ, but they share one premise: consequential AI outputs should be checked against an explicit specification and should leave an artifact that can be inspected independently.

A proof is only as good as the statement being proved. It can establish that a conclusion follows from specified rules and inputs; it cannot establish that those rules capture what a person meant, that an omitted constraint should not have been present, or that the available evidence describes the world well. This is the specification problem. Language models make it more important because they can translate an underspecified request into a precise but wrong formal statement with unusual fluency.

Itoflow addresses a narrower version of this problem in investment research. It is not a general-purpose theorem prover, and its proof obligations do not make an empirical investment conclusion mathematically true. Its workflow DSL records the commitments a research process must honor; deterministic validators check exact properties of that contract and the evidence attached to it. The remaining question is how to turn an investor's ambiguous request into the right contract in the first place.

Why isn't a capable language model enough?

Tell an investing agent: "build me a short-horizon portfolio that tracks MSCI World, minimize the tracking error, and avoid oil and gas and linked industries." In one sentence you have made four commitments — a benchmark, an objective, an exclusion, a horizon. The interesting question is not whether an AI can parse that sentence. It can. The question is what, exactly, holds the system to those four commitments an hour later, when the portfolio arrives.

For most AI agents the honest answer is: nothing but the model's continued attention. The constraints live in the conversation, and conversations are where constraints go to soften. We built our agent differently — between your words and its work sits a formal language.

Start with what natural language gets right, because it gets a lot right. Natural language is descriptive, ambiguous, context-dependent, and redundant — and those aren't bugs. They are the product of centuries of evolution, and they are precisely what makes language the right medium for negotiating meaning under incomplete information. When an investor says "I want less tech risk, but don't churn my account," an agent needs ambiguity tolerance to even begin: which holdings count as tech, how much is less, what turnover is acceptable. Modern language models inherit this flexibility, and it's why they are genuinely useful partners in investment reasoning — interpreting intentions, reconciling conflicting signals, forming hypotheses. If you tried to strip the ambiguity out of that stage, you'd have built a form, not an advisor.

But investment management is a domain of consequences. Decisions affect accumulated wealth; errors in portfolio construction or risk oversight carry real costs; and the discipline that makes global markets function at scale is precisely finance's long habit of formal methods — contracts, controls, audit trails. High-stakes domains demand more than interpretation and reasoning. They demand explicit commitments, constraints, obligations, evidence, and accountability. Those are things a conversation, by its nature, does not pin down.

Henri Poincaré put the division of labor in one sentence in 1908: "It is by logic that we prove, but by intuition that we discover." Natural language is the medium of discovery — exploring objectives, preferences, beliefs, alternatives. Formal language is the medium of proof — the durable, checkable representation of what was actually decided. The recent success of language models does not shrink the role of the formal side. It enlarges it: the more responsibility a language-capable system takes on, the more valuable an explicit representation of its obligations becomes.

What does the agent actually commit to?

Languages differ on two axes that matter here. One is ambiguity tolerance — how much interpretive burden the language places on whoever applies it. The other is prescriptive force — whether the language merely describes states of the world, or encodes obligations that bind an agent. Colloquial English is flexible and descriptive. A programming language is precise and prescriptive. Constitutional law is the strange one — flexible and binding, which is why it needs courts. Contract law sits in the middle, balancing precision against the irreducible ambiguity of human affairs.

Our domain-specific language occupies a deliberate spot on that map, closer to a contract than to code. When a strategy has been drafted in conversation, the agent expresses it as a formal workflow contract: an explicit representation of everything the coming work is accountable to. Concretely, a contract encodes:

• Portfolio constraints — the benchmark, exclusions, position and concentration limits, turnover bounds, capital.
• Asset identities and data provenance — which securities, which identifiers, which data sources, so "the index" and "that stock" can't quietly drift mid-analysis.
• Temporal assumptions — the windows and as-of dates the analysis is allowed to use.
• Validation requirements — what must be checked, and what evidence satisfies each commitment, before a result counts.
• Execution rules — what the agent may do, must do, and must not do on the way to a recommendation.

Because the contract is written in a closed formal language — a fixed set of typed steps and rules, not free prose — it can be checked mechanically for errors, omissions, and inconsistencies. This is the part that changes the engineering: an ill-formed plan is rejected and repaired before any work runs, the way a compiler rejects a program rather than letting it fail in production. Verification stops being a final step and becomes part of how the system reasons.

And because every commitment must be satisfied by evidence, the contract carries a ledger of proof obligations — one per claim the final answer will rest on:

What happens between your message and the portfolio?

The whole path has five stages. Conversation handles ambiguity at the edges; the contract carries commitments through the middle; and an independent check sits at the end.

Here is that pipeline on a real session — the request from the opening paragraph, given to our agent verbatim: "Create a static, short-horizon investment portfolio. Use MSCI World as a benchmark and minimize the corresponding tracking error. Avoid oil and gas and linked industries. Request additional information as needed." The entire session, including everything below, is public as a read-only replay.

With intent clarified, the commitments compile into a contract and the deterministic work runs inside it: a screened ETF universe, three candidate constructions — a Vanguard pair, a risk-parity anchor across four screened funds, an iShares pair with the broadest screen — each tested for tracking error against a tradeable MSCI World proxy. Then comes the stage that makes this system unusual: the draft answer went to an independent verifier, and the verifier said no.

Read that verdict closely, because it is the contract doing its job. The tracking-error numbers were correct — a lazier system would have shipped them. What failed was an evidentiary obligation: the claim "these funds exclude fossil fuels" rested on the agent's summary rather than the issuers' documents. The agent went back, retrieved iShares' and Vanguard's own methodology documents, persisted the extracts as evidence, and resubmitted. Only then was it allowed to answer.

The recommendation itself is almost anticlimactic, which is rather the point: 73.1% in one screened ETF, 26.9% in another — the lowest-tracking-error construction among the candidates, satisfying the broad exclusion by the issuers' documented methodology, not by vibes. And the answer arrives wearing its own qualifications: the fit was estimated against a tradeable proxy over roughly two years of daily returns, and the design is explicitly static and short-horizon. For the full session — and a second one where the same machinery stress-tests a tactical strategy through Covid — see the companion walkthrough.

How do qualitative objectives fit a formal contract?

The obvious objection: this works for turnover limits and name counts, which a machine can check — but investors care about things no formula captures. That objection is right about the premise and wrong about the conclusion, and the distinction is exactly what the contract is for.

The evidence required to satisfy a commitment depends on its nature. Some commitments are verified mechanically: portfolio exposures, concentration limits, benchmark definitions, security identities, execution constraints. Others require research and interpretation. Take an investor who wants to track a broad index while overweighting companies with genuinely strong water stewardship — better efficiency, more recycling. "Genuinely strong" is not a number. The contract handles it not by pretending it is one, but by turning it into a research obligation: the formal spec names the objective, defines the universe and data sources, and obliges the workflow to gather specific evidence — company disclosures, independent assessments — evaluated against the stated criteria. That research becomes part of the record supporting the recommendation, reviewable alongside the tracking-error math.

This is the same settlement legal systems reached long ago. Laws and fiduciary obligations do not attempt to prescribe every action; they establish rules, responsibilities, and procedures within which judgment is exercised, and they distinguish what is mechanically checkable from what requires discretion. Attempting to formalize every decision produces systems that shatter on ambiguity and novelty — the very things markets reliably supply. The practical design is the one we chose: formal language for the commitments, constraints, and evidentiary requirements; agent judgment, exercised inside those boundaries, for everything that makes the problem genuinely hard.

What does this not prove?

• It doesn't eliminate ambiguity — it relocates it. The contract is only as good as the elicitation that produced it. If "fossil-fuel exclusion" was clarified carelessly, the system will faithfully verify the wrong commitment. The conversation stage is load-bearing.
• Interpretive evidence is still interpreted. For qualitative obligations, the contract specifies what evidence is required — whether that evidence is adequate remains a judgment, made visible rather than made mechanical.
• A verified portfolio is not a profitable one. The contract guarantees the work honored your constraints and the claimed checks ran; it says nothing about future returns. In the session above the agent named its own bounds: benchmark fit was estimated against a tradeable proxy ETF over roughly two years of daily returns — not the raw index series.
• Coverage grows with the language. A closed formal language is deliberately restrictive; objectives it cannot yet express fall back to conversational handling until the language grows to cover them.

What does a formal contract enable?

Once intent lives in a formal contract rather than a chat transcript, things that are impossible for conversational agents become routine. Every recommendation has a traceable path from investor intent through analysis, construction, and review. Constraints are enforced during the work, not audited after it. An independent reviewer — human or agent — can check the result against the same spec the work was built from, instead of re-deriving what the user probably meant. And when your objectives change, the delta is a contract amendment with consequences you can see, not a vibe shift in a conversation.

Formal languages have always worked this way: they extend human capability by making thought explicit and action reliable — algebra did it for quantity, double-entry bookkeeping for obligation, and our agent's research discipline for evidence. In the age of language-capable AI their role gets larger, not smaller. They are the bridge from conversation to commitment — from reasoning under ambiguity to accountable action.

Sources

• Lean, Theorem Proving in Lean 4: Introduction — formal verification as machine-checked claims expressed in precise mathematical terms.
• 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.
• Henri Poincaré, Science and Method (1908) — "It is by logic that we prove, but by intuition that we discover."
• Bertrand Meyer, "Applying 'Design by Contract'," IEEE Computer 25(10), 1992 — the software lineage of preconditions, postconditions, and invariants as contracts.
• Martin Fowler, Domain-Specific Languages (Addison-Wesley, 2010) — on small, closed languages built to make one domain's intent explicit.

What should you take away?