Open-source library
FloatLib: Verified Floating-Point Arithmetic in Lean
We care about a future where important scientific and mathematical work can be checked, trusted, and built on with confidence. Our lab develops tools that make formal verification more approachable and useful in practice, using large language models together with proof assistants like Lean. Our interests span scientific computing, software, experimental workflows, and pure mathematics: anywhere correctness, reproducibility, and rigorous reasoning matter.
We also believe this work should be open and collaborative. Our tools, benchmarks, datasets, and research artifacts are open sourced here whenever possible, so that others can inspect them, build on them, and help improve them. Formal verification has the potential to become part of everyday scientific practice, but that will only happen if the community can experiment with the technology, understand how it works, and adapt it to real problems across disciplines.
If this vision resonates with you, we would love to hear from you. Whether you have questions, ideas, use cases, or features you wish existed, please reach out.