Inch [1] has an example using complexity annotations, showing that a red-black tree insert/delete are linear in the black height.

ATS [2] is my go-to language for static guarantees with C's efficiency. Not sure if it counts as small but the implementation is not big.

[1] https://github.com/adamgundry/inch [2] http://www.ats-lang.org