LeanLang for Verified Autonomy
Who sacked my cluster?
Sachin Kumar Singh
Winner
Judges say
This is the highest-graded project. The judges noted it has a "realistic model of k8s" and proves "sensible theorems," making it the clear winner.
Winner says
I worked on making a formally verified model of Kubernetes in Lean, that was used as a judge during reinforcement learning to train a model that can be used as an SRE agent.
This was my first time working with Lean (or any theorem proving language) and it seemed to fill most of the gaps that I saw as potential issues with the rise of AI agents.
Access the code
Sambar & Soundness
Vimala S.
Durwasa Chakraborty
Winner
Judges say
Tied with Kleisli Triple on both Grade and Expertise, it takes 2nd prize because it achieved "end-to-end verification" and a "working LLM → jq → SQL pipeline," whereas Kleisli Triple was noted as needing "further furnishing" and having potential scalability issues.
Winner says
Vimala S.
The project gave me the opportunity to apply formal verification in a practical setting while learning Lean.
Durwasa
I'm deeply grateful to Dr. Siddhartha Gadgil for the mentorship and resources that made learning Lean4 possible for us.
Access the code
Five projects that stood out
Kleisli Triple
A toy model of a version control system (VCS) with verified behavior to flag merge conflicts and certify safe actions for collaborating agents.
Access the code
Judges say
Despite some concerns about scalability, it is technically very strong and was one of the highest-rated projects overall.
FlowGuard
A formal verification framework that proves a foundational safety property: individual agent safety does not guarantee compositional safety. It detects emergent capabilities in multi-agent systems before deployment.
Access the code
Judges say
Highly praised by the judges for its theoretical approach to multi-agent systems and for mechanizing "impossibility results."
MARS
A bridge between LLMs and Lean4 that rigorously verifies the legality and soundness of chess mate-in-N puzzles.
Access the code
Judges say
The highest expertise score among the Grade 2 projects, providing a "nice demonstration of what's possible with Lean + verification."
Caplean
A capability envelope for agentic coding pipelines, ensuring agents only invoke operations within their declared scope.
Access the code
Judges say
A very comprehensive submission that delivered all three core objectives, including a bonus Python middleware layer and a Cursor/MCP integration.
Totientfunction
A Lean 4 library that turns redaction policies into proof-carrying artefacts to ensure safe data handling in multi-agent pipelines.
Access the code
Judges say
The judges specifically highlighted that the "framing, implementation, and theorems are nice," making it stand out among other Grade 2 projects.
