Skip to content

AI engineer, designer, implementer · St. Paul, Minnesota

AI, Software, Design Engineer.

Ontomancer and Claw Fanatic.

AI engineer, designer, implementer — usually all three on the same project. I build ontologies and reasoning agents that keep language models honest, design the interfaces people actually touch, and write the proofs and evaluations that say whether any of it works.

See the proofs Selected work

What I work on

Proof, not sampling

Formal verification

Model checking establishes properties over all inputs in a bounded space. A test tells you about the cases you thought of.

Measure what you cannot prove

AI security & evaluation

Language models are probabilistic. Where proof does not apply, the answer is graded evaluation, determinism, and adversarial testing.

Structure a reasoner can traverse

Symbolic grounding

Formal schemas turn tacit domain knowledge into something a reasoner can walk and a model can be held accountable to.

The loop is the product

Agents, workflows & harnesses

An agent is easy to demo and hard to trust. The interesting engineering is the harness around it — what it is allowed to do, what grades it, and whether the same input twice gives the same answer.

Corpora nobody has built yet

Data mining

Fine-tuning a model for a domain means first having the data for it, and for the domains I care about that data does not exist in a convenient form. So I go and build it.

Wireframe through to deploy

Platforms & full stack

The verification work only matters if the thing ships. I build the whole path — schema, API, interface, pipeline, host — and I have run it in production for paying customers.

Formal verification

72 proof harnesses, across 44 files.

A statistical library is a poor fit for testing alone: the interesting failures are index arithmetic, float edge cases, and structural invariants that only break on inputs nobody thinks to write down. Kani model-checks these over every input in a bounded space.

  • resampling_permutation_is_bijection — A permutation resampler emits each index exactly once — it permutes rather than merely shuffling.
  • resampling_kfold_test_sets_partition — K-fold test sets partition the dataset: no sample is held out twice, none is silently dropped.
  • resampling_bootstrap_indices_in_bounds — Every bootstrap draw indexes inside the sample, for all sample sizes.
  • resampling_loo_indices_partition — Leave-one-out splits cover the dataset exactly once each.
All 12 shown

Selected work

All projects

stats-claw

Data science on the hot path

In-process statistical computing for Rust — distributions, hypothesis tests, and resampling — with zero runtime dependencies, validated against scipy.

yee-claw

private

An ontology as a type system

An ontological application builder for verified code generation. A TypeDB ontology is the source of truth; a zero-dependency generator compiles it into the Rust type layer that hand-written numerics are built against.

cobol-coder

A small model that reads COBOL

A Qwen2 0.5B fine-tune for COBOL system understanding, trained with Unsloth and Hugging Face Transformers.

COBOLEval

Measuring generated COBOL

A substantial rebuild of bloop's COBOL code-generation benchmark, adding JCL static analysis, an agentic orchestrator, and local inference.

Writing

All posts