For decades, formal methods occupied a peculiar position in software engineering: universally respected and almost universally avoided. The idea of mathematically proving that software behaves correctly—rather than merely testing it on a finite set of inputs—appeals to anyone who has suffered the consequences of a software bug in a safety-critical system. But the cost of formal verification—in specialized expertise, in development time, in tool complexity—confined it to a narrow niche: avionics, nuclear systems, and the occasional security protocol.

AI is changing this economics. Not by replacing formal verification with something less rigorous, but by automating the most labor-intensive parts of the verification process. LLMs that generate proof obligations, RL agents that search proof spaces, and generative AI that produces verified code alongside its proofs are collectively making formal methods accessible to a broader class of software projects.

Averill's essay (presented at ACM, 2025) captures the moment with an apt theatrical metaphor: formal methods have been waiting in the wings while testing held center stage. The escalating scale and sophistication of cyberattacks, combined with AI's ability to reduce verification costs, may finally bring formal methods onto the main stage of software development.

Automotive Software: Where the Stakes Justify the Cost

Pan et al. focus on the domain where formal verification is most urgently needed and where AI assistance provides the greatest leverage: automotive software. Modern vehicles contain substantial amounts of software code, with safety-critical subsystems—braking, steering, collision avoidance—subject to rigorous verification requirements. The automotive safety standard ISO 26262 highly recommends formal verification for the highest Automotive Safety Integrity Levels (ASIL-D), making it one of the preferred verification methods for safety-critical automotive software.

Their workflow demonstrates the AI and model-based engineering synergy:

The closed loop between generation and verification is the key innovation. Traditional development separates these activities—code is written first, then (if budget permits) verified. The integrated approach makes verification a continuous constraint on generation, catching errors at creation time rather than after deployment.

Testing-Based Formal Verification

Liu et al. propose a middle ground between full formal verification (proving correctness for all inputs) and traditional testing (checking correctness for selected inputs). Testing-based formal verification (TBFV) uses formal methods to guarantee that tested execution paths are correct, while testing ensures that enough paths are exercised to provide meaningful coverage.

Their contribution is a condition sequence coverage criterion that determines which test cases are needed to maximize the paths verified by TBFV. The automated test case generation tool produces test inputs that, when combined with formal path verification, provide coverage guarantees stronger than testing alone but achievable at lower cost than full formal verification.

This pragmatic approach may represent the most adoptable path for bringing formal methods into mainstream software development: not full verification of everything, but formal verification of the paths that matter most, combined with testing for the rest.

LLM-Driven SAT Solving

Sheng et al.'s SolSearch applies LLMs to a foundational formal methods tool: SAT solvers. The Boolean satisfiability problem (SAT)—determining whether a logical formula can be satisfied—underlies most automated verification tools. Better SAT solvers directly improve the scalability of formal verification.

SolSearch uses LLMs not to solve SAT instances directly but to generate efficient SAT-solving code. The LLM explores different algorithmic strategies for specific categories of SAT problems, generating solver code that is optimized for the problem structure at hand. This is a form of automated algorithm design: the LLM acts as a programmer that writes solvers tailored to each verification task.

The results show that LLM-generated solvers can outperform general-purpose solvers on structured instances—the type of instances that arise from real software verification problems. The approach does not replace decades of SAT solver engineering but adds a learned, problem-specific optimization layer on top of it.

Claims and Evidence

Open Questions

What This Means for Your Research

For software engineering researchers, the AI-formal methods convergence creates a new research agenda: not just building better verification tools, but building tools that integrate seamlessly with AI-assisted development workflows. The automotive use case (Pan et al.) provides a template; similar integration opportunities exist in medical devices, financial systems, and critical infrastructure.

For formal methods researchers, AI addresses the field's historical adoption barrier: cost. If LLMs can automate requirement formalization, proof generation, and test case synthesis, the human effort required for verification drops substantially—potentially enough to make formal methods economically viable for a much broader class of software.

For practitioners building safety-critical systems, the message is that the traditional choice between "verified but expensive" and "unverified but practical" is dissolving. AI-assisted formal methods offer a middle path that provides meaningful correctness guarantees at a cost that mainstream development budgets can absorb.

면책 조항: 이 글은 정보 제공을 목적으로 한 연구 동향 개요이다. 학술 연구에서 인용하기 전에 구체적인 발견, 통계, 주장은 원본 논문을 통해 반드시 확인해야 한다.

형식적 방법의 조용한 귀환: AI가 수학적 소프트웨어 검증을 실용화하다

수십 년간 형식적 방법(formal methods)은 소프트웨어 공학에서 독특한 위치를 차지해 왔다. 즉, 보편적으로 존중받으면서도 거의 보편적으로 기피되어 왔다. 유한한 입력 집합에 대한 테스트에 그치지 않고 소프트웨어가 올바르게 동작함을 수학적으로 증명한다는 개념은, 안전 필수 시스템(safety-critical system)에서 소프트웨어 버그의 결과를 경험해 본 이라면 누구에게나 매력적으로 다가온다. 그러나 형식적 검증(formal verification)에 수반되는 비용—전문 지식, 개발 시간, 도구의 복잡성—은 이를 항공전자, 원자력 시스템, 일부 보안 프로토콜이라는 좁은 틈새 영역에 가두어 왔다.

AI가 이러한 경제 구조를 바꾸고 있다. 형식적 검증을 덜 엄밀한 무언가로 대체함으로써가 아니라, 검증 프로세스에서 가장 노동 집약적인 부분을 자동화함으로써 말이다. 증명 의무(proof obligation)를 생성하는 LLM, 증명 공간을 탐색하는 RL 에이전트, 증명과 함께 검증된 코드를 생산하는 생성형 AI는 총체적으로 형식적 방법을 더 넓은 범주의 소프트웨어 프로젝트에서 접근 가능하게 만들고 있다.

Averill의 에세이(ACM, 2025 발표)는 이 순간을 적절한 연극적 은유로 포착한다. 즉, 형식적 방법은 테스팅이 중심 무대를 차지하는 동안 무대 뒤에서 대기해 왔다. 사이버 공격의 규모와 정교함이 갈수록 높아지는 상황과, AI가 검증 비용을 낮추는 능력이 결합되면서 형식적 방법이 마침내 소프트웨어 개발의 주 무대에 오를 수 있게 될지도 모른다.

자동차 소프트웨어: 비용을 정당화하는 위험 수준

Pan et al.은 형식적 검증이 가장 시급하게 필요하며 AI 지원이 가장 큰 효과를 발휘하는 영역인 자동차 소프트웨어에 주목한다. 현대 차량에는 상당한 양의 소프트웨어 코드가 탑재되어 있으며, 제동, 조향, 충돌 회피 등 안전 필수 하위 시스템은 엄격한 검증 요구 사항의 적용을 받는다. 자동차 안전 표준인 ISO 26262는 가장 높은 자동차 안전 무결성 등급(ASIL-D)에 대해 형식적 검증을 강력히 권장하며, 이를 안전 필수 자동차 소프트웨어의 선호 검증 방법 중 하나로 규정하고 있다.

이들의 워크플로우는 AI와 모델 기반 공학(model-based engineering)의 시너지를 보여 준다.

생성과 검증 사이의 폐루프(closed loop)가 핵심적인 혁신이다. 전통적인 개발은 이 두 활동을 분리한다. 즉, 코드를 먼저 작성하고, 예산이 허락하면 이후에 검증한다. 통합된 접근법은 검증을 생성에 대한 지속적인 제약 조건으로 삼아, 배포 이후가 아닌 생성 시점에 오류를 포착한다.

테스팅 기반 형식적 검증

Liu et al.은 완전한 형식적 검증(모든 입력에 대한 정확성 증명)과 전통적인 테스팅(선택된 입력에 대한 정확성 확인) 사이의 중간 지점을 제안한다. 테스팅 기반 형식적 검증(testing-based formal verification, TBFV)은 형식적 방법을 사용하여 테스트된 실행 경로가 올바름을 보장하는 한편, 테스팅을 통해 의미 있는 커버리지를 제공할 만큼 충분한 경로가 실행되도록 한다.

이들의 기여는 TBFV가 검증하는 경로를 최대화하기 위해 필요한 테스트 케이스를 결정하는 조건 시퀀스 커버리지 기준(condition sequence coverage criterion)이다. 자동화된 테스트 케이스 생성 도구는 형식적 경로 검증과 결합될 때, 테스팅 단독보다 강력하지만 완전한 형식적 검증보다 낮은 비용으로 달성 가능한 커버리지 보장을 제공하는 테스트 입력을 생성한다. 이러한 실용적 접근 방식은 형식적 방법(formal methods)을 주류 소프트웨어 개발에 도입하는 데 있어 가장 수용 가능한 경로를 나타낼 수 있다: 모든 것을 완전히 검증하는 것이 아니라, 가장 중요한 경로에 대한 형식적 검증(formal verification)과 나머지에 대한 테스팅을 결합하는 방식이다.

LLM 기반 SAT 풀이

Sheng 등의 SolSearch는 LLM을 형식적 방법의 근본적인 도구인 SAT 솔버(SAT solver)에 적용한다. 논리 공식이 만족될 수 있는지를 판단하는 부울 만족 가능성 문제(Boolean satisfiability problem, SAT)는 대부분의 자동화된 검증 도구의 기반을 이룬다. 더 나은 SAT 솔버는 형식적 검증의 확장성을 직접적으로 향상시킨다.

SolSearch는 LLM을 SAT 인스턴스를 직접 풀기 위해서가 아니라 효율적인 SAT 풀이 코드를 생성하기 위해 사용한다. LLM은 특정 범주의 SAT 문제에 대한 다양한 알고리즘적 전략을 탐색하여, 당면한 문제 구조에 최적화된 솔버 코드를 생성한다. 이는 자동화된 알고리즘 설계의 한 형태로, LLM이 각 검증 작업에 맞춤화된 솔버를 작성하는 프로그래머 역할을 한다.

결과에 따르면 LLM이 생성한 솔버는 구조화된 인스턴스—실제 소프트웨어 검증 문제에서 발생하는 유형의 인스턴스—에서 범용 솔버를 능가할 수 있다. 이 접근 방식은 수십 년에 걸친 SAT 솔버 공학을 대체하는 것이 아니라, 그 위에 학습 기반의 문제별 최적화 계층을 추가한다.

주장과 근거

미해결 질문

연구자에게 주는 시사점

소프트웨어 공학 연구자에게 있어, AI와 형식적 방법의 융합은 새로운 연구 의제를 창출한다: 단순히 더 나은 검증 도구를 구축하는 것이 아니라, AI 보조 개발 워크플로우와 원활하게 통합되는 도구를 구축하는 것이다. 자동차 활용 사례(Pan 등)는 하나의 템플릿을 제공하며, 의료 기기, 금융 시스템, 핵심 인프라에서도 유사한 통합 기회가 존재한다. 형식적 방법 연구자들에게 AI는 이 분야의 역사적인 도입 장벽인 비용 문제를 해결한다. LLM이 요구사항 형식화, 증명 생성, 테스트 케이스 합성을 자동화할 수 있다면, 검증에 필요한 인적 노력이 상당히 줄어들어 형식적 방법이 훨씬 더 광범위한 소프트웨어 분야에서 경제적으로 실행 가능해질 수 있다.

안전-critical 시스템을 구축하는 실무자들에게 이 메시지는, "검증되었지만 비싼" 방법과 "검증되지 않았지만 실용적인" 방법 사이의 전통적인 선택이 사라지고 있다는 것이다. AI 보조 형식적 방법은 주류 개발 예산이 감당할 수 있는 비용으로 의미 있는 정확성 보장을 제공하는 중간 경로를 제시한다.