- Kiểm chứng hình thức (formal verification) là phương pháp chứng minh bằng toán học rằng mã luôn thỏa mãn đặc tả, và trong thời gian dài đã chỉ tồn tại trong một phạm vi hạn chế mang tính nghiên cứu
- Một số hệ thống lớn như vi nhân seL4 đã được phát triển bằng kiểm chứng hình thức, nhưng do độ khó và chi phí cao nên gần như không được sử dụng trong môi trường công nghiệp
- Gần đây, các công cụ hỗ trợ lập trình dựa trên LLM không chỉ cho thấy hiệu quả với mã triển khai mà còn cả trong việc viết script chứng minh bằng nhiều ngôn ngữ, làm dấy lên khả năng thay đổi lớn cấu trúc chi phí của việc kiểm chứng
- Nếu AI có thể tự động hóa cả việc chứng minh tính đúng đắn cùng với sinh mã, thì phương thức phát triển có thể chuyển sang một mô hình đáng tin cậy hơn so với review mã bởi con người
- Việc tự động hóa kiểm chứng hình thức là công nghệ cốt lõi để bảo đảm độ tin cậy phần mềm trong kỷ nguyên AI, và yếu tố quyết định để phổ biến rộng rãi có lẽ sẽ là chuyển đổi văn hóa hơn là giới hạn kỹ thuật
Hiện trạng và giới hạn của kiểm chứng hình thức
- Các ngôn ngữ và công cụ hướng chứng minh như Rocq, Isabelle, Lean, F*, Agda cho phép chứng minh bằng toán học rằng mã thỏa mãn đặc tả
- Các ví dụ tiêu biểu gồm nhân hệ điều hành seL4, trình biên dịch C CompCert và ngăn xếp giao thức mật mã Project Everest
- Tuy nhiên, trong thực tế công nghiệp, kiểm chứng hình thức hầu như không được sử dụng
- Với seL4, việc kiểm chứng 8.700 dòng mã C cần tới 20 người-năm và 200.000 dòng mã Isabelle
- Mỗi dòng triển khai đòi hỏi 23 dòng chứng minh và nửa ngày công lao động
- Trên toàn thế giới, số chuyên gia có thể viết được các chứng minh như vậy được ước tính chỉ ở mức vài trăm người
- Xét về kinh tế, trong phần lớn hệ thống, chi phí kiểm chứng còn lớn hơn thiệt hại do lỗi gây ra, nên tính thực tiễn thấp
AI đang thay đổi tính kinh tế của kiểm chứng hình thức
- Gần đây, các trợ lý lập trình dựa trên LLM đã cho thấy kết quả không chỉ ở mã triển khai mà còn trong viết script chứng minh
- Nature, Galois, arXiv và các nguồn khác đã báo cáo các trường hợp LLM sinh chứng minh bằng nhiều ngôn ngữ
- Hiện tại vẫn cần sự hướng dẫn của chuyên gia, nhưng dự kiến tự động hóa hoàn toàn có thể khả thi trong vài năm tới
- Nếu chi phí kiểm chứng giảm mạnh, có thể áp dụng kiểm chứng hình thức cho nhiều phần mềm hơn
- Đồng thời, mã do AI sinh ra cũng cần được bảo đảm độ tin cậy bằng kiểm chứng hình thức thay vì chỉ dựa vào con người xem xét
- Nếu AI có thể tự chứng minh tính đúng đắn của mã, thì nó có thể được ưu tiên hơn cả mã viết thủ công
Tính bổ trợ lẫn nhau giữa LLM và kiểm chứng chứng minh
- Khi LLM viết script chứng minh, ngay cả nếu nó tạo ra nội dung sai lệch (hallucination), trình kiểm tra chứng minh (proof checker) sẽ từ chối
- Trình kiểm tra được cấu thành từ một lượng nhỏ mã đã được tự kiểm chứng, nên rất khó để một chứng minh sai vượt qua
- Vì vậy, tính nghiêm ngặt của kiểm chứng hình thức có thể bù đắp cho sự bất định của LLM
- Sự kết hợp này hoạt động như một con đường tự động hóa an toàn để bảo đảm độ tin cậy cho mã do AI tạo ra
Thách thức mới: độ chính xác trong định nghĩa đặc tả
- Ngay cả trong môi trường kiểm chứng tự động, việc định nghĩa đúng đặc tả (specification) vẫn là bài toán cốt lõi
- Cần xác nhận rằng thuộc tính đã được chứng minh thực sự khớp với thuộc tính mà nhà phát triển định hướng tới
- Việc viết đặc tả vẫn đòi hỏi chuyên môn và tư duy cẩn trọng, nhưng đơn giản và nhanh hơn rất nhiều so với tự viết chứng minh
- AI cũng có thể hỗ trợ dịch đặc tả giữa ngôn ngữ tự nhiên và ngôn ngữ hình thức
- Tuy vậy, vẫn tồn tại rủi ro mất mát ý nghĩa, dù được đánh giá là ở mức có thể kiểm soát
Triển vọng thay đổi phương thức phát triển phần mềm
- Nhà phát triển có thể chuyển sang mô hình mô tả các thuộc tính mong muốn của mã bằng đặc tả khai báo, còn AI sẽ cùng lúc tạo ra phần triển khai và chứng minh
- Trong trường hợp đó, nhà phát triển không cần trực tiếp rà soát mã do AI sinh ra, mà có thể sử dụng nó dựa trên niềm tin giống như cách dùng mã máy do trình biên dịch tạo ra
- Tóm lại, có thể kỳ vọng ba thay đổi sau
- Chi phí kiểm chứng hình thức giảm mạnh
- Nhu cầu kiểm chứng tăng lên để bảo đảm độ tin cậy cho mã do AI sinh ra
- Độ chính xác của kiểm chứng hình thức bù đắp cho đặc tính xác suất của LLM
- Nếu những yếu tố này kết hợp lại, kiểm chứng hình thức có khả năng cao sẽ trở thành công nghệ chủ đạo của kỹ nghệ phần mềm
- Trong tương lai, yếu tố giới hạn có lẽ sẽ không phải là công nghệ mà là tốc độ chấp nhận thay đổi của văn hóa phát triển
1 bình luận
Ý kiến trên Hacker News
Tôi nghĩ kiểm chứng hình thức (formal verification) thật sự phát huy giá trị ở những lĩnh vực mà phần triển khai phức tạp hơn đặc tả rất nhiều
Ví dụ như tối ưu hóa ở mức bit trong triển khai mật mã hoặc các giai đoạn tối ưu hóa của trình biên dịch
Nhưng phần lớn mã mà các lập trình viên (hoặc AI) viết ra hiện đã khá gần với đặc tả nhờ các ngôn ngữ bậc cao, nên tôi cho rằng lợi ích của kiểm chứng hình thức không lớn đến vậy
Cũng chưa chắc việc viết riêng đặc tả sẽ dễ đọc hơn
Ngay cả bây giờ, nhiều framework và thư viện đã trừu tượng hóa các chi tiết triển khai
Kiểm chứng hình thức có thể mang lại các đảm bảo mạnh hơn, nhưng đa số mọi người không cần mức đảm bảo như vậy, và AI có lẽ cũng sẽ không tạo ra nhu cầu mới cho điều đó
Có người dự đoán AI sẽ tự động hóa hoàn toàn kiểm chứng hình thức, nhưng tôi thấy lập luận đó có vấn đề
Nếu AI có thể tự động chứng minh phần mềm, thì cũng chẳng cần phải kiểm chứng phần mềm do con người viết nữa
Vì AI sẽ tự hình thành ý tưởng, triển khai và quyết định mức độ kiểm chứng
Cuối cùng, việc lập trình hay kiểm chứng do con người làm có khả năng sẽ biến mất
Trên thực tế, con người có thể thiết kế proof assistant, nhưng dùng nó để kiểm chứng các chương trình quy mô lớn thì khó hơn rất nhiều
Vì thế nếu loại AI đó xuất hiện, nó có lẽ cũng sẽ tự tạo ra các proof assistant mới
Tất nhiên, kiểu hình dung này gần với lĩnh vực SF hơn, và khi còn chưa rõ AI sẽ khiến việc gì dễ hơn hay khó hơn, thì các dự đoán như vậy cũng không có nhiều ý nghĩa
Liên kết thảo luận liên quan
Có cảm giác đó sẽ là bước ngoặt đưa loài người sang một giai đoạn hoàn toàn khác
Để có kết quả hữu ích từ các coding agent như Claude Code, Codex CLI, v.v., điều cốt lõi là phải chuẩn bị tốt môi trường có thể chạy và kiểm chứng mã mà chúng viết
Những ngôn ngữ dễ thực thi như Python là phù hợp nhất, còn với HTML+JS thì nên dùng công cụ như Playwright
Bước tiếp theo là bộ test tự động, rồi đến các công cụ chất lượng như code formatter, linter, fuzzer
Debugger cũng tốt, nhưng vì mang tính tương tác nên agent khó xử lý hơn
Tôi nghĩ các công cụ kiểm chứng hình thức cũng nằm trong phổ đó — vì các mô hình ngày nay cũng xử lý tốt ngôn ngữ lập trình chuyên biệt
Nếu bạn thấy coding agent không mấy hữu ích, rất có thể là do thiếu môi trường chạy và test
Lấy Haskell làm ví dụ, chỉ cần biên dịch được là gần như lúc nào cũng chạy đúng
Nếu đặc tính đó hữu ích cho con người thì với LLM cũng sẽ vậy
Đặc biệt, property test rất hợp với LLM — vì chỉ với ít test có thể bao phủ được phạm vi lỗi rộng
Nhìn vào việc cộng đồng toán học đang thử dùng LLM để cải thiện mã Lean, có vẻ phát triển phần mềm với hệ thống kiểu mạnh hơn cũng hoàn toàn khả thi
Debug không mang tính tuần tự, và thời điểm của nguyên nhân với kết quả thường bị trộn lẫn
Trước đây khi bắt bug đa luồng bằng gdb, tôi từng thử dùng ChatGPT nhưng nó chỉ lặp đi lặp lại các gợi ý đơn giản như thêm lệnh print
Cuối cùng tôi lại cảm thấy đây là lĩnh vực cần kinh nghiệm và trực giác
Bảo một kỹ sư junior làm việc mà không có debugger hay test runner thì thật vô lý
Rốt cuộc có lẽ sẽ cần nhiều tài nguyên tính toán hơn
Claude triển khai, còn Codex và Gemini review
Cách này tốn kém, nhưng là phương pháp chắc chắn nhất tôi từng thấy để giảm tự thiên vị (self-bias) và nâng chất lượng mã
Các công cụ phân tích tĩnh có thể giúp thêm, nhưng tôi cảm thấy chỉ tăng số lượng tool thôi thì chưa đủ
Khi quy trình kiểm chứng được tự động hóa, phần thực sự khó sẽ chuyển sang định nghĩa chính xác đặc tả (specification)
Viết đặc tả nhanh và dễ hơn nhiều so với tự chứng minh, nhưng vẫn đòi hỏi chuyên môn và sự cẩn trọng
Lý do kiểm chứng hình thức không phổ biến trong quá khứ không chỉ vì nó khó, mà còn vì mô hình waterfall đã biến mất và phát triển agile trở thành xu hướng chính
Thay vì viết đặc tả dài, quy trình đã tiến hóa theo hướng lặp nhanh để đáp ứng yêu cầu người dùng
Có lẽ giờ là lúc phải học OCaml
Nhiều proof assistant và hệ thống kiểm chứng có thể sinh ra mã OCaml, và ADA/Spark cũng đáng để cân nhắc
Dù kỹ nghệ phần mềm trong kỷ nguyên AI sẽ thay đổi theo cách nào đi nữa, chúng ta vẫn phải tạo ra phần mềm chất lượng cao hơn so với hiện nay
Kiểm chứng hình thức chắc chắn sẽ giúp ích cho mục tiêu đó
Dù vẫn chưa hoàn thiện, tôi chia sẻ dự án thử nghiệm của mình
Trong một thế giới thiếu các bài viết thiên về mã nguồn, nếu ai đó đang tìm một ý tưởng hackathon thú vị thì có thể tham khảo
Liên kết dự án py-mcmas
LLM có xu hướng giải tốt những bài toán dễ kiểm chứng
Vì vậy tôi chia quá trình giải quyết vấn đề thành ba bước
1️⃣ trước hết viết chương trình điều kiện thành công
2️⃣ dùng chương trình đó để kiểm chứng bài toán gốc
3️⃣ cuối cùng tự mình xác nhận lại
Cách này là hướng tiếp cận tôi đã dùng từ lâu, nhưng giờ các mô hình như Opus hay GPT-5.2 còn làm tốt ngay cả ở chế độ không giám sát
Bài blog liên quan
Ở những lĩnh vực mà việc kiểm chứng tốn nhiều thời gian, gánh nặng xác minh của con người thậm chí có thể còn tăng lên
Có thể sẽ xuất hiện câu hỏi “ai kiểm chứng chương trình kiểm chứng?”
Nếu LLM cũng viết luôn phần đó thì nó có thể trông như một tháp rùa vô tận (turtles all the way down)
Phần khó là quá trình tạo ra chứng minh
Tất nhiên với các mệnh đề phức tạp thì vẫn có ngoại lệ, nhưng nó giúp giảm bug rất nhiều
Dù kiểm chứng hình thức có trở nên phổ biến, tôi không nghĩ ai cũng sẽ dùng Lean hay Isabelle
Thay vào đó, nó có lẽ sẽ lan rộng theo dạng hòa vào quy trình làm việc hiện có một cách tự nhiên nhờ AI
Ví dụ như kiểm chứng thuộc tính trong CI, hoặc một nút “chứng minh bất biến của module này” trong IDE
Phần lớn kỹ sư có lẽ thậm chí không cần trực tiếp nhìn vào proof script
Điều thật sự khó không phải là để LLM tạo ra chứng minh, mà là khiến tổ chức chịu đầu tư để viết đặc tả và mô hình
Nếu AI khiến việc đề xuất và chỉnh sửa đặc tả trở nên dễ dàng hơn, kiểm chứng sẽ trở thành một công cụ refactor tự nhiên giống như test hay linter
Cũng có người phàn nàn rằng GPT‑5.2 còn không đếm nổi “garlic” có mấy chữ r
Nếu thực sự cần, cứ bảo LLM viết rồi chạy một đoạn script Python là được
Nó đúng thì đúng thật, nhưng chỉ là chi tiết triển khai của tokenization, gần như không liên quan đến tính hữu ích thực tế
Hầu như chẳng có lý do gì để dùng LLM cho việc đếm số chữ cái trong một từ