A formally verified R-tree implementation
kuruczgy.com