Research
The category and the foundation
How we read the verified-runtime category, and the mechanized foundation the trust stack rests on.
Category
The category
A verified runtime for AI-generated code is the next infrastructure layer. The forces driving this are structural. Coding agents now produce code faster than human review can absorb. Type systems and formal methods, after decades of waiting for the right workflow, finally have one. The verification bottleneck becomes the determining factor in what AI can be trusted to do.
C Proof operates at the substrate layer. Whole categories of bug refuse to compile because the type system carries enough semantic information to reject them. Properties bind implementations to specifications. Proof artifacts make the trust story inspectable. The runtime is designed for code that machines write and people supervise, not for code humans write line by line.
Foundation
The mechanized foundation
The Chelis language semantics are mechanized in Lean 4. The core type-system guarantees rest on machine-checked theorems rather than implementation choices that could drift.
- Type soundness: well-typed programs do not get stuck.
- Dimension safety: named tensor shapes line up.
- Effect correctness: effects occur only where allowed.
- Linearity soundness: linear values keep their usage discipline.
- AD correctness: differentiation follows the formal specification.
The mechanization is what makes the trust stack defensible. A type system that catches dimension errors is useful. A type system whose dimension-safety property is a theorem is a different kind of artifact. The compiler implements what the proof certifies.
Verification
The verification machinery
Specifications enter Chelis as typed program properties, derived from structured English requirements, mathematical notation, or migrated from existing typed code. A dispatcher routes each property to the strongest available proof.
Type-level discharge handles structurally provable properties at compile time. An SMT solver discharges arithmetic and transcendental properties where the math admits formal proof. Randomized validation with reproducible seeds covers properties too complex for either, with the route and evidence labeled on every result.
The output is an audit chain. Every property carries its proof tier, the solver and logic used where applicable, the evidence behind the result, and provenance back to the originating specification. The chain extends from the source of truth your team approved through the compiled binary that runs in production.
Expansion
The expansion path
Quantitative finance is the first vertical because the pain is acute and current. The architecture is domain-general. The same checked path behind a pricing model applies to a drug dosing calculation, a flight control constraint, a process safety property, or a grid protection rule. What changes from one to the next is the domain knowledge in the specification, not the machinery underneath.
The deeper expansion follows the same shape. Scientific computing, where correctness in numerical workloads matters. Climate and weather modeling, where simulation results inform consequential decisions. AI research, where the substrate for trustworthy code becomes the substrate for trustworthy inference and increasingly trustworthy training. The category position is the substrate underneath any computation where errors carry real cost.
Scope
What we do not claim
The trust stack is explicit about its scope. The type system catches the bugs the type system catches. Properties verify what properties verify. Proof artifacts say what was proved and what was statistically validated.
A correct implementation of a wrong specification is still wrong code. Verification does not write the right specification for you. Domain judgment still belongs to the people who understand what their code should do.
The trust we offer is structural and inspectable, not absolute.
Contact