tric-proof

Inspiration

tric-proof grew from my research into applications of the Typed Ranked Incidence Complex (TRIC), a shared mathematical substrate connecting combinatorial topology, category theory, spectral analysis, and algebraic graph transformation. The theoretical foundation is available in The Typed Ranked Incidence Complex as a Mathematical Intersection (https://zenodo.org/records/19642980).

The project explores theorem proving as a concrete TRIC application. My longer-term goal is to combine it with a sibling C++ compiler frontend into a formal-verification system where humans and AI agents collaboratively author specifications, trace them through compiler transformations, and discharge the resulting obligations with independently checked evidence. Both projects remain useful independently: tric-proof is already a standalone proof assistant, while the C++ frontend is being developed as a separate compiler tool.

Together, they could eventually connect source-code semantics, compiler transformations, proof obligations, diagnostics, and checked evidence on one queryable substrate. I believe this could become especially valuable for agentic coding, where agents need more than code generation: they need trustworthy ways to understand, transform, and verify large software systems.

What it does

tric-proof verifies proofs written in a readable surface language from end to end. Its command-line interface can:

• check one or more proof files;
• report precise source-positioned diagnostics;
• format proof source;
• publish and replay checked proof bundles;
• query verified theorems and their dependencies; and
• support controlled proof re-derivation.

The verification path can be summarized as:

[ \text{source} \longrightarrow \text{coarse TRIC structure} \longrightarrow \text{proof-specific lowering} \longrightarrow \text{independent checking} \longrightarrow \text{replayable evidence}. ]

The current language includes dependent proof terms, equality reasoning, tactics, modules and notation, together with a small generic constructor/eliminator framework used for natural numbers and lists.

A key design principle is that frontend results are only proposals. Proof authority comes from an independent checker that reconstructs and validates declarations, terms, environments, dependencies, certificates, and capabilities before accepting them.

How I built it

The implementation is written in modern C++ and builds on three focused layers:

1. TRIC supplies the typed, ranked incidence substrate and its rewriting, indexing, canonicalization, and copy-on-write operations.
2. compiler-kit supplies shared grammarlet, fixed-point execution, lowering, and structural-analysis machinery.
3. compiler-proof describes the proof language’s coarse grammar, full grammar, and candidate analysis.

The proof-specific layer lowers coarse source spans directly into proof cells and records. This is intentionally different from the conventional tokenizer–parser–AST pipeline: it uses a coarse grammarlet to recover structure, then total proof-specific lowerers to cross the remaining semantic boundaries.

I built the project collaboratively with several generations of AI models. The most recent work was carried by GPT‑5.5 and now GPT‑5.6, which increased productivity substantially. I used the models not only as implementers, but as parallel researchers and independent reviewers. Work was divided into bounded goals with frozen contracts, objective acceptance matrices, mutation tests, performance censuses, and separate implementation and review roles.

What I learned

My strongest lesson is that much of today’s software-building infrastructure was designed before capable coding agents existed. Build systems, compiler interfaces, test organization, proof tooling, and review workflows often become the bottleneck—not the agents’ ability to reason about or implement the software.

Powerful agents can work at much greater scale, but only when the surrounding substrate gives them:

• explicit structure instead of ambiguous text;
• bounded and independently reviewable work;
• machine-checkable end conditions;
• stable provenance and replayable evidence;
• fast, targeted feedback; and
• clear separation between proposals and trusted authority.

Improving these foundations can unlock far more of what agentic systems are capable of while making their output safer and easier to audit.

Challenges

The first challenge was the project’s sheer size. The proof assistant spans language design, elaboration, tactics, dependent typing, inductive structures, compiler infrastructure, persistence, replay, diagnostics, and user-facing tooling.

The second was keeping agents aligned with its non-traditional architecture. Models frequently tried to reintroduce familiar compiler components—standalone tokenizers, ASTs, parse forests, recognition pipelines, or disambiguation stages—even when those components were unnecessary for the intended direct-lowering design.

The final challenge was preserving trust and usability at the same time. Independent replay, immutable authority, atomic publication, mutation resistance, and complete declaration-history checks are important, but naïve implementations can perform the same reconstruction repeatedly. Making the system responsive required tracing the full checking, hosting, bundle, and query dataflow and removing accidental multiplicative work without weakening independent verification.

What’s next

The next steps are to broaden generic inductive definitions and recursion, expand proof re-derivation, and grow the verified library.

When the sibling C++ frontend is ready, the two projects can be connected through the formal verification architecture: compiler facts and transformation witnesses on one side, proof obligations and independently checked evidence on the other. The intended result is a compiler-native formal-verification environment designed not only for human developers, but also for trustworthy large-scale agentic coding.

Built With

• c++