Show HN: Formal – LLM-driven property checker, backed by Lean 4 and Mathlib

Category: devtools

Tags: formal-verification, llm-tooling, proof-assistant

Score: 7.3/10 (Innovation: 8, Technical: 7, Documentation: 8, Utility: 6)

Formal is an LLM-driven property checker that uses Lean 4 and Mathlib as a proof engine to verify properties of pure functions in code. It's interesting because it combines LLMs for code understanding and theorem generation with a rigorous proof assistant for mechanical verification, creating a novel bridge between informal code and formal methods.

Target audience: backend devs, software engineers, ai engineers

Repository: https://github.com/yamafaktory/formal · Python · 10 stars

View on Hacker News