Abstract This extended abstract reports on recent industrial activities exploring pragmatic and controlled uses of AI in railway systems developed with formal methods. First, large language models are used to synthesize and query large-scale railway technical specifications, improving accessibility while requiring systematic human validation. Second, early experiments assess AI-assisted generation of interactive proof scripts for B method proof obligations, showing initial productivity gains but substantial research challenges. Third, AI-based perception is integrated into railway safety functions, where machine learning acts solely as a proposer whose outputs are redundantly checked by a formally verified safety controller. Finally, a proof of concept applies multimodal language models to relay-based railway interlocking systems, automatically transforming relay diagrams into propositional logic specifications applicable to new diagrams. The results confirm that AI-assisted formalization is feasible and accessible, opening promising perspectives for advancing automation and trustworthiness in railway formal verification.