PDD Kit sử dụng chứng minh hình thức để xác minh mã do AI tạo ra

Microsoft Research đã ra mắt PDD Kit, một bộ công cụ mới được thiết kế nhằm đưa các phương pháp xác minh hình thức vào quy trình phát triển phần mềm hàng ngày do các tác nhân AI thúc đẩy. Được công bố vào ngày 5 tháng 11 năm 2026, cách tiếp cận này giải quyết thách thức ngày càng tăng trong việc xác thực khối lượng lớn mã được tạo ra bởi các trợ lý lập trình tự động. Bằng cách kết hợp các chứng minh toán học với kiểm thử thực nghiệm, PDD Kit hướng tới việc đảm bảo rằng các ứng dụng do tác nhân viết tuân thủ nghiêm ngặt ý định của nhà phát triển mà không cần phải xem xét từng dòng mã theo cách thủ công.

Điều gì đã xảy ra

Khi các tác nhân AI trở nên có khả năng tạo ra toàn bộ tính năng hoặc ứng dụng full-stack trong một phiên làm việc duy nhất, các quy trình xem xét mã truyền thống đang gặp khó khăn trong việc bắt kịp tốc độ. Nhà phát triển thường dựa vào các kế hoạch bằng ngôn ngữ tự nhiên như những hợp đồng cho các tác nhân này, nhưng không có cơ chế nội tại nào buộc tác nhân phải tuân theo kế hoạch một cách chính xác. Các tác nhân có thể lệch khỏi đặc tả kỹ thuật, triển khai logic hơi khác biệt và sau đó viết các bài kiểm tra vượt qua cho cách triển khai sai của chúng thay vì hành vi dự kiến. Điều này tạo ra một khoảng trống ẩn giữa những gì được yêu cầu và những gì được cung cấp, điều mà các pipeline tích hợp liên tục (CI) tiêu chuẩn thường bỏ sót vì chúng chỉ kiểm tra các trường hợp kiểm thử cụ thể.

Để giải quyết vấn đề này, Microsoft Research đã phát triển Proof-Driven Development (PDD - Phát triển dựa trên chứng minh) cùng với bộ công cụ đi kèm, PDD Kit. Hệ thống này tích hợp với môi trường lập kế hoạch Chopin của GitHub Next để biến đổi ý định của người dùng thành các đặc tả kỹ thuật hình thức. Sau đó, nó sử dụng các đặc tả này để chứng minh về mặt toán học rằng mã được tạo ra là đúng đắn cho mọi đầu vào có thể. Đối với các khía cạnh của phần mềm không thể được chứng minh hình thức, chẳng hạn như tương tác với các thư viện bên thứ ba hoặc giao diện người dùng, bộ công cụ sẽ quay lại sử dụng các bài kiểm tra thực nghiệm chất lượng cao. Cách tiếp cận lai này cho phép các kỹ sư không có nền tảng về phương pháp hình thức vẫn có thể áp dụng quy trình xác minh chặt chẽ cho các dự án của họ.

Nhóm nghiên cứu đã minh họa PDD Kit bằng cách xây dựng Pet Store, một ứng dụng web full-stack được viết bằng Rust. Ứng dụng bao gồm backend sử dụng Axum và SQLite, và frontend được xây dựng với Leptos biên dịch sang WebAssembly. Mặc dù toàn bộ ứng dụng gồm khoảng 5.000 dòng mã, nhóm tập trung nỗ lực xác minh hình thức vào logic đăng nhập. Thành phần quan trọng này xử lý xác thực và ủy quyền, khiến nó trở thành ứng viên lý tưởng cho việc xác minh dựa trên chứng minh. Quy trình này cho phép nhà phát triển xem xét ý định và đặc tả kỹ thuật mà không cần đọc từng dòng mã được tạo ra, nhưng vẫn đạt được mức độ tin cậy cao về tính bảo mật và độ chính xác của luồng đăng nhập.

Cách hoạt động

PDD Kit hoạt động bằng cách thu hẹp khoảng cách giữa ý định bằng ngôn ngữ tự nhiên và các đặc tả kỹ thuật toán học hình thức. Khi nhà phát triển đưa ra một yêu cầu, bộ công cụ sẽ đặt các câu hỏi làm rõ để giải quyết sự mơ hồ, chẳng hạn như phân biệt giữa "chỉ lấy token khi có mật khẩu đúng" và "mật khẩu đúng luôn hoạt động". Những quyết định này được ghi lại trong một tài liệu ý định (intent artifact), ánh xạ các yêu cầu của người dùng sang các đặc tả kỹ thuật hình thức trong Verus, một ngôn ngữ chứng minh dành cho Rust. Bộ công cụ sau đó tạo ra các chứng minh rằng mã thỏa mãn các đặc tả này cho tất cả các đầu vào, đồng thời tạo ra các bài kiểm tra cho những phần của hệ thống nằm ngoài phạm vi xác minh hình thức, được gọi là Trusted Computing Base (Cơ sở điện toán tin cậy).

Quy trình xác minh phân biệt giữa hai loại đảm bảo: xác minh hình thức và xác minh thực nghiệm. Xác minh hình thức sử dụng trình xác minh Verus để cung cấp một chứng minh toán học rằng mã đáp ứng đặc tả kỹ thuật của nó cho mọi đầu vào có thể. Mặt khác, xác minh thực nghiệm dựa vào việc chạy mã và quan sát hành vi của nó thông qua các bài kiểm tra đơn vị (unit tests), kiểm thử end-to-end và các tác nhân trình duyệt. PDD Kit làm cho ranh giới giữa hai loại này trở nên rõ ràng, yêu cầu nhà phát triển phê duyệt từng thành phần tin cậy, chẳng hạn như các thư viện mã hóa bên ngoài hoặc truy vấn cơ sở dữ liệu, đảm bảo rằng các giả định đằng sau các chứng minh được hiểu rõ và chấp nhận.

Chi tiết chính

• PDD Kit tích hợp với môi trường Chopin của GitHub Next để hỗ trợ lập kế hoạch và xác minh theo thời gian thực, đa người dùng.
• Bộ công cụ sử dụng Verus, một ngôn ngữ chứng minh dành cho Rust, để tạo ra các chứng minh toán học rằng mã thỏa mãn các đặc tả kỹ thuật hình thức cho mọi đầu vào.
• Nó tự động chuyển đổi các phần của ý định người dùng không thể được chứng minh hình thức thành các đặc tả kỹ thuật không chính thức được bao phủ bởi các bài kiểm tra thực nghiệm.
• Hệ thống xác định rõ ràng Trusted Computing Base, yêu cầu nhà phát triển phê duyệt các phụ thuộc bên ngoài và các hành vi được giả định.
• Trong bản demo Pet Store, PDD Kit đã xác minh logic đăng nhập của một ứng dụng Rust dài 5.000 dòng, phát hiện các lỗi tồn tại trước đó và chứng minh sự vắng mặt của các lỗi đăng nhập so với đặc tả kỹ thuật.
• Quy trình làm việc bao gồm một bản đồ ý định liên kết các yêu cầu với các đặc tả kỹ thuật hình thức và bài kiểm tra, cung cấp một dấu vết kiểm toán rõ ràng về cách ý định người dùng được triển khai.

Tại sao điều này quan trọng

Đối với các kỹ sư phần mềm và trưởng nhóm kỹ thuật, PDD Kit cung cấp một giải pháp có khả năng mở rộng cho cuộc khủng hoảng độ tin cậy do mã được tạo bởi AI gây ra. Khi các tác nhân tạo ra các codebase lớn hơn và phức tạp hơn, chi phí của việc xem xét thủ công trở nên quá cao, và các chiến lược kiểm thử truyền thống để lại những khoảng trống đáng kể trong phạm vi bao phủ. Bằng cách tự động hóa việc tạo ra các chứng minh hình thức, PDD Kit cung cấp mức độ đảm bảo mà chỉ riêng việc kiểm thử không thể sánh kịp, bắt được các trường hợp biên (edge cases) và lỗi logic mà nếu không sẽ lọt vào môi trường sản xuất. Điều này chuyển đổi vai trò của nhà phát triển từ người xem xét từng dòng mã thành một kiến trúc sư cấp cao, người định nghĩa ý định và xác thực các đặc tả kỹ thuật.

Hơn nữa, cách tiếp cận này dân chủ hóa các phương pháp hình thức, vốn trước đây chỉ dành cho các hệ thống ngách, an toàn-critical (safety-critical) do độ phức tạp và chi phí của chúng. Bằng cách tận dụng AI để xử lý phần nặng nề của việc tạo chứng minh và viết đặc tả kỹ thuật, PDD Kit làm cho các kỹ thuật chặt chẽ này trở nên dễ tiếp cận đối với việc phát triển ứng dụng hàng ngày. Điều này có thể dẫn đến một tiêu chuẩn mới về chất lượng phần mềm, nơi các thành phần quan trọng như xác thực, giao dịch tài chính và xử lý dữ liệu được xác minh thường xuyên bằng toán học, giảm thiểu rủi ro của các lỗi nghiêm trọng và lỗ hổng bảo mật.

Bạn có thể làm gì

• Đánh giá các quy trình xem xét mã hiện tại của bạn để xác định các nút thắt cổ chai gây ra bởi các pull request lớn do AI tạo ra.
• Xác định các thành phần quan trọng trong ứng dụng của bạn, chẳng hạn như logic xác thực hoặc thanh toán, sẽ hưởng lợi nhiều nhất từ xác minh hình thức.
• Khám phá các khả năng của Verus và các công cụ xác minh hình thức khác dành cho Rust để hiểu tiềm năng tích hợp chúng vào quy trình làm việc của bạn.
• Thử nghiệm với việc chỉ định các yêu cầu rõ ràng, không mơ hồ cho các tác nhân AI để giảm khả năng lệch khỏi triển khai dự kiến.
• Cân nhắc áp dụng chiến lược kiểm thử lai kết hợp các bài kiểm tra đơn vị truyền thống với kiểm thử dựa trên thuộc tính (property-based testing) để bao phủ nhiều kịch bản đầu vào hơn.
• Cập nhật thông tin về các tiến bộ trong Proof-Driven Development và các công cụ như PDD Kit khi chúng trở nên phổ biến hơn.