GitHub PDD Kit: 5 bước chứng minh mã Rust do AI tạo ra và 3 giới hạn cần biết

GitHub Next và Microsoft Research đã giới thiệu Proof-Driven Development Kit, viết tắt là PDD Kit, dưới dạng bản xem trước dành cho nghiên cứu. Công cụ này hướng đến một câu hỏi ngày càng quan trọng trong thời đại lập trình bằng AI: Làm thế nào để biết mã nguồn do tác nhân AI tạo ra thực sự đáp ứng yêu cầu?

Thay vì chỉ yêu cầu kỹ sư đọc từng dòng mã hoặc chạy một bộ kiểm thử hữu hạn, PDD Kit đưa ra một hướng tiếp cận khác: con người phê duyệt đặc tả chính thức, còn trình kiểm chứng tự động chứng minh rằng mã nguồn tuân thủ đặc tả đó với mọi đầu vào nằm trong phạm vi mô hình.

Đây là một ý tưởng đáng chú ý đối với các nhóm đang sử dụng coding agent. Tuy nhiên, PDD Kit không phải là “nút bấm chứng minh mọi phần mềm đều đúng”. Công cụ hiện tập trung vào Rust, phụ thuộc vào khả năng diễn đạt của đặc tả và vẫn cần kiểm thử hoặc con người xử lý những phần không thể chứng minh hình thức.

Mục lục

PDD Kit là gì?

Proof-Driven Development Kit là quy trình phát triển phần mềm kết hợp giữa lập kế hoạch có AI, đặc tả hình thức và kiểm chứng chương trình. Theo cách GitHub Next mô tả, mục tiêu của quy trình là chuyển trọng tâm tin cậy từ:

“Con người đã đọc kỹ toàn bộ phần thay đổi chưa?”
Sang: “Mã nguồn có được kiểm chứng dựa trên đặc tả đã được phê duyệt hay không?”

PDD Kit sử dụng Verus, một framework mã nguồn mở dùng để chứng minh tính đúng đắn của chương trình Rust. Verus cho phép nhà phát triển mô tả điều kiện đầu vào, kết quả đầu ra, bất biến và các thuộc tính cần duy trì trong quá trình thực thi.

Điểm quan trọng là PDD Kit không loại bỏ vai trò của con người. Con người vẫn phải xác định hoặc phê duyệt điều hệ thống cần làm. AI và trình kiểm chứng hỗ trợ viết mã, tạo chứng minh và phát hiện sự không phù hợp giữa triển khai với yêu cầu.

Quy trình PDD Kit gồm 5 bước

Trong ví dụ về một luồng đăng nhập, GitHub Next mô tả quy trình PDD Kit qua năm giai đoạn chính.

1. Lập kế hoạch tính năng

Nhóm phát triển bắt đầu bằng việc xác định tính năng, phạm vi thay đổi và các yêu cầu liên quan. Giai đoạn này được thực hiện trong Chopin, môi trường lập kế hoạch cộng tác có tích hợp tác nhân AI của GitHub Next.

Mục tiêu của bước lập kế hoạch không chỉ là tạo danh sách công việc. Nhóm cần làm rõ:

Tính năng phải giải quyết vấn đề gì?
Đầu vào hợp lệ và không hợp lệ là gì?
Kết quả mong đợi trong từng trường hợp?
Có giới hạn bảo mật, hiệu năng hoặc trạng thái nào cần duy trì?

Đây là nền tảng cho các bước đặc tả và kiểm chứng về sau. Nếu yêu cầu ban đầu mơ hồ, việc tạo ra một chứng minh chính xác cũng sẽ trở nên khó khăn.

2. Tạo đặc tả hình thức

Sau khi hiểu mục tiêu của tính năng, PDD Kit phân tích mã nguồn và yêu cầu để đề xuất một đặc tả hình thức bằng Verus.

Đặc tả hình thức mô tả hành vi cần được bảo đảm bằng các điều kiện có thể kiểm tra về mặt logic. Ví dụ, thay vì viết yêu cầu chung chung như “giới hạn số lần đăng nhập thất bại”, đặc tả có thể nói rõ rằng thao tác chỉ được phép khi số lần thất bại nhỏ hơn một ngưỡng nhất định.

Một ví dụ đơn giản bằng Verus có thể có dạng:

verus! {
    spec fn max_attempts() -> nat {
        5
    }

    fn check_attempt(failed: nat) -> (allowed: bool)
        ensures allowed == (failed < max_attempts())
    {
        failed < max_attempts()
    }
}

Trong ví dụ này, điều kiện ensures mô tả kết quả mà hàm phải trả về. Trình kiểm chứng không chỉ chạy hàm với một vài giá trị mẫu. Nó cố gắng chứng minh quan hệ giữa đầu vào và đầu ra đúng với mọi giá trị phù hợp với mô hình.

3. Con người phê duyệt đặc tả

Đây là điểm thay đổi đáng kể so với quy trình review mã truyền thống. Người phụ trách không nhất thiết phải đọc từng dòng mã do agent tạo ra trước tiên. Thay vào đó, họ xem xét đặc tả: liệu đặc tả có phản ánh đúng yêu cầu nghiệp vụ và yêu cầu kỹ thuật hay không?

Việc phê duyệt đặc tả cần trả lời các câu hỏi như:

Đặc tả có bỏ sót trường hợp biên nào không?
Điều kiện đầu vào có được mô tả đầy đủ không?
Đặc tả có vô tình cho phép hành vi không an toàn không?
Thuộc tính được chứng minh có thực sự tương ứng với điều doanh nghiệp cần không?

Một chương trình có thể được chứng minh hoàn toàn đúng theo một đặc tả sai. Vì vậy, đặc tả đúng quan trọng không kém việc chứng minh mã nguồn đúng theo đặc tả đó.

4. Tự động chứng minh mã nguồn

Sau khi đặc tả được chấp thuận, trình kiểm chứng Verus phân tích mã Rust do agent tạo ra. Mục tiêu là chứng minh rằng triển khai thực tế đáp ứng các tiền điều kiện, hậu điều kiện và bất biến đã được mô tả.

Kiểm thử thông thường chỉ kiểm tra một tập hợp đầu vào cụ thể. Trong khi đó, kiểm chứng hình thức tìm cách chứng minh mệnh đề tổng quát trong phạm vi mô hình được định nghĩa.

Ví dụ:

Kiểm thử có thể xác nhận hàm hoạt động với các giá trị 0, 1, 4 và 5.
Chứng minh hình thức có thể xác nhận thuộc tính tương ứng với mọi giá trị tự nhiên mà hệ thống xem xét.

Tuy nhiên, điều này không có nghĩa toàn bộ phần mềm được chứng minh “đúng tuyệt đối”. Kết quả chỉ có ý nghĩa trong phạm vi:

Đặc tả đã viết.
Mô hình hệ thống được sử dụng.
Các giả định mà trình kiểm chứng chấp nhận.
Phần mã thực sự nằm trong phạm vi kiểm chứng.

5. Chuyển sang kiểm thử khi không thể chứng minh

Không phải mọi loại mã đều dễ biểu diễn bằng logic hình thức. Khi không thể hoàn tất chứng minh, PDD Kit có thể chuyển sang cơ chế dự phòng gồm kiểm thử và các tác nhân sử dụng máy tính để kiểm tra hành vi thực tế.

Điều này đặc biệt quan trọng với những phần mềm có nhiều tương tác bên ngoài như:

Giao diện người dùng.
Luồng thao tác trình duyệt.
Tích hợp API bên thứ ba.
Hệ thống tệp và mạng.
Hành vi phụ thuộc vào môi trường triển khai.

Bước dự phòng này cho thấy PDD Kit không thay thế toàn bộ quy trình đảm bảo chất lượng. Nó bổ sung một lớp chứng minh mạnh hơn cho những phần có thể đặc tả chính xác, còn các phần khác vẫn cần kiểm thử và review.

Verus chứng minh điều gì?

Verus là framework kiểm chứng chương trình dành cho Rust. Nhà phát triển có thể dùng nó để mô tả các thuộc tính toán học hoặc logic mà chương trình phải duy trì.

Một số loại thuộc tính phù hợp với kiểm chứng hình thức gồm:

Quan hệ giữa đầu vào và đầu ra.
Giới hạn giá trị.
Bất biến của cấu trúc dữ liệu.
Điều kiện trước và sau khi gọi hàm.
Chuyển đổi trạng thái trong state machine.
Tính đúng đắn của thuật toán thuần.
Không truy cập dữ liệu ngoài phạm vi cho phép trong mô hình.

Ví dụ, với một hàng đợi, đặc tả có thể yêu cầu rằng số phần tử không bao giờ âm, thao tác lấy phần tử không làm thay đổi sai lệch thứ tự và phần tử được lấy ra phải là phần tử đã được đưa vào trước đó.

Ngược lại, những phát biểu như “giao diện dễ sử dụng”, “trải nghiệm đăng nhập tự nhiên” hoặc “thời gian phản hồi đủ nhanh trong điều kiện thực tế” cần được chuyển thành các chỉ số cụ thể mới có thể kiểm chứng một phần. Nếu không, chúng thường vẫn cần đánh giá thủ công và kiểm thử thực nghiệm.

Vì sao kiểm chứng hình thức khác với kiểm thử?

Kiểm thử và kiểm chứng hình thức không phải hai cách gọi cho cùng một hoạt động.

Tiêu chí	Kiểm thử	Kiểm chứng hình thức
Cách hoạt động	Chạy chương trình với các trường hợp cụ thể	Chứng minh thuộc tính dựa trên mô hình logic
Phạm vi đầu vào	Một tập hợp đầu vào được lựa chọn	Có thể bao quát miền đầu vào trong đặc tả
Phát hiện lỗi	Cho thấy chương trình sai trong trường hợp đã thử	Chứng minh hoặc bác bỏ một thuộc tính được mô tả
Điều kiện cần thiết	Test case và môi trường chạy	Đặc tả, mô hình và quy tắc chứng minh

Một bộ kiểm thử xanh không chứng minh rằng không còn lỗi. Ngược lại, một chứng minh thành công cũng không bảo đảm yêu cầu nghiệp vụ ban đầu là đúng hoặc hệ thống ngoài phạm vi mô hình không có vấn đề.

Nền tảng nghiên cứu phía sau PDD Kit

PDD Kit không xây dựng toàn bộ công nghệ từ con số không. Nó dựa trên Verus và những nghiên cứu trước đó về việc dùng mô hình ngôn ngữ để tạo hoặc sửa chứng minh chương trình.

Kho mã verus-proof-synthesis của Microsoft Research đề cập đến các hệ thống như AutoVerus và VeruSAGE. Những hệ thống này nghiên cứu cách sử dụng LLM để hỗ trợ sinh chứng minh Verus và khắc phục các chứng minh chưa hoàn chỉnh.

Theo thông tin được công bố, các hệ thống nghiên cứu đã được đánh giá trên những tập nhiệm vụ kiểm chứng có quy mô khác nhau, lần lượt khoảng 150 và 849 bài toán. PDD Kit có thể được xem là bước đóng gói những hướng nghiên cứu đó thành quy trình gần với hoạt động phát triển phần mềm thực tế hơn:

Lập kế hoạch tính năng.
Đề xuất đặc tả.
Con người xem xét yêu cầu.
Agent tạo mã và chứng minh.
Tạo pull request có bằng chứng kiểm chứng.

Dù vậy, kết quả nghiên cứu và bản preview không nên được hiểu là bằng chứng cho khả năng áp dụng rộng rãi trong mọi dự án sản xuất. Cần thêm đánh giá độc lập về độ chính xác, chi phí, khả năng mở rộng và tỷ lệ thất bại trong các codebase phức tạp.

Ba giới hạn lớn của PDD Kit

1. Hiện tập trung vào Rust

Giới hạn rõ ràng nhất là phạm vi ngôn ngữ. Verus kiểm tra chương trình Rust, vì vậy PDD Kit hiện phù hợp nhất với các nhóm đang phát triển thư viện, dịch vụ hoặc thành phần hệ thống bằng Rust.

Nếu coding agent của bạn chủ yếu tạo mã TypeScript, Python, Java, Go hoặc C#, PDD Kit chưa thể trực tiếp cung cấp cùng mức kiểm chứng. Các ngôn ngữ đó vẫn cần dựa vào test, static analysis, type checker, fuzzing, review và các kỹ thuật bảo đảm chất lượng khác.

Điều này không làm giảm giá trị của hướng tiếp cận, nhưng cho thấy PDD Kit chưa phải giải pháp phổ quát cho mọi quy trình phát triển phần mềm bằng AI.

2. Chỉ chứng minh được điều có thể đặc tả chính xác

Kiểm chứng hình thức không thể tự quyết định “đúng” nghĩa là gì. Nó chỉ có thể kiểm tra một mệnh đề đã được diễn đạt đủ rõ ràng.

Những phần thường phù hợp gồm thuật toán, parser, cấu trúc dữ liệu, bộ điều phối trạng thái và các hàm thuần. Trong khi đó, những phần khó hơn thường liên quan đến:

Hành vi giao diện.
Khả năng sử dụng.
Phụ thuộc mạng hoặc dịch vụ bên ngoài.
Quy tắc nghiệp vụ chưa được định nghĩa rõ.
Hiệu năng dưới tải thực tế.
Hành vi phát sinh từ nhiều hệ thống kết hợp.

Do đó, PDD Kit có thể giảm khối lượng review thủ công cho một nhóm mã nhất định, nhưng không thể loại bỏ hoàn toàn review, kiểm thử tích hợp hoặc kiểm thử chấp nhận người dùng.

3. Vẫn đang ở giai đoạn nghiên cứu

PDD Kit được công bố dưới dạng research preview. Điều đó có nghĩa tính năng, giao diện, khả năng tích hợp và phạm vi hỗ trợ vẫn có thể thay đổi.

Chopin, môi trường lập kế hoạch liên quan đến quy trình này, cũng được GitHub Next giới thiệu như một nguyên mẫu nghiên cứu. Các dự án thử nghiệm của GitHub Next có thể cung cấp góc nhìn quan trọng về tương lai phát triển phần mềm, nhưng không phải dự án nào cũng trở thành sản phẩm thương mại khả dụng rộng rãi.

Vì vậy, doanh nghiệp không nên ngay lập tức xây dựng toàn bộ quy trình phát hành quanh PDD Kit. Cách thận trọng hơn là thử nghiệm trên một thành phần nhỏ, đo lường chi phí và xác định những loại mã thực sự hưởng lợi từ kiểm chứng hình thức.

PDD Kit có thay thế code review không?

Câu trả lời ngắn gọn là không hoàn toàn.

PDD Kit có thể thay đổi thứ tự và trọng tâm của review. Thay vì để kỹ sư phải đọc toàn bộ diff do AI tạo ra, nhóm có thể tập trung trước vào đặc tả, các giả định và phạm vi chứng minh. Khi mã đã vượt qua kiểm chứng, phần review thủ công có thể dành nhiều thời gian hơn cho:

Tính phù hợp với kiến trúc tổng thể.
Rủi ro bảo mật ngoài đặc tả.
Khả năng vận hành và giám sát.
Ảnh hưởng đến dữ liệu và quyền riêng tư.
Chất lượng trải nghiệm người dùng.
Các phần mã không thể kiểm chứng hình thức.

Đặc tả sai vẫn có thể dẫn đến mã sai nhưng được chứng minh thành công. Vì vậy, review yêu cầu và review đặc tả có thể trở thành nhiệm vụ quan trọng hơn trước.

Ứng dụng thực tế cho quy tắc của coding agent

Đối với các nhóm đang dùng AI coding agent, bài học quan trọng không phải là chờ PDD Kit phát hành chính thức. Bài học là cần phân loại công việc theo loại bằng chứng có thể thu thập.

Nhóm có khả năng kiểm chứng cao

Hàm xử lý dữ liệu thuần.
Parser và bộ kiểm tra cú pháp.
Thuật toán tìm kiếm, sắp xếp hoặc biến đổi dữ liệu.
State machine.
Logic giới hạn quyền truy cập.
Cấu trúc dữ liệu có bất biến rõ ràng.

Nhóm cần kết hợp nhiều phương pháp

API có phụ thuộc cơ sở dữ liệu.
Luồng xác thực và phân quyền.
Ứng dụng web có nhiều tích hợp.
Giao diện người dùng.
Tác vụ nền và hệ thống phân tán.
Quy trình triển khai, giám sát và khôi phục sự cố.

Trong file quy tắc của agent, nhóm phát triển nên quy định rõ bằng chứng cần có trước khi hoàn thành một nhiệm vụ:

# Ví dụ quy tắc cho coding agent

- Phải mô tả yêu cầu đầu vào và đầu ra trước khi triển khai.
- Với hàm thuần, phải bổ sung test cho trường hợp biên.
- Với mã Rust phù hợp, cần đánh giá khả năng viết đặc tả Verus.
- Không tuyên bố hoàn thành nếu chưa chạy formatter, lint và test.
- Mọi giả định chưa được kiểm chứng phải được ghi rõ trong pull request.
- Không dùng câu "đã hoạt động" thay cho bằng chứng kiểm tra cụ thể.

Nên chuẩn bị gì trước khi PDD Kit được phát hành rộng rãi?

1. Phân loại codebase

Hãy lập danh sách các thành phần có thể đặc tả rõ bằng đầu vào, đầu ra và bất biến. Đồng thời, đánh dấu những thành phần phụ thuộc vào giao diện, mạng, con người hoặc môi trường bên ngoài.

Việc phân loại này hữu ích ngay cả khi bạn chưa sử dụng Verus. Nó giúp nhóm biết phần nào có thể tự động hóa và phần nào cần đầu tư vào test hoặc review.

2. Thử Verus độc lập

Verus là dự án mã nguồn mở và có thể được nghiên cứu độc lập với PDD Kit. Hãy bắt đầu bằng một hàm Rust nhỏ, ít phụ thuộc và có yêu cầu rõ ràng.

Mục tiêu của thử nghiệm ban đầu không phải chứng minh toàn bộ ứng dụng. Bạn cần hiểu:

Đặc tả mất bao nhiêu thời gian để viết?
Agent có tạo được chứng minh đáng tin cậy không?
Những lỗi nào thường khiến chứng minh thất bại?
Chi phí bảo trì đặc tả khi mã thay đổi là bao nhiêu?

3. Định nghĩa “hoàn thành” trước khi agent bắt đầu

Agent không thể tự suy đoán chính xác tiêu chí chấp nhận nếu nhóm không cung cấp yêu cầu rõ ràng. Mỗi nhiệm vụ nên có danh sách bằng chứng cụ thể, chẳng hạn:

Test đơn vị đã chạy thành công.
Test tích hợp đã hoàn tất.
Lint và kiểm tra kiểu không còn lỗi.
Đặc tả đã được review.
Chứng minh hình thức đã hoàn tất nếu thuộc phạm vi áp dụng.
Các giới hạn và giả định đã được ghi trong pull request.

Các nguồn tham khảo đáng chú ý

Để tìm hiểu sâu hơn về công nghệ và bối cảnh nghiên cứu, bạn có thể tham khảo:

GitHub Next Projects – danh sách các dự án và nguyên mẫu nghiên cứu của GitHub Next.
Microsoft Research Verus Proof Synthesis – mã nguồn và tài liệu liên quan đến nghiên cứu sinh chứng minh Verus.
Verus trên GitHub – framework kiểm chứng chương trình Rust mã nguồn mở.
Tài liệu Verus – hướng dẫn về đặc tả và kiểm chứng chương trình bằng Verus.

Kết luận: bằng chứng mạnh hơn, nhưng không phải bằng chứng cho mọi thứ

PDD Kit đại diện cho một hướng phát triển đáng chú ý của phần mềm do AI tạo ra: thay vì chỉ đánh giá agent bằng tốc độ viết mã, nhóm phát triển có thể yêu cầu bằng chứng rằng mã đáp ứng các thuộc tính đã được định nghĩa.

Quy trình gồm năm bước — lập kế hoạch, tạo đặc tả, con người phê duyệt, tự động chứng minh và chuyển sang kiểm thử khi cần — có thể giúp giảm áp lực review đối với những phần mã phù hợp với kiểm chứng hình thức.

Tuy nhiên, ba giới hạn cần luôn được ghi nhớ: PDD Kit hiện tập trung vào Rust, chỉ chứng minh được những gì có thể diễn đạt chính xác và vẫn đang ở giai đoạn nghiên cứu. Đặc tả không thay thế yêu cầu nghiệp vụ; chứng minh không thay thế kiểm thử; còn agent không thể thay thế trách nhiệm của đội ngũ phát triển.

Cách tiếp cận thực tế nhất là kết hợp các phương pháp: dùng đặc tả và kiểm chứng cho logic có thể chứng minh, dùng test cho hành vi có thể quan sát, dùng review cho kiến trúc và rủi ro, đồng thời quy định rõ tiêu chí hoàn thành trong cấu hình của coding agent.

GitHub PDD Kit: 5 bước chứng minh mã Rust do AI tạo ra và 3 giới hạn cần biết

PDD Kit là gì?