Some questions about Larch

I'm Noemie Slaats and I read about Larch on internet.

I'm a PhD student in Gent, and I'm looking for a good theorem prover
which I can use in the area of formal specifications and verifications.
It is not clear to me if Larch is suited for this job.

I read about LP and although it is not an automated theorem prover 
it seems to be o good theorem prover. And when I'm not wrong this 
system contains more than just a metalanguage.
But now about the specification language. I don't understand completely
what this language does. Is this just a metalanguage and do you need to 
implement the object language yourself or is it a complete specifcation
If it is possible I would like to get some more information about LCL and 

Thanks a lot,