TLA+ kiểm tra được gì và không kiểm tra được gì?

Gần đây, sau khi Boris Cherny — cha đẻ của Claude Code — tiết lộ rằng Opus có thể dùng TLA+ để tìm ra các lỗi tranh chấp (race condition) trong mã nguồn, cả cộng đồng mạng bắt đầu bàn tán về kiểm chứng hình thức (formal verification). Là người ủng hộ TLA+ lâu năm, tác giả Hillel Wayne vừa mừng vừa lo: TLA+ rất giỏi thiết kế hệ thống đồng thời phức tạp, nhưng kỳ vọng rằng phương pháp hình thức sẽ giải quyết triệt để vấn đề phát triển phần mềm bằng AI là một ngộ nhận nguy hiểm.

Bài viết này tập trung vào một giới hạn ít được nhắc tới: để kiểm chứng một thuộc tính, trước tiên ta phải diễn đạt được thuộc tính đó. Vậy TLA+ không thể diễn đạt những loại thuộc tính nào?

TLA+ kiểm tra được gì?

TLA+ chia hệ thống thành một tập hợp các hành vi (behavior). Mỗi hành vi là một chuỗi trạng thái, ví dụ "đèn 1 xanh, rồi vàng, rồi đỏ". Trong mỗi trạng thái, ta có thể viết các biểu thức boolean thông thường như Light4 = "green" hay AllLights = "red". Ta cũng có thể kết hợp thêm ba toán tử logic thời gian (temporal):

• []P ("luôn luôn P"): đúng nếu P đúng ở trạng thái hiện tại và mọi trạng thái tương lai. Ví dụ: [](at_most_one_green) đúng nếu mọi trạng thái đều có không quá một đèn xanh.
• P' ("P phẩy"): đúng nếu P đúng ở trạng thái kế tiếp. Ví dụ: light = "green" && light' = "red".
• <>P ("cuối cùng P"): đúng nếu P đúng ở hiện tại hoặc ít nhất một trạng thái tương lai.

Khi nói P là một thuộc tính của hệ thống, nghĩa là P đúng ở trạng thái khởi tạo của mọi hành vi. Kiểm tra []P tương đương với việc P đúng ở mọi trạng thái của mọi hành vi — gọi là bất biến (invariant), một trong những thuộc tính nền tảng nhất của TLA+.

Kết hợp [] với ' cho ta thuộc tính hành động (action property), ví dụ [](x' >= x) — giá trị mới của x luôn lớn hơn hoặc bằng giá trị cũ. Hay [](P => P') — một khi P đúng thì không bao giờ sai trở lại. Cả bất biến lẫn thuộc tính hành động đều là thuộc tính an toàn (safety), nghĩa là "điều xấu không bao giờ xảy ra".

Liveness (tính sống) là "điều tốt luôn xảy ra". <>P đơn thuần thường quá yếu để làm thuộc tính hệ thống, nhưng kết hợp lại thì rất hữu ích:

• []<>P: ở mọi thời điểm, P sẽ đúng ở một tương lai nào đó. Dùng để mô hình hóa cơ chế phục hồi, ví dụ "nếu các nút bầu lại lãnh đạo, cuối cùng chúng sẽ thống nhất".
• <>[]P: tại một thời điểm nào đó P trở thành đúng và giữ nguyên mãi mãi. Dùng để chứng minh thuật toán kết thúc với kết quả đúng.
• [](P => <>Q), viết gọn là P ~> Q: mọi trạng thái mà P đúng thì sẽ có tương lai Q đúng.

Ngoài ra còn các toán tử như ENABLED và >_v mở ra nhiều thủ thuật khác, cùng với tinh chỉnh (refinement) — sự kết hợp giữa safety và liveness. Nhưng phần lớn những gì ta kiểm tra vẫn là bất biến, thuộc tính hành động và liveness.

TLA+ không làm được gì?

Đầu tiên là điều hiển nhiên: nếu bạn không biết cách biểu diễn thuộc tính dưới dạng công thức logic, TLA+ không giúp được gì. Không một phương pháp hình thức nào có thể làm điều đó. Nếu bạn không hình thức hóa được khái niệm "con chim", bạn không thể chứng minh ứng dụng của mình nhận diện được chim. Rất tiếc, nhiều thuộc tính quan trọng mà ta quan tâm lại rơi vào nhóm này.

Tiếp theo là những thuộc tính quá cụ thể. Thuộc tính an toàn của TLA+ hoạt động ở cấp độ từng trạng thái (bất biến) hoặc từng bước (thuộc tính hành động). Bạn không thể định nghĩa thuộc tính trải qua hai bước trở lên, ví dụ "nhấn delete rồi undo sẽ trả về trạng thái ban đầu", hay "sau khi nhấn nút nguồn, máy tính khởi động trong vòng mười bước". TLA+ cũng không định nghĩa được thuộc tính trên phép toán số thực dấu phẩy động hay theo thời gian thực — chỉ theo thời gian logic.

Giới hạn thú vị nhất: thuộc tính của TLA+ được lượng hóa ngầm trên mọi hành vi. Khi nói []P nghĩa là P đúng ở mọi trạng thái, thực chất là "với mọi hành vi, []P đúng tại trạng thái khởi tạo của hành vi đó". Nghĩa là mọi thuộc tính TLA+ kiểm tra được đều phải đúng cho từng hành vi riêng lẻ.

Điều đó loại trừ những gì? Nhiều hơn bạn tưởng!

Thuộc tính khả năng đạt tới (reachability)

TLA+ không diễn đạt được "tồn tại một hành vi mà P đúng". Nghĩa là ta không thể nói P có thể xảy ra, kể cả khi thực tế chưa bao giờ chạm tới. Ví dụ điển hình: chứng minh một trò chơi có thể thắng. Các thuộc tính mở rộng hơn như "P có thể đạt tới từ mọi trạng thái khởi tạo" hay "P có thể đạt tới từ mọi trạng thái mà Q đúng" cũng nằm ngoài tầm với.

Hyperproperty

TLA+ cũng không định nghĩa được thuộc tính trên một tập hợp các hành vi. Giả sử bạn mô hình hóa phần cứng điện thoại và muốn xác minh chế độ tiết kiệm năng lượng luôn dùng ít điện hơn chế độ thường. Thuộc tính là "mọi chuỗi hành động đều tiêu thụ ít điện hơn ở chế độ tiết kiệm". Để phản bác, bạn phải đưa ra hai hành vi giống hệt nhau, chỉ khác ở chế độ khởi tạo. Một hành vi đơn lẻ không đủ, nên TLA+ không thể tự nhiên kiểm tra được loại thuộc tính này.

Hyperproperty nghe có vẻ hẹp, nhưng thực tế bao trùm rất nhiều thuộc tính bảo mật và mọi thuộc tính thống kê (ví dụ "thời gian phản hồi phân vị 95 là 5ms").

Thuộc tính trên toàn bộ không gian trạng thái

Cuối cùng, mang tính học thuật hơn, TLA+ không định nghĩa được thuộc tính trên toàn bộ không gian trạng thái. Ta không thể nói chỉ có duy nhất một đường đi từ trạng thái X tới Y. Loại "siêu thuộc tính" này có tiềm năng ý nghĩa, nhưng chưa rõ ứng dụng thực tế cụ thể ra sao.

Những "thủ thuật" để TLA+ làm được

Thực ra nói TLA+ "không làm được" là hơi đơn giản hóa. Ý tác giả là: nếu bạn viết một đặc tả (spec) tương ứng trực tiếp với hệ thống muốn xây dựng, thì TLA+ không diễn đạt được những thuộc tính này như thuộc tính của hệ thống đó. Nhưng bạn có thể mô phỏng:

• Thuộc tính hai bước có thể mô phỏng bằng biến phụ trợ (auxiliary variable), ví dụ lưu mọi thay đổi trạng thái vào một chuỗi state_history rồi định nghĩa thuộc tính như bất biến trên chuỗi đó.
• Một số hyperproperty có thể mô phỏng bằng tự hợp thành (self-composition), trong đó mỗi hành vi của spec tự hợp thành là hai hành vi của hệ thống thật.
• Trình kiểm tra mô hình chính của TLA+ (TLC) có thể kiểm tra các thuộc tính reachability cơ bản nhất với từ khóa REACHABLE mới, và một số thuộc tính không gian trạng thái với TLCGet.

Đây là những thủ thuật hữu ích nhưng vẫn là thủ thuật. Mỗi cái đòi hỏi nhiều sự khéo léo và đi kèm hạn chế nghiêm trọng: biến phụ trợ phá vỡ khả năng tinh chỉnh, tự hợp thành làm nổ không gian trạng thái theo cấp số nhân. Chúng không kết hợp tốt với các tính năng khác của TLA+ và khiến mô hình trở nên kỳ dị, lộn xộn, không còn tương ứng với hệ thống thực.

Bạn cũng có thể dùng công cụ khác với trọng tâm khác. CTL làm được thuộc tính reachability, PRISM làm được thuộc tính xác suất, v.v. Nhưng chúng đánh đổi bằng việc yếu hơn ở những thứ TLA+ mạnh, và tất nhiên không công cụ nào xử lý được những thuộc tính không thể diễn đạt bằng logic.

Kết luận

Suy cho cùng, TLA+ khá giỏi hái quả thấp: bất biến và liveness bao quát nhiều thứ ta quan tâm, và TLA+ diễn đạt — kiểm tra chúng ở mức độ hợp lý. Có rất nhiều tiềm năng (và không ít cạm bẫy) trong việc dùng TLA+ để kiểm tra mã nguồn do AI sinh ra. Nhưng cũng có vô số thứ TLA+ thậm chí không diễn đạt được, chứ chưa nói tới kiểm tra.

Với độc giả Việt Nam đang tìm hiểu về kiểm chứng hình thức: TLA+ là công cụ tuyệt vời để thiết kế hệ thống phân tán, nhưng đừng kỳ vọng nó thay thế được tư duy thiết kế và kiểm thử. Việc hiểu rõ giới hạn của công cụ quan trọng không kém việc nắm vững điểm mạnh của nó.