Can I order PCB/chip manufacture from provided LOTOS specification?
Currently, no. Formal methods have successful uses in restricted domains : static timing analysis (that an FPGA or other digital circuit) meets the timing constraints you ask for, for one example.

It can also prove properties about software or hardware - such as correctness of a program written in SPARK (based on Ada) - eliminating the need for runtime checks, guaranteeing the impossibility of buffer overruns, integer overflows, etc.

A little more generally, formal can potentially prove the equivalence of two designs - or a design and a higher level specification - exposing errors in the design, for example. See "equivalence checking" in ASIC design - hasn't made it down to FPGA tools yet, as far as I know.

But formal methods don't - yet - allow synthesis of a detailed design at a high level. (One could argue that a compiler is a formal translation of a "high level" specification in C or Ada, into an assembly language design, but I don't think you'd regard C as sufficiently high level, and I'd agree.

In any case, comments suggest you are dealing in the analog domain, which is arguably even more backward, SPICE netlists still seem to be state of the art. You may wish to flesh out the question with something specific - perhaps illustrating 1 or 5 of your 50 lines of specification, to give us a better idea what you're asking.