Show HN: Formal – Formal verification for AI-generated code using Lean 4

Category: devtools

Tags: formal-verification, ai-code-generation, lean4, code-correctness

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

Formal is a tool that automatically extracts correctness properties from pure functions in AI-generated code, translates them into Lean 4 theorems, and machine-checks them using Mathlib. It's interesting because it provides mathematical proof rather than just tests for AI-produced logic, bridging formal verification with modern AI coding workflows.

Target audience: backend devs, ai engineers, devops

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

View on Hacker News