yamafaktory/formal: Lean 4 증명 엔진 기반의 LLM 구동 코드 속성 검사기

이 프로젝트는 LLM의 추론 능력과 Lean 4의 수학적 엄밀함을 결합하여 코드의 논리적 타당성을 검증하는 파이프라인을 제공한다. LLM이 소스 코드에서 순수 함수를 식별하고 만족해야 할 속성을 추출한 뒤, 이를 Lean 4 정리(Theorem)로 변환하여 증명을 시도하는 방식으로 작동한다. Lean 4는 기계적으로 증명을 검증하므로 LLM이 범할 수 있는 논리적 오류를 확실히 걸러낼 수 있다. 결과적으로 계산 로직이나 비즈니스 규칙 등 순수 도메인 로직의 신뢰성을 높이는 데 기여한다.