◆ Research Topic — Formal Methods

LLM for Formal Methods

Bridging natural language, code, and machine-checkable proof — teaching large language models to specify, verify, and repair with mathematical rigor.

NL Requirement ⟶ Formal Spec ⊢ Verified ✓

Papers

Venues

10k+

HuggingFace Downloads

Scroll to explore
▼

Featured Work

ACL '25

From Informal to Formal — NL Requirements to Verifiable Formal Proofs

Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian

Can LLMs turn ambiguous natural-language requirements into machine-checkable formal specifications? This work distills 18k GPT-4o instruction-response pairs to fine-tune LLMs across five formal languages — Coq, Lean4, Dafny, ACSL, and TLA+ — so a 7-8B model matches DeepSeek-R1-671B.

Paper HuggingFace Media

💡 A fine-tuned 7–8B model matches DeepSeek-R1-671B (80× larger) on formal specification generation across 5 proof languages.

📥 10k+ HuggingFace downloads 📱 37k+ social media reads

Natural Language Requirement

LLM

translate

Formal Specification · Coq (1 of 5 target languages)

Verification0/3 lemmas

Lemma add_comm✓ proved

Lemma bound_safe✓ proved

Theorem correct✓ proved

Featured Work

CAV '24

Enchanting Program Specification Synthesis by LLMs using Static Analysis & Program Verification

Cheng Wen, Jialun Cao (Corresponding), Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, Cong Tian

AutoSpec pairs an LLM with static analysis to synthesize ACSL specifications, then discharges them with Frama-C — producing annotations a deductive verifier can actually prove.

Paper Homepage

💡 LLM + static analysis verifies 79% of programs — a 1.592× improvement — validated on a real-world X509 parser.

✅ 79% of programs verified ⚡ 1.592× improvement over prior work 🔍 validated on real-world X509 parser

C Code → LLM + Static Analysis → C + ACSL → Frama-C → ✓ Verified

Input · C source

Output · C + ACSL annotations

max(int, int)✓ Verified

abs(int)✓ Verified

Featured Work

FM '26

ModelWisdom: TLA+ Model Visualization, Digest and Repair

Zhiyong Chen, Jialun Cao, Chang Xu, Shing-Chi Cheung

TLA+ specifications describe how systems evolve, but their state spaces are hard to read. ModelWisdom visualizes the state machine, digests its behavior, traces counterexamples, and repairs faulty transitions.

Paper Website

💡 Iterative LLM-driven repair can restore liveness properties in TLA+ specifications by detecting and removing faulty transitions.

Visualize · Digest · Repair

→Digest: LLM summarizes the state graph — 5 states, 5 transitions.

▸Visualize: click-through trace Init → Ready → Wait.

✗Bug: Wait → Run back-edge creates a livelock — Done unreachable.

⟳Repair (iterative): remove faulty back-edge, synthesize Wait → Done.

✓Verified: liveness restored, Done now reachable.

Featured Work

arXiv '26

Can Large Language Models Model Programs Formally?

Zhiyong Chen, Jialun Cao, Jiarong Wu, Chang Xu, Shing-Chi Cheung

Introduces Model-Bench: 400 Python programs from HumanEval, MBPP, and LiveCodeBench, each converted into a model-checking specification and checked by an accompanying model checker. Across the benchmark, LLMs show significant limitations in modeling program behavior formally.

Paper

💡 LLMs show significant limitations in formally modeling program behavior — even frontier models struggle with model-checking specifications.

Python Program → LLM → Model-Checking Spec → Model Checker → Verdict

⚠Finding: significant limitations in LLMs’ ability to formally model program behavior.

Model-Bench · 400 Python Programs

HumanEval

MBPP

LiveCodeBench

Featured Work

arXiv '26

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation

Dong Xu, Jialun Cao, Guozhao Mo, Junjie Hu, Cheng Wen, Hongyu Lin, Xianpei Han, Shengchao Qin, Cong Tian, Shing-Chi Cheung, Le Sun, Yaojie Lu

Benchmarks LLM and agent-based formal specification generation for C programs with rigorous evaluation that detects prover deception.

Paper HuggingFace

💡 Standard evaluation inflates results by ~20% because models can deceive automated provers — incorrect loop invariants remain the dominant failure mode.

LLM → Spec → Prover

⚠ naive eval +20% inflated

✓ Rigorous evaluation corrects for prover deception

Featured Work

ICCD '19

Learning-Based Parameterized Verification

Yongjian Li, Jialun Cao (1st student author), Jun Pang

Uses machine learning to automatically infer auxiliary invariants for parameterized protocol verification.

Paper

💡 Learning-based invariant inference can verify cache coherence protocols of arbitrary scale without manual lemma annotation.

Protocol (n params) → ML Invariant Learning → ✓ Verified for all n

✓ Cache coherence verified at arbitrary scale

Featured Work

ASE '18

L-CMP: An Automatic Learning-Based Parameterized Verification Tool

Jialun Cao, Yongjian Li, Jun Pang

A tool that automatically verifies parameterized concurrent protocols by learning inductive invariants from finite instances.

Paper

💡 Automated learning of protocol invariants eliminates the need for manual annotation — enabling push-button parameterized verification.

Finite Instances → Learn Invariants → Generalize → ✓ All Instances

✓ Push-button parameterized verification