Weining Cao

Graduate student in Computer Science at Nanjing University.
I develop neuro-symbolic methods for program and distributed-protocol verification.

— Project Stars

101 Citations

Selected Research ↓ 🐙 GitHub

About

I am a graduate student in the School of Computer Science at Nanjing University and the State Key Laboratory for Novel Software Technology. My research combines large language models with formal reasoning to make verification more automated.

My recent work focuses on inductive invariant inference, counterexample-guided candidate synthesis, and machine-assisted proof development for distributed systems.

Research Interests

01 Inductive Invariant Inference

02 Distributed Protocol Verification

03 Neuro-symbolic Formal Verification

04 Automated Proof Generation

Publications

I3DP · SOSP 2026
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models

Weining Cao, Guangyuan Wu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma

Accepted at SOSP 2026 · First author
📄 View Preprint → 💻 View Code →
ISSTA 2025
Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference

Weining Cao, Guangyuan Wu, Tangzhi Xu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma

First author
📄 View Paper → 💻 View Code →
ASE 2024
LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference

Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma

Second author · Distinguished Paper Award
📄 View Paper → 💻 View Code →

Technical Blog

TLAPS
How We Used Agents to Produce a 6,000-Line TLAPS Proof

Agentic TLAPS proof generation for MongoLoglessDynamicRaft.
📄 Read Blog →

Education & Honors

EDUCATION
Nanjing University

Combined M.S.-Ph.D. program in Computer Science, School of Computer Science and State Key Laboratory for Novel Software Technology, Sep. 2023 - present.

B.Sc. in Computer Science, Kuang Yaming Honors School, Sep. 2019 - Jun. 2023.
HONOR
Distinguished Paper Award, ASE 2024