Hi, I'm Yuri 👋

I'm a software engineer interested in formal verification, theorem proving, and programming language theory.

What I'm working on

• categorica — An experimental proof engine for category theory using equational reasoning and e-graphs. Think "Vampire for CT."

• lean4-shimmer — Autogenerates reverse FFI shims for Lean exports

• strandal — A multi-threaded Interaction Combinators implementation in Rust

  Areas of interest

• Lean 4 — metaprogramming, FFI, tooling

• Category theory — applied CT, categorical databases, functorial semantics

• Proof automation — e-graphs, term rewriting, ATP

• Interaction nets — optimal reduction, graph rewriting

  Previously

  I've spent time with algorithmic trading systems, constraint solvers, and distributed systems. My GitHub history goes back to 2010 — some ancient repos are still here as artifacts.

        📍 Los Angeles, CA