Show HN: Llmll – AI agents fill typed holes, an SMT solver rejects wrong fills

Category: devtools

Tags: formal-verification, ai-agents, smt-solver, haskell, programming-language

Score: 6.8/10 (Innovation: 7, Technical: 8, Documentation: 7, Utility: 5)

LLMLL is a Haskell-based programming language and verification pipeline designed for AI agents to fill typed holes under formal contracts, with Z3/SMT proving each body against its specification before merging. It introduces a structured agent protocol using JSON-AST patches and trust levels, and optionally uses Leanstral and Lean for kernel-checked proofs beyond SMT. The project is an interesting experiment in verification-driven AI coding, though its niche focus and experimental status limit broad utility.

Target audience: researchers and developers interested in AI-assisted formal verification and programming language design

Repository: https://github.com/machunter/llmll · Haskell · GPL-3.0 · 1 stars

View on Hacker News