There was a long period where a fairly unknown theorem proving language ATS (1) was beating C in many test cases on the benchmark game (2) the benchmarks were removed though (3). I expect many languages could be made to win with sufficient effort.
ATS is not really a theorem proving language, it's almost a superset of C with a very long list of type system and language features that lets you write anything from C code with no safety to very high level recursive functional code with lifetime tracking which will translate to efficient C code, if the transformations are proved to be correct. It's a weird beast, but I'm not surprised it outperformed some C implementations, because it is basically C with a lot more features.
