This paper contributes towards a multi-paradigm approach for the specification validation verification and refinement of concurrent agile systems. It brings together two complementary rigorous and largely accepted frameworks: Meseguer’s true-concurrent Rewriting Logic (RL) with its Maude prototype and Lamport’s Temporal Logic of Actions (Tla) with its current prototype Tla+. At the specification / validation phase, we adopt a variant of Maude that we endow with strategy for controlling rules and state splitting / recombining for exhibiting full intra-concurrency. For the verification / refinement phase, we automatically derive Tla’s formulas from validated Maude specification, on which crucial properties are checked using Tla’s deductions and invariants. A production system is considered as proof-of-concept.