About Me
I am Qian Cheng (程潜), a PhD student in the Department of Computer Science at Nanjing University. My research lies at the intersection of formal methods, software systems, and artificial intelligence. I develop agentic tools for formal specification, model checking, and formal proof of complex real-world systems.
Research Interests
My primary research area is formal methods for real-world systems, especially model checking and specification-driven assurance. I am also exploring how generative AI can help create and refine formal specifications for complex computer systems. I am particularly interested in:
- AI-assisted authoring and maintenance of formal specifications
- Generative AI techniques that bridge software engineering and formal methods
Education
- PhD in Computer Science, Nanjing University, 2024 - Present
- Advisor: Yu Huang
- Research focus: Formal methods on real-world systems
- Bachelor in Computer Science, Nanjing University, 2020 - 2024
- Department of Computer Science
News
- 2026-08-13: Released Specula v1.1.0.
- 2026-07-28: Released our paper, “Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code.”
- 2026-07-13: Released TLAPS-Bench v1.0.0, a benchmark for AI-written, machine-checked TLAPS proofs.
- 2026-01: Our paper “SysMoBench” is accepted to ICLR 2026!
- 2025-11-12: Presented Specula at the TLA+ Community meeting (talk recording).
- 2025-08: Winners of the TLAi+ Challenge.
Projects
- Specula: An agentic system that generates and validates TLA+ specifications, uses model checking to find deep bugs, and reproduces them in real system code. [Website] [Paper]
- TLAPS-Bench: A benchmark for evaluating AI’s ability to write machine-checked TLAPS proofs, covering both proof completion and proof construction from scratch. [Website]
- SysMoBench: Benchmark suite and artifacts for system modeling and runtime verification. [Website]
Publications
- Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, Tianyin Xu. “Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code.” arXiv preprint, 2026. [Paper] [Code]
- Qian Cheng, Ruize Tang, Emilie Ma, Finn Hackett, Peiyang He, Yiming Su, Ivan Beschastnikh, Yu Huang, Xiaoxing Ma, Tianyin Xu. “SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems.” ICLR 2026. [arXiv]
- Tang Ruize, Huang Yu, Ouyang Lingzhi, Cheng Qian, Zhang Yuqi, Ma Xiaoxing. “Research Progress on Distributed System Model Checking.” Journal of Software. (In Chinese)
Contact
Feel free to reach out to me via email at cq@smail.nju.edu.cn