Show HN: Formally Verified FPSan

Category: other

Tags: formal-verification, floating-point, lean, compiler, proof-assistant

Score: 5.0/10 (Innovation: 6, Technical: 7, Documentation: 5, Utility: 2)

This project formally verifies the correctness of Triton's FPSan sanitizer by lifting its C++ implementation into Lean and proving homomorphism, ring, and trigonometric identities using floating-point definitions. It's interesting as it applies advanced proof techniques (e.g., Macintyre's theorem) to a practical compiler sanitizer, though it remains a highly specialized academic effort.

Target audience: researchers, formal methods engineers

Repository: https://github.com/bollu/fpsan-verification · Lean · 2 stars

View on Hacker News