Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter).

C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1...

Java: http://ieeexplore.ieee.org/document/6042069

The C work seems more thorough.