Giải mã TLA+: Từ trào lưu của Boris Cherny đến tương lai phần mềm kiểm chứng bằng máy

Boris tweet, cả internet copy-paste

Tuần này, Boris Cherny đã làm rạng danh TLA+, một bộ công cụ mô hình hóa hình thức đã hơn 30 năm tuổi, bằng một bài đăng trên X (Twitter). Anh ấy đã sử dụng Opus 5.5 để mô hình hóa các phần của Claude Agent SDK trong TLA+ và Lean, và internet đã làm điều mà nó vẫn thường làm: ~1 triệu lượt xem, hàng ngàn lượt lưu, và mọi người đang hỏi TLA+ thực sự là gì. Bài đăng của Boris là một ví dụ tuyệt vời, và nó bổ sung vào những minh chứng sớm cho thấy TLA+ rất đáng để đầu tư công sức trong lập trình tác tử (agentic coding): xem bài viết của Datadog về harness-first agents.

Nếu bạn là một trong những người đang tự hỏi TLA+ là gì và dùng để làm gì, thì bạn đã đến đúng nơi rồi. TLA+ tình cờ là một trong những kỹ thuật hình thức mà đội ngũ của chúng tôi đã nghiên cứu chuyên sâu.

Nhưng còn một lý do lớn hơn khiến chúng tôi quan tâm đến nó. TLA+ cung cấp cho chúng tôi một ngôn ngữ cô đọng để xác định những gì một hệ thống được phép làm và những gì phải luôn luôn hoặc cuối cùng phải đúng với hệ thống đó. Đó là một điểm khởi đầu hữu ích cho việc xác minh, nhưng chưa phải là tất cả.

Đây là phiên bản tóm tắt:

• TLA+ mô tả các hành vi có thể có của hệ thống và các thuộc tính mà những hành vi đó cần thỏa mãn.
• Bản thân TLA+ không xác minh hoàn toàn một bản triển khai. Nó kiểm tra một mô hình của phần mềm chứ không phải chính phần mềm đó, và trình kiểm tra mô hình chính của nó chỉ khám phá các trường hợp hữu hạn.
• Các hệ thống chứng minh hiện đại có thể đưa chúng ta đi xa hơn. Trong Verus, đặc tả, chứng minh và bản triển khai Rust có thể cùng tồn tại trong một ngôn ngữ.
• AI đã có thể tự động hóa một phần của quy trình này. Chúng tôi đã xây dựng một đường ống tác tử (agentic pipeline) chuyển đổi hơn 16.000 cặp đặc tả/thuộc tính TLA+ thành hơn 3.000 chứng minh Verus được máy kiểm tra.

Câu hỏi thú vị ở đây không chỉ là liệu một tác tử có thể viết TLA+ hay không. Mà là điều gì sẽ trở nên khả thi khi các tác tử có thể di chuyển linh hoạt giữa các đặc tả, chứng minh và chương trình thực tế.

Một phần công việc của chúng tôi tại Reasonable là huấn luyện các mô hình để cho phép các tác tử thực hiện điều này một cách nhất quán, đáng tin cậy và nhanh chóng.

TLA+ là gì

Ví dụ thực tế của chúng tôi là ví dụ trong sân chơi tương tác bên dưới, nơi ba máy tính a, b và c phải đồng thuận xem ai trong số chúng là người dẫn đầu (leader). Các cơ sở dữ liệu dựa vào việc bầu chọn người dẫn đầu phải chính xác. Chúng tôi yêu cầu không bao giờ có hai người dẫn đầu cùng một lúc. Bạn có thể nhấp qua sân chơi để tìm hiểu những kiến thức cơ bản về TLA+ thông qua năm cấp độ của trò chơi.

TLA+ (Temporal Logic of Actions - Logic thời gian của các hành động) là một ngôn ngữ dùng để viết ra hai loại đối tượng:

• Một hệ thống chuyển đổi: những gì hệ thống có thể làm. Có các trạng thái, là những ảnh chụp nhanh của hệ thống (ai là ứng cử viên, ai đã bỏ phiếu cho ai, ai là người dẫn đầu) và các hành động, là những bước đơn lẻ làm thay đổi trạng thái ("a bắt đầu một cuộc bầu cử", "b bỏ phiếu cho a"). Trong sân chơi tương tác, bạn thực hiện các bước này bằng tay, khám phá một lượt chạy có thể xảy ra theo cách mà một người kiểm thử (tester) sẽ làm.
• Các thuộc tính thời gian là những tuyên bố về cách một lượt chạy diễn ra theo thời gian. Ví dụ: "Không bao giờ có hai người dẫn đầu." "Một người dẫn đầu cuối cùng sẽ được bầu chọn."

Một mô hình TLA+ khai báo các trạng thái hệ thống hợp lệ và các chuyển đổi được phép giữa các trạng thái này. Ví dụ, trong cuộc bầu cử, bất kỳ ai trong số a, b hoặc c đều có thể bắt đầu một cuộc bầu cử từ trạng thái ban đầu, tự bỏ phiếu cho chính mình khi thực hiện, và b có thể bỏ phiếu cho a hoặc cho c.

Nó không áp đặt thứ tự lên các chuyển đổi và không cố gắng mô hình hóa phân phối xác suất của các sự kiện khác nhau xảy ra, đây là sự trừu tượng hóa phù hợp cho các hệ thống phân tán, nơi các thông điệp, thời gian chờ (timeouts) và hành động của người dùng có thể xảy ra theo nhiều thứ tự khác nhau.

Toán học nền tảng rất đơn giản, nó sử dụng các tập hợp, các tuyên bố đúng/sai và các quan hệ. Các thuộc tính thời gian sau đó được xây dựng từ các toán tử trên các lượt thực thi:

• □ P (luôn luôn P): P đúng trong mọi trạng thái đã ghé qua.
• ◇ P (cuối cùng thì P): P đúng trong một trạng thái tương lai nào đó.
• P ⇝ Q (P dẫn đến Q): bất cứ khi nào P đúng, thì Q cuối cùng cũng sẽ đúng sau đó.

Hai loại thuộc tính thường quan trọng.

An toàn (Safety): không có điều tồi tệ nào xảy ra. Đối với cuộc bầu cử của chúng ta: □ (không bao giờ có hai người dẫn đầu). Trong sân chơi, trình kiểm tra mô hình khám phá mọi trạng thái có thể: tất cả 38 trạng thái cho ba máy tính, và xác nhận thuộc tính đó. Cấp độ 2 thay đổi một quy tắc để một máy tính có thể bỏ phiếu hai lần. Trình kiểm tra sau đó trả về một lượt thực thi sáu bước kết thúc với hai người dẫn đầu. Lượt thực thi đó là một phản ví dụ: một cách cụ thể mà mô hình có thể vi phạm thuộc tính.

Sống động (Liveness): điều tốt đẹp cuối cùng sẽ xảy ra. Chỉ riêng an toàn là không đủ. Một hệ thống không làm gì cả mãi mãi là hoàn toàn an toàn. Vì vậy, chúng ta có thể yêu cầu thêm: ◇ (ai đó là người dẫn đầu). Cấp độ 3 cho thấy lý do tại sao điều này quan trọng: một lỗi đánh máy ngăn cản mọi thứ xảy ra, và kiểm tra an toàn vẫn vượt qua. Tính sống động đòi hỏi các giả định về tính công bằng (fairness), loại bỏ các lượt thực thi nơi một hành động có thể thực hiện mãi mãi nhưng đơn giản là không bao giờ được chọn. Tính công bằng yếu WF(A) nói rằng một hành động vẫn được kích hoạt thì cuối cùng phải xảy ra; tính công bằng mạnh SF(A) bao gồm các hành động trở nên được kích hoạt vô số lần.

Mô hình tư duy rất đơn giản: một mô hình TLA+ mô tả các dấu vết thực thi (execution traces) có thể có của một hệ thống, và một thuộc tính mô tả những dấu vết nào là chấp nhận được. Xác minh là đặt câu hỏi liệu mọi dấu vết có thể có đều chấp nhận được hay không.

TLC, trình kiểm tra mô hình TLA+ tiêu chuẩn, trả lời câu hỏi này bằng cách liệt kê các trạng thái có thể đạt tới cho một trường hợp hữu hạn. Một chứng minh đưa ra tuyên bố mạnh mẽ hơn rằng thuộc tính đó đúng trong trường hợp tổng quát.

Để biết thêm thông tin, Jack Vanlightly đã dạy TLA+ trên blog của mình từ rất lâu trước khi các tác tử làm cho nó trở nên thời thượng.

TLA+ không phải là gì

TLA+ ngày càng được triển khai rộng rãi vì cách suy luận về hệ thống này có thể hữu ích trong thực tế; bạn sẽ thấy nó được sử dụng tại AWS, MongoDB, và Datadog, trong Kafka, và nhiều nơi khác. Nhưng có ba lưu ý quan trọng, nơi mà chỉ riêng TLA+ vẫn chưa đủ để xác minh phần mềm toàn diện.

Kiểm tra mô hình chỉ đi được đến một mức độ nhất định. Trong thực tế, mọi người thường sử dụng TLA+ với TLC. TLC khám phá mọi lượt chạy có thể, nhưng chỉ cho một mô hình hữu hạn. Trong ví dụ của chúng tôi, không gian trạng thái tăng từ 38 trạng thái với ba máy tính lên hơn một triệu với chín máy tính. Để thiết lập một thuộc tính cho các kích thước hệ thống tùy ý, bạn cần một chứng minh. Trình chứng minh của riêng TLA+, TLAPS, có thể làm điều này trong một số trường hợp, nhưng khả năng tự động hóa của nó còn hạn chế, đặc biệt là đối với các lập luận về tính sống động.

Mô hình không phải là bản triển khai. Một đặc tả TLA+ thường là một mô hình riêng biệt của phần mềm. Không có gì tự động đảm bảo rằng bản triển khai hoạt động chính xác như mô hình, và cả hai có thể lệch nhau khi mã nguồn thay đổi. Đây là một yếu tố của khoảng cách kinh điển giữa đặc tả và triển khai.

TLA+ không thể diễn đạt mọi thuộc tính mà chúng ta mong muốn. TLA+ dựa trên logic thời gian tuyến tính (linear temporal logic), đưa ra các tuyên bố về các lượt thực thi riêng lẻ: "Trong mọi lượt chạy, một người dẫn đầu cuối cùng sẽ được bầu chọn." Nhưng một số thuộc tính thú vị lại liên quan đến các tương lai hoặc chiến lược thay thế.

• CTL, một logic thời gian phân nhánh (branching-time logic), có thể diễn đạt các tuyên bố như: "từ bất kỳ trạng thái nào, một cuộc bầu cử mới vẫn có thể được bắt đầu."
• ATL có thể diễn đạt các tuyên bố chiến lược như: "máy tính này có chiến lược để trở thành người dẫn đầu bất kể những máy khác làm gì."

Những thuộc tính phong phú hơn này trở nên phù hợp khi chúng ta bắt đầu suy nghĩ về các hệ thống chứa nhiều tác tử cạnh tranh hoặc cộng tác.

Như vậy, TLA+ cung cấp cho chúng ta một ngôn ngữ hữu ích khác thường để mô tả hành vi theo thời gian, nhưng một ngăn xếp kiểm chứng hoàn chỉnh cần nhiều hơn thế: cơ chế chứng minh mạnh mẽ hơn, kết nối với mã nguồn thực tế và cuối cùng là các logic phong phú hơn.

Từ TLA+ đến các chứng minh

Một hướng đi là đưa mô hình vào một hệ thống chứng minh hiện đại. Có một vài tùy chọn, ví dụ bao gồm:

• Lean mang tính tương tác: bạn (hoặc AI) viết chứng minh từng bước một. Nó rất tổng quát, được sử dụng rộng rãi trong toán học và là trình chứng minh được sử dụng trong bài viết của Boris.
• Verus là công cụ tự động-tương tác (auto-active) và được thiết kế xoay quanh Rust. Bạn cung cấp các đặc tả và cấu trúc chứng minh quan trọng, trong khi một bộ giải tự động sẽ xử lý phần lớn các lập luận ở cấp độ thấp hơn.
• Veil là một công cụ dựa trên Lean được xây dựng dành riêng cho các mô hình máy trạng thái. Leo de Moura đã đề xuất công cụ này và nó gần đây đã được sử dụng để kiểm chứng một công cụ đồng bộ hóa, qua đó sửa được 17 lỗi. Tuy nhiên, tính sống (liveness) vẫn là công việc trong tương lai và mô hình được kiểm chứng vẫn tách biệt với mã thực thi.

Tại sao lại sử dụng Verus? Bởi vì các đặc tả và chứng minh có thể tồn tại song song với mã thực thi Rust thực tế. Điều đó quan trọng vì nó cung cấp cho chúng ta một lộ trình để thu hẹp khoảng cách giữa đặc tả và thực thi: thay vì chỉ chứng minh các thuộc tính về một mô hình trừu tượng riêng biệt, cuối cùng chúng ta có thể chứng minh rằng mã thực thi tinh chỉnh mô hình đó. Các hệ thống như Anvil đã chứng minh phong cách kiểm chứng này; công việc của chúng tôi tại Reasonable xây dựng dựa trên Anvil một cách đặc biệt chặt chẽ.

Tại sao phải tự động hóa kiểm chứng hình thức? Các chứng minh liên quan thường ít kỳ lạ hơn so với những gì cụm từ "kiểm chứng hình thức" gợi ý.

• Các chứng minh an toàn thường mang tính quy nạp. Hãy chỉ ra rằng thuộc tính đó đúng ngay từ đầu, sau đó chỉ ra rằng mọi hành động có thể xảy ra đều bảo toàn thuộc tính đó. Phần lớn công việc bao gồm việc phân tách các hành động khác nhau và theo dõi các bất biến liên quan.
• Các chứng minh về tính sống thiết lập sự tiến triển. Thông thường, một đại lượng nào đó sẽ giảm dần khi hệ thống tiến triển, kết hợp với các giả định về tính công bằng để loại trừ các quá trình thực thi mà trong đó một hành động được kích hoạt bị trì hoãn mãi mãi. Các quy tắc như WF1, WF2, SF1 và SF2 đóng gói các lập luận này; thư viện thời gian của chúng tôi triển khai chúng dưới dạng các bổ đề Verus đã được chứng minh.

Một phần lớn công việc này mang tính lặp đi lặp lại: theo dõi các bất biến, phân tách các hành động, cung cấp các bổ đề trung gian và điền vào các chi tiết mà bộ giải có thể thấy được. Điều đó làm cho nó trở thành mục tiêu tự nhiên cho các tác nhân tạo chứng minh.

Từ chứng minh đến phần mềm được máy kiểm tra

Chứng minh định lý tự động gần đây đã đạt được những tiến bộ nhanh chóng trong toán học. Kiểm chứng phần mềm đặt ra một vấn đề hơi khác: trước khi chứng minh bất cứ điều gì, chúng ta cần một mô tả hữu ích về những gì phần mềm đó dự kiến sẽ thực hiện.

Bài gốc còn tiếp — xem tiếp tại bài gốc ↗