Small announcement: ✅ formal-git As an experiment, over the last 2 months we've modelled ~30% of Git in Lean 4, making heavy use of coding agents, and proved >8000 theorems of varying usefulness about the implementation. In the process of doing this we've uncovered >100 potential defects in Git v2.55, at least two of which may constitute security vulnerabilities. We've also built a DRT (differential random testing) harness and the biggest corpus of relevant pinned differential test cases for Git implementations with >10k unique tests at the moment. We've used the test cases to test our own small internal implementation of Git in TypeScript. The next step will be to differentially test all notable public Git implementations against this corpus of tests to help improve their correctness and security 🫡 We'll be reaching out to library maintainers in due course. If you have a Git implementation you'd like us to help you test, please reach out and let me know. We'll open-source all this eventually, after potential security issues that were uncovered are responsibly disclosed and fixed.