Consulting

Type-safe software and AI systems for complex problems

I build type-safe software and domain-specific AI tools, working hands-on with your engineers. When useful, I check architectural models and invariants in Lean or Agda alongside implementation. AI tools support engineering judgment; they do not replace it.

Areas of focus

Architecture-led implementation

I use Lean or Agda to model architecture and invariants. I can also prove selected properties of an algorithm or system. How much to formalize, and how much to implement alongside the model, depends on the problem.

Work on large codebases led me to create Compass, an open-source, concept-first workspace for coding agents that uses checked architectural models and semantic bindings to guide repository navigation and implementation. In Formal models versus Markdown specifications, I show how a checked model can carry more than a prose specification.

AI tools for specific domains

I build AI harnesses tailored to a domain. My private work includes audio-and-text processing, an agentic video stringout editor, and a multimedia indexer. The indexer can distribute asynchronous indexing jobs; it can also run on one machine with local AI models.

The customer work is private. I can explain the technical approach without naming customers or sharing their code. Separately, my open-source research projects ParaForge and its predecessor Heuron explore typed descriptions of neural networks. These are examples of my approach, not customer results.

Business automation

I also automate repetitive workflows that come up in many large enterprises. For example, synchronizing hundreds of data sources and building ways for non-specialists to interpret and aggregate the data.

How I work

First, we define the problem, constraints, and expected result. Then we agree on scope and decide whether a formal model would help or if other means are more appropriate. I document the result, and we can agree on checkpoints to review progress.

I talk more about how I use types and formal models in Thinking in Types.

Start a conversation

Email me an anonymized description of the problem, your constraints, and what you need to achieve. An abstract version is fine. Please do not send credentials, confidential code, customer data, or other sensitive material in the first email.

If it looks like work I can take on, I will reply with questions or initial thoughts. Email is free. If we decide to meet, the first 45-minute meeting costs €50 plus VAT where applicable. If we then agree to work together, the €50 goes toward that engagement. My availability is limited; I will confirm the fee before scheduling.