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

Category: devtools

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

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

Formal is an LLM-driven property checker that uses Lean 4 and Mathlib to verify properties of pure functions in code. It's interesting because it combines large language models 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

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

View on Hacker News