Formalizing LLM Guardrails with AgentSpec in Lean 4
Executable Lean 4 semantics and 42 machine-checked theorems for AgentSpec, a DSL for runtime enforcement of LLM agent behavior. Fall 2025.
Paper · Code
Projects
Formalization projects, each with a paper and a code repository.ProbaLean: A Probabilistic DSL in Lean 4
A discrete probabilistic programming language in Lean 4 with denotational semantics over s-finite measures on Mathlib and a machine-checked soundness proof. Spring 2026.
Paper · Code