I reverse engineered the binary to find the encoding function, converted it to Python, and verified correctness. I then wasted a bunch of time making an iterative bruteforcer, until I realized that the encoding function is basically equivalent to:

bits('RTFM') + tab[buf[0]] + '00' + tab[buf[1]] + '00' + ... + tab[buf[n]]

where tab is a mapping from ascii characters to variable-length bitstrings, with the important property that they start and end with 1s, and contain no 00s. (match /^1.*1$/ but not /00/)

After that, decoding is simple.