Project showcase: NetTopologySuite.Proofs (JTS/NTS companion)

[grootstebozewolf]

Cross-posted from Zulip (already live discussion):
#rocq-community-devs & users > Project showcase: NetTopologySuite.Proofs (JTS/NTS companion)

---

Project
NetTopologySuite.Proofs — mechanically-verified formalisation of foundational properties of geometry algorithms used in NetTopologySuite (the main .NET port of JTS).

Repo: https://github.com/grootstebozewolf/NetTopologySuite.Proofs

Key points

• 1100+ theorems, all Qed, no Admitted
• Only 3 standard classical reals axioms + audited Flocq slice
• 6 machine-checked counterexamples with witnesses

Focus
Algorithmic / production computational geometry (robust orientation, intersection, snap-rounding, overlay, curve linearisation) with tight alignment to real code (NTS/JTS issues), rather than axiomatic geometry (different angle from e.g. GeoCoq).

Tooling

• CI-enforced admitted/counterexample registry
• Observatory dashboard
• Oracle → test generation loop (proofs directly feed implementation tests)

---

What I’m looking for (concrete questions)

1. Packaging
   Should the foundations layer (real/vec/bbox/orientation/…) be stabilised first as a standalone opam library (rocq-geometry-foundations or similar) before considering upstreaming?

2. Structure / boundaries
   Where does the community usually draw the line between reusable library vs application-specific proofs?

3. Reusable patterns
   The CI-enforced admitted workflow + oracle loop — is this something worth extracting as a community pattern?

Concrete decision question
Should such foundations be stabilised as a standalone opam package first, or upstreamed incrementally per theory?

I’m happy to stay primary maintainer for now and am open to co-maintainers or any guidance on the best path.

Happy to demo the dashboard + oracle live or share the audit scripts/CI.

Thanks in advance!