Sora、Gen-3、MovieGen和CogVideoX等文本到视频模型的最新进展正在突破合成视频生成的界限，并在机器人技术、自动驾驶和娱乐等领域得到应用。随着这些模型的普及，涌现出各种评估生成视频质量的指标和基准。然而，这些指标强调视觉质量和流畅性，而忽略了时间保真度和文本到视频的对齐，这对于安全关键型应用至关重要。为了解决这一差距，我们引入了NeuS-V，这是一种新颖的合成视频评估指标，它使用神经符号形式化验证技术严格评估文本到视频的对齐。我们的方法首先将提示转换为形式化定义的时间逻辑（TL）规范，并将生成的视频转换为自动机表示。然后，通过正式检查视频自动机是否符合TL规范来评估文本到视频的对齐。此外，我们提供了一个包含时间扩展提示的数据集，以评估最先进的视频生成模型与我们的基准。我们发现，与现有指标相比，NeuS-V与人工评估的相关性提高了5倍以上。我们的评估进一步表明，当前的视频生成模型在这些时间上复杂的提示方面表现不佳，突出了未来改进文本到视频生成能力的必要性。