La brecha entre el diseño de software y la implementación a menudo resulta en una falta de claridad y precisión. Los lenguajes formales, basados en reglas matemáticas, lógica y símbolos, son invaluables para especificar y verificar diseños de sistemas. Varios lenguajes semi-formales y formales, como JSON, XML, lógica de predicados y expresiones regulares, junto con modelos formales como las máquinas de Turing, sirven a dominios específicos. Este documento presenta un nuevo lenguaje formal de especificación, ObTFL (Lenguaje Formal de Transacciones de Objetos), desarrollado para sistemas distribuidos de propósito general, como la especificación de las interacciones entre servidores y dispositivos IoT y sus protocolos de seguridad. El documento detalla la sintaxis y la semántica de ObTFL y presenta tres estudios de caso reales: aprendizaje federado, blockchain para redes de criptomonedas y bitcoin, y la placa PCB industrial con sincronización de máquinas, para demostrar su versatilidad y efectividad en la especificación formal de las interacciones y comportamientos de los sistemas distribuidos.