Federal research
Feasibility prototype. Not awarded, not in production.Compositional Verification Engine
A typed bridge between machine-learning outputs and symbolic reasoning, with bounded inference, explicit abstention, and provenance on every decision.
A Rust prototype I built for a federal research solicitation: it translates typed ML outputs into logical facts, runs bounded reasoning through a real symbolic backend, and abstains when a case falls outside what it can support.
Problem
The problem.
Machine-learning models output scores; safety-critical decisions need reasoning that can be checked. Bolting an LLM on top produces fluent answers with no guarantees: no record of which inputs supported a conclusion, and no honest "I can't answer this" when the case is out of scope. The solicitation asked for the opposite, a bounded and inspectable seam between learned perception and symbolic reasoning, so I built a prototype to show the seam was feasible.
Approach
How I built it.
- Translate typed ML-style payloads into typed logical facts across an explicit IR boundary, so the reasoning layer works against a checked contract instead of raw model internals.
- Run inference through a real symbolic backend (Answer Set Programming via Clingo), not a hand-rolled rule engine, so the reasoning is bounded and the results are deterministic.
- Abstain by construction: unsupported or out-of-bounds inputs return an explicit "not supported" rather than a confident guess.
- Emit structured provenance for every decision (which facts and which rules produced the result) into a journal you can audit after the fact.
- Ship it as a roughly 2,100-line Rust codebase with 10 integration tests covering multi-rule composition, abstention, provenance, IR transforms, and determinism.
Architecture
What's running, and why.
Reasoning core
- Typed IR boundary
- ML-style payloads translated into typed logical facts; the reasoning layer never sees raw model internals.
- Symbolic backend (Clingo / ASP)
- Bounded, deterministic inference through a real Answer Set Programming backend.
- Abstention
- Out-of-bounds and unsupported inputs return an explicit non-answer by construction.
Evidence + provenance
- Provenance generator + journal
- Every decision records the facts and rules that produced it, into an auditable journal.
Build
- Rust + integration tests
- Roughly 2,100 lines of Rust, a single ~1 MB static binary, 10 integration tests passing.
Outcome
What shipped.
10 / 10
Integration tests passing: composition, abstention, provenance, IR transform, determinism
~2,100 LOC
Rust prototype compiling to a single ~1 MB static binary
Real ASP backend
Bounded symbolic reasoning via Clingo, not a toy rule engine
Abstains by design
Returns an explicit non-answer on out-of-bounds inputs instead of guessing
Submitted
Proposal delivered through formal federal channels. Not awarded, not in production.
Stack
- Rust
- Clingo (Answer Set Programming)
- Typed IR
- Cargo
- Integration test harness
What this proves
Where this ports.
Hard problems with a correctness bar (medical adjudication, compliance review, claims, government decisions) need more than a confident LLM answer. The pattern here (a typed boundary between learned perception and symbolic reasoning, bounded inference, abstention when unsupported, provenance on every output) ports to any domain where being wrong is expensive and a decision has to hold up to scrutiny after the fact.
Want the same pattern in your business?
Thirty minutes. Describe what you're working on and I'll tell you if I can ship it.