Quantitative research (in-house)
A verifiable research and execution platform
How we built an in-house research platform where AI agents run reproducible experiments, and where nothing reaches execution without passing risk controls whose safety rules are formally proved.
The challenge
Research driven by AI agents is fast but easy to fool: results that cannot be reproduced, statistics that overfit, and automation that could act on a bad conclusion. We needed agents to do real research while making it impossible for an unverified decision to reach execution.
What we built
- 1
Reproducible by construction
Every research run is a declared manifest, executed as a typed graph and sealed with fingerprints of the exact data and code used.
- 2
Statistics that resist overfitting
Walk-forward validation, purge and embargo gaps, block bootstrap and deflated performance metrics are built into promotion gates.
- 3
Agents as first-class researchers
External agent harnesses drive research through a small set of stateless primitives and can resume an investigation after a restart.
- 4
Formally verified safety rules
Safety rules such as "nothing reaches dispatch without full authority" are proved in Lean 4; a Datalog check shows code cannot bypass the risk gate; generated fixtures test production code against the model.
- 5
Built to be operated
Preview-then-commit execution, kill switch and halt states, reconciliation and written runbooks for every failure mode we could name.
Results
- 4,697execution-engine tests passing, 0 failures
- 22local quality and security gates on every change
- Lean 4proofs of core safety rules with conformance fixtures
Technology
- Python
- Polars
- Rust
- Julia
- Lean 4
- Soufflé Datalog
- Picat
Cosinara presents this platform as engineering work only. We do not offer investment, trading or financial services.