# Test hay verify hình thức khi agent viết code?

> Test chạy code thật, verify hình thức xét mọi trạng thái của một mô tả. Mỗi loại bỏ sót gì, và khi agent viết code thì nên phân công ra sao.

Canonical URL: https://learn.chabulab.com/vi/ai/test-hay-verify-hinh-thuc-khi-agent-viet-code. Kiểm tra thông tin: 2026-11-04.

- Test chứng minh code thật chạy đúng trong những lần chạy thử. Verify hình thức chứng minh một mô tả đúng ở mọi trạng thái, với những luật đã viết ra. Không loại nào thay được loại kia.
- Phần lớn lỗi còn sót sau verify hình thức nằm ở chỗ nó không bao phủ: luật chưa viết, chỗ mô tả khác code, và môi trường thật. Nghiên cứu về hệ thống đã chứng minh hình thức cũng cho kết quả như vậy.
- Một check chỉ đáng tin sau khi đã thấy nó báo đỏ: đưa lỗi trở lại và xem nó có bắt được không. Điều này càng quan trọng khi cùng một agent viết cả code lẫn check.
- Việc agent ngày càng viết được nhiều chứng minh hơn là điều đã đo được trên benchmark. Agent giỏi hơn con người trong mọi việc vẫn chỉ là dự đoán. Chúng tôi khuyên phân công theo rủi ro, và con người giữ phần quyết định điều gì được coi là đúng.

Muốn biết một cây cầu có an toàn không, bạn có hai cách. Cho xe tải chạy qua: cây cầu thật được thử, nhưng chỉ với những chiếc xe đã chạy qua. Hoặc tính toán trên bản vẽ: mọi tải trọng đều được xét, nhưng chỉ trong bản vẽ, và thợ có thể đã không xây đúng bản vẽ. Test giống cách đầu. **Verify hình thức** (formal verification) giống cách sau. Bài này so sánh hai cách, rồi trả lời nên phân công chúng thế nào khi agent viết phần lớn code.

Câu trả lời ngắn: hai loại bắt những lỗi khác nhau, nên đừng chọn một. Hãy chọn theo rủi ro, và luôn kiểm tra xem bản thân check có báo đỏ được không.

## Tự thử: cùng một lỗi, ba loại check thấy gì?

Bản demo dưới đây có một luồng lưu dữ liệu nhỏ và sáu cách viết sai, rút gọn từ các lỗi có thật. Ba loại check chạy thật ngay trong trình duyệt của bạn. Bấm vào một ô để xem đường dẫn tới lỗi.

*Hàng đầu là code đúng để đối chứng, nên phải luôn xanh. Bật từng giả định và xem ô nào đổi. Bấm vào một ô để đọc chi tiết.*

Thử theo thứ tự:

1. Chưa bật gì. Chỉ lỗi "Lưu bản sao cũ" bị bắt, 3 trên 18 ô. Sáu lỗi vẫn nằm đó, và hầu như mọi check đều xanh.
2. Bật **Đọc hoặc ghi có thể lỗi**. Con số lên 6 trên 18. Xem hàng "Đọc lần hai sau lỗi": test ngẫu nhiên bắt được, model thì bỏ sót. Test chạy code thật, còn model chạy theo mô tả mà tác giả tin là đúng, với chỉ một lần đọc.
3. Bật **Model đọc đúng số lần như code**. Model bắt được ngay. Công cụ không đổi, chỉ mô tả đã đúng hơn.
4. Bật **Có luật: chưa lưu phải báo**. Hàng "Chưa lưu mà không báo" chuyển sang bắt được ở cả ba cột. Trước đó không check nào thấy, vì chưa ai viết luật này.
5. Bật hai giả định còn lại: kết quả là 14 trên 18. Bốn ô còn bỏ sót đều ở cột test ví dụ, vì không ai viết kịch bản cho các lỗi đó.
6. Đổi số lần chạy ngẫu nhiên xuống 5 rồi đổi seed vài lần. Có lần test ngẫu nhiên bỏ sót tới ba lỗi. Với 50 lần chạy thì ba seed chúng tôi thử đều bắt đủ. Model không phụ thuộc may rủi như vậy, trong phạm vi mô tả của nó.

## Mỗi loại check chứng minh được gì, và bỏ sót gì?

Mỗi loại trả lời một câu hỏi khác nhau, và không loại nào trả lời được cả hai vế: "code thật có chạy đúng không" và "mọi trường hợp đã được xét chưa".

| Loại | Chứng minh được | Bỏ sót | Hợp nhất với |
| --- | --- | --- | --- |
| Test ví dụ | Code thật đúng với những đầu vào đã viết | Trường hợp không ai nghĩ tới | Ghi lại hành vi đã thống nhất, chặn lỗi cũ quay lại |
| Test thuộc tính, ngẫu nhiên | Một luật đúng trên rất nhiều đầu vào sinh ra, chạy trên code thật | Trường hợp hiếm mà bộ sinh dữ liệu ít chạm tới, luật chưa viết | Parser, tính toán, biến đổi dữ liệu |
| E2E, chạy thử thật | Luồng người dùng chạy trên môi trường thật hoặc gần thật | Thứ tự hiếm, chậm và tốn công nên chạy ít | Luồng chính, tích hợp, thiết bị thật |
| Model checking (TLA+) | Trong mô tả và trong giới hạn đã đặt, không có đường nào phá luật đã viết | Chỗ mô tả khác code, luật chưa viết, kích thước lớn hơn giới hạn | Retry, race, thứ tự sự kiện, thiết kế trước khi viết code |
| Chứng minh bằng máy (Dafny, Lean, Rocq) | Code đã chứng minh đúng với đặc tả, trên mọi đầu vào | Đặc tả sai, phần không được chứng minh quanh nó, hiệu năng | Lõi nhỏ, sống lâu, sai thì rất đắt |
| Review kèm lệnh tái hiện | Một lỗi cụ thể có thật, vì đã chạy ra | Không chứng minh được là hết lỗi | Tìm luật còn thiếu, người khác nhìn với giả định khác |

Điểm dễ nhầm: model checking và chứng minh đều là verify hình thức, nhưng khác nhau ở một chỗ quan trọng. TLA+ thường xét một **mô tả** của hệ thống, nên code thật vẫn chưa được kiểm tra. Dafny hay Lean có thể chứng minh trên chính code, nhưng cái giá công sức cao hơn nhiều.

## Bằng chứng từ nơi khác nói gì?

Các nghiên cứu dưới đây lớn hơn trải nghiệm của chúng tôi nhiều, và phần lớn cho thấy verify hình thức có giá trị thật, nhưng dừng ở đúng ranh giới của nó.

- **AWS dùng TLA+ từ năm 2011.** [Paper năm 2015](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf) kể model tìm ra lỗi thiết kế ở S3, DynamoDB và EBS, có lỗi cần chuỗi 35 bước mới lộ ra. Họ cũng cho biết kỹ sư học được và có kết quả sau 2 đến 3 tuần. Cùng paper viết rõ hai giới hạn: lúc đó họ không biết công cụ nào kiểm tra được code khớp với đặc tả ở quy mô của họ, và đặc tả hình thức không phù hợp với suy giảm hiệu năng kéo dài.
- **Hệ thống đã chứng minh vẫn có lỗi, nhưng ở ranh giới.** [Fonseca và cộng sự](https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf) tìm thấy 16 lỗi trong ba hệ thống phân tán đã chứng minh hình thức, 11 lỗi ở lớp shim nối phần đã chứng minh với hệ điều hành. Họ không tìm thấy lỗi nào trong phần giao thức, trong khi hệ thống chưa chứng minh thì có nhiều lỗi kiểu này. Họ tìm ra các lỗi đó bằng đọc code và test.
- **Trình biên dịch đã chứng minh cũng vậy.** Khi [thử Csmith](https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf) trên CompCert với khoảng sáu năm CPU, nhóm tác giả không tìm được lỗi sinh sai mã ở phần giữa, trong khi mọi trình biên dịch khác đều có. Lỗi họ tìm được nằm ở các phần chưa được chứng minh.
- **Độ phủ không phải thước đo chất lượng.** [Inozemtseva và Holmes](https://www.cs.ubc.ca/~rtholmes/papers/icse_2014_inozemtseva.pdf) thấy tương quan giữa độ phủ và khả năng phát hiện lỗi chỉ ở mức thấp đến vừa khi đã kiểm soát số lượng test.
- **Test thuộc tính có ích, và khó biết nó đủ chưa.** [Nghiên cứu ở Jane Street](https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf) qua 30 cuộc phỏng vấn cho thấy lập trình viên đánh giá cao phương pháp này, nhưng thấy khó viết bộ sinh dữ liệu và khó đánh giá test có hiệu quả không. Đây là nghiên cứu định tính ở một công ty.

## Vì sao một check xanh chưa đủ để tin?

Vì màu xanh chỉ có ý nghĩa khi check có khả năng báo đỏ. Cách kiểm tra rất đơn giản: đưa lỗi trở lại, hoặc bỏ đoạn bảo vệ, và xem check có đỏ không. Làm việc này một cách có hệ thống gọi là **mutation testing**, và [Google đã chạy nó](https://arxiv.org/abs/2102.11378) ở quy mô hơn 24.000 lập trình viên, ngay trong lúc review code.

Điều này quan trọng hơn khi agent viết test. [Một thí nghiệm có đối chứng](https://arxiv.org/abs/2410.21136) trên 24 repo Java thấy test do LLM sinh ra chủ yếu ghi lại hành vi hiện có của code, thay vì hành vi đúng ra phải có, nên khó phát hiện lỗi. Ở chiều ngược lại, [hệ thống ACH của Meta](https://arxiv.org/abs/2501.12862) dùng lỗi giả để định hướng LLM viết test, và kỹ sư chấp nhận 73% số test đó trong các đợt thử.

Trong thử nghiệm của chúng tôi, một test kiểm tra "mở app nhiều lần chỉ tạo một bản sao lưu" không thể fail: các lần mở rơi vào cùng một mili giây nên gộp thành một khoá. Nó báo xanh vì lý do sai, và chỉ lộ ra khi chúng tôi hỏi vì sao nó không đỏ.

## Thử nghiệm nhỏ của chúng tôi cho thấy gì?

Cho thấy review độc lập kèm lệnh tái hiện vẫn tìm ra lỗi thật sau khi model và test đều xanh, nhưng bằng chứng này yếu. Nó bắt đầu từ một [bài đăng của Lauren Tan (@poteto)](https://x.com/poteto) ngày 3/11/2026, cho rằng review đối kháng phần lớn phí token, và nên dùng số token đó cho kiểm thử thực nghiệm kết hợp với verify hình thức. Skill [interrogate](https://github.com/cursor/plugins/tree/main/pstack) của tác giả cũng chỉ giữ lại phát hiện có lần chạy chứng minh. Chúng tôi thử cách này trên phần lưu tiến độ của LexiLoop, app học từ vựng của ChabuLab. Repo này riêng tư, nên bạn không tự kiểm tra được các số dưới đây.

Quy trình là: viết luật, viết model TLA+ và test, thấy chúng đỏ khi bỏ đoạn bảo vệ, rồi mới sửa. Sau mỗi bản sửa, một reviewer trên mô hình khác cố phá code và phải đưa ra lệnh tái hiện. Kết quả sáu lượt, trong khoảng ba giờ:

| Lượt | Lỗi do chính bản vá trước gây ra | Lỗi có từ trước | Ví dụ |
| --- | --- | --- | --- |
| Lượt 1 | 2 | 2 | Ghi lại bản sao lưu đã có mà lỗi thì chặn luôn việc lưu |
| Lượt 2 | 1 | 1 | Dữ liệu hỏng khi đang mở app làm mất phần tab còn giữ |
| Lượt 3 | 1 | 2 | Đọc lần hai thành công duyệt một lần ghi dựa trên lần đọc đã lỗi |
| Lượt 4 | 0 | 2 | Một hàng hỏng trong JSON hợp lệ bị xoá không sao lưu |
| Lượt 5 | 1 | 0 | Sửa bản ghi hỏng làm lùi tiến độ tab khác vừa lưu |
| Lượt 6 | 0 | 0 | Không tìm ra lỗi, sau bảy cách phá thử riêng |

Mỗi lượt đều chạy sau khi kiểm tra của tác giả báo xanh. Lượt 2 có 154 test qua, lượt 3 có 159, lượt 4 có 162. Ngày 4/11/2026, chúng tôi chạy lại trên bản cuối: 169 test, 899.377 lần so khớp, ba model đạt với 18, 26 và 4.840 trạng thái. Bỏ đoạn bảo vệ ở model lớn nhất thì TLC báo vi phạm ngay sau 23 trạng thái.

Hai chuyện đáng nhớ:

- **Model sai theo đúng lỗi tư duy của tác giả.** Lượt 3 tìm ra lỗi ở chỗ code đọc hai lần, trong khi model chỉ có một lần đọc. Model xanh vì nó mô tả code mà tác giả nghĩ mình đã viết. Cách sửa là cho code khớp với model, và thêm test làm lỗi từng lần gọi bộ nhớ.
- **Chạy thật đổi thứ tự ưu tiên.** Model báo bấm đúp có thể xoá tiến độ, nhưng chạy thật thì một lần bấm đúp chỉ kích hoạt một lần. Trong khi đó, một lần chạm vào nút "Đã thuộc" xoá mười câu trả lời đúng, và lỗi này từng bị một review trước đó xếp mức thấp nhất.

### Bằng chứng này yếu ở đâu?

Đừng dùng nó như kết luận chung, vì những lý do sau:

- **Mẫu rất nhỏ.** Một dự án, một người, một buổi tối, một phần code. Không có nhóm đối chứng.
- **Phản biện từ chủ dự án.** Có thể review tìm ra lỗi chính vì verify hình thức trước đó chưa đủ tốt: model mới viết, và lỗi đọc thất bại lúc đầu chưa có trong model. Thử nghiệm này không tách được hai giả thuyết "review bắt được thứ verify hình thức không bắt được" và "verify hình thức ở đây còn yếu".
- **Mỗi bản vá thêm code mới.** Bốn trên năm lượt đầu bắt được lỗi do bản vá trước gây ra, nên số lỗi không đo được chất lượng ban đầu.
- **Lượt 6 sạch không chứng minh là hết lỗi.** Nó chỉ cho biết một mô hình miễn phí không tìm ra. Các reviewer cũng không dùng cùng một mô hình.
- **Chưa đo chi phí token,** nên không kết luận được cách nào rẻ hơn.
- **Phần chưa được kiểm tra.** Android, chạm thật trên iPhone, và lỗi lưu trữ thật của hệ điều hành. Các lỗi lưu trữ trong test đều là giả lập.

Điều chúng tôi rút ra chỉ ở mức này: với thay đổi về dữ liệu người dùng, chúng tôi giữ một reviewer độc lập, và mọi phát hiện phải kèm lệnh tái hiện.

## Về agent, điều gì đã đo được và điều gì chỉ là dự đoán?

Năng lực viết chứng minh trên benchmark đã được đo và đang tăng. Việc agent giỏi hơn con người trong toàn bộ công việc thì chưa có ai đo được.

| Nhận định | Bằng chứng | Trạng thái |
| --- | --- | --- |
| LLM viết được gợi ý chứng minh cho Dafny | [68% năm 2024](https://arxiv.org/abs/2406.08467), [96% một năm sau](https://arxiv.org/abs/2509.22908), trên benchmark | Đã đo, trên benchmark |
| LLM sinh được code kèm chứng minh từ đặc tả có sẵn | [82% Dafny, 44% Verus, 27% Lean](https://arxiv.org/abs/2509.22908) | Đã đo. Đặc tả có sẵn, không phải do agent tự nghĩ ra |
| Agent làm được việc ngày càng dài | [Khoảng 50 phút vào đầu 2025, gấp đôi sau khoảng 7 tháng](https://arxiv.org/abs/2503.14499) | Xu hướng đã đo. Kéo dài nó ra tương lai là dự báo |
| Agent giúp lập trình viên nhanh hơn | [Chậm hơn 19% đầu 2025](https://arxiv.org/abs/2507.09089). [Đợt sau nhanh hơn 18% và 4%, nhưng METR gọi là tín hiệu không đáng tin](https://metr.org/blog/2026-02-24-uplift-update/) | Chưa ngã ngũ |
| Verify hình thức sẽ thành phổ biến nhờ AI | [Kleppmann](https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html) tự gọi đây là dự đoán | Dự đoán |
| Agent sẽ giỏi hơn con người trong mọi việc | Chúng tôi không tìm thấy nghiên cứu nào đo được điều này | Dự đoán, không phải sự thật |

Phần dưới đây là suy luận của chúng tôi, chưa có số đo. Giả sử agent thật sự viết code và chứng minh giỏi hơn con người:

- **Chi phí đổi, câu hỏi thì không.** Kleppmann cũng chỉ ra rằng khi chứng minh rẻ đi, khó khăn dời sang việc đặc tả: những thuộc tính đã chứng minh có đúng là thứ bạn cần không.
- **Ranh giới vẫn còn.** Lỗi trong nghiên cứu của Fonseca nằm ở giả định về phần không được chứng minh. Ổ đĩa, mạng và trình duyệt thật không tự chứng minh được, nên vẫn cần chạy thử.
- **Cùng tác giả, cùng điểm mù.** Khi một agent viết cả code, test và model, chúng dễ chia sẻ một giả định sai. Thông minh hơn không tự xoá đi việc này. Dùng một tác nhân độc lập, hoặc buộc check báo đỏ, thì có.
- **"Đúng" là một lựa chọn.** Có nên xoá ghi chú khi xoá điểm đánh dấu không? Không công cụ nào trả lời được cho tới khi có người quyết định.

Nếu sau này có bằng chứng ngược lại, phần này nên được viết lại.

## Nên phân công hai loại check thế nào?

Hãy chọn theo rủi ro, và đừng chạy mọi thứ cho mọi thay đổi. Đây là khuyến nghị của chúng tôi, dựa trên các nguồn ở trên và một dự án của chúng tôi, không phải kết quả đã được chứng minh.

| Rủi ro | Check chính | Check bổ sung | Con người quyết định |
| --- | --- | --- | --- |
| Tính toán, parser, biến đổi dữ liệu | Test thuộc tính hoặc vét cạn | Mutation testing | Luật nào phải luôn đúng |
| Retry, race, lưu và hoàn tác, hàng đợi | Model checking | Test làm lỗi từng lần gọi trên code thật, cho khớp số lần đọc và ghi | Giới hạn nào chấp nhận được |
| Dữ liệu người dùng, tiền, đăng nhập | Như trên | Một reviewer độc lập, kèm lệnh tái hiện | Có phát hành hay không |
| Lõi nhỏ, sống lâu, sai rất đắt (mật mã, đồng thuận) | Chứng minh bằng máy | Test ở ranh giới với phần không được chứng minh | Có đáng chi trả không |
| Luồng người dùng, tích hợp | E2E trên môi trường thật | Thiết bị thật trước khi phát hành | Luồng nào là chính |
| Hiệu năng, quá tải | Thử tải, đo thật | Theo dõi sau phát hành | Ngưỡng chấp nhận |
| Giao diện, câu chữ, cảm giác | Ảnh chụp và người xem | Kiểm tra ngôn ngữ, độ tương phản bằng máy | Đẹp và đúng giọng hay chưa |
| Thay đổi nhỏ, không có logic | Lint, kiểm tra kiểu | Không cần thêm | Không cần |

Với các thay đổi rủi ro, quy trình chúng tôi đang dùng là:

Viết luật → Agent viết code → Đưa lỗi trở lại → Reviewer độc lập → Thử thật → Chốt giới hạn

## Con người còn giữ phần nào?

Theo chúng tôi là những việc có người chịu trách nhiệm về kết quả, kể cả khi agent làm giỏi hơn phần còn lại. Đây là quan điểm, không phải số đo.

- **Quyết định điều gì được coi là đúng.** Ở LexiLoop, hai tab lưu trong cùng 1 đến 2 mili giây có thể mất một câu trả lời. Chúng tôi chấp nhận, vì một người không trả lời nhanh như vậy, và khoá mọi lần lưu lại mở ra một rủi ro khác khi đóng tab. Reviewer tìm ra lỗi, nhưng không check nào quyết định thay được.
- **Chọn mức đầu tư.** Chứng minh toàn bộ một app học từ vựng là lãng phí. Không chứng minh phần lõi của một hệ thống thanh toán thì có thể không.
- **Việc cần trải nghiệm thật.** Chạm trên điện thoại thật, đọc câu chữ, cảm nhận nhịp của giao diện.
- **Đọc kết quả với thái độ nghi ngờ.** Hỏi "check này không bao phủ gì?" sau mỗi lần xanh.

## Tự chạy một model checker nhỏ

Đoạn mã dưới đây cần Node 22.18 trở lên, không cần thư viện ngoài. Lưu thành `lost-update.ts` rồi chạy `node lost-update.ts`. Nó là một model checker đầy đủ cho lỗi hai tab ghi đè nhau. Nó đặt test tuần tự, test ngẫu nhiên và duyệt mọi trạng thái cạnh nhau.

```ts
// lost-update.ts: node lost-update.ts
// Hai tab cộng vào một số đã lưu. Mỗi lần lưu đọc trước, ghi sau.
type State = { disk: number; tabs: { read: number | null; done: number }[] };
type Step = { tab: number; kind: "read" | "write" };

const ANSWERS_PER_TAB = 2;

function steps(s: State): Step[] {
  return s.tabs.flatMap((t, tab): Step[] => {
    if (t.read !== null) return [{ tab, kind: "write" }];
    return t.done < ANSWERS_PER_TAB ? [{ tab, kind: "read" }] : [];
  });
}

function apply(s: State, { tab, kind }: Step): State {
  const next: State = structuredClone(s);
  const t = next.tabs[tab]!;
  if (kind === "read") t.read = s.disk;
  else {
    next.disk = t.read! + 1;
    t.read = null;
    t.done += 1;
  }
  return next;
}

// Luật: khi không tab nào đang lưu dở, mọi câu trả lời đều đã lưu.
const holds = (s: State) =>
  s.tabs.some((t) => t.read !== null) || s.disk === s.tabs[0]!.done + s.tabs[1]!.done;

const start: State = { disk: 0, tabs: [{ read: null, done: 0 }, { read: null, done: 0 }] };

// Model checker: đi qua mọi trạng thái theo chiều rộng, nên đường tìm được là đường ngắn nhất.
function check(): { states: number; path: Step[] | null } {
  const seen = new Set([JSON.stringify(start)]);
  let frontier = [{ state: start, path: [] as Step[] }];
  while (frontier.length > 0) {
    const next: typeof frontier = [];
    for (const { state, path } of frontier) {
      for (const step of steps(state)) {
        const after = apply(state, step);
        const key = JSON.stringify(after);
        if (seen.has(key)) continue;
        seen.add(key);
        const trail = [...path, step];
        if (!holds(after)) return { states: seen.size, path: trail };
        next.push({ state: after, path: trail });
      }
    }
    frontier = next;
  }
  return { states: seen.size, path: null };
}

// Test như cách thường viết: tab này lưu xong rồi mới tới tab kia.
function sequentialTest(): boolean {
  let s = start;
  for (const tab of [0, 1, 0, 1]) {
    s = apply(apply(s, { tab, kind: "read" }), { tab, kind: "write" });
  }
  return holds(s);
}

// Test ngẫu nhiên: cùng các bước đó theo thứ tự ngẫu nhiên, lặp lại nhiều lần.
function randomTest(runs: number): number {
  let failures = 0;
  for (let run = 0; run < runs; run++) {
    let s = start;
    for (let options = steps(s); options.length > 0; options = steps(s)) {
      s = apply(s, options[Math.floor(Math.random() * options.length)]!);
      if (!holds(s)) {
        failures += 1;
        break;
      }
    }
  }
  return failures;
}

const { states, path } = check();
console.log("sequential test passes:", sequentialTest());
console.log("random test failures in 1000 runs:", randomTest(1000));
console.log("model states visited:", states);
console.log("shortest path:", path?.map((p) => `tab${p.tab} ${p.kind}`).join(", "));
```

Ngày 4/11/2026, trên Node 26.11.1, kết quả là:

```text
sequential test passes: true
random test failures in 1000 runs: 825
model states visited: 17
shortest path: tab0 read, tab1 read, tab0 write, tab1 write
```

Test tuần tự xanh dù có lỗi, vì nó không bao giờ cho hai tab chen nhau. Dòng thứ hai là ngẫu nhiên, nên số của bạn sẽ khác một chút. Chúng tôi chạy lại lần nữa được 804. Thay đổi `apply` để đọc và ghi trong cùng một bước, rồi chạy lại để thấy lỗi biến mất.

## Chạy thử TLA+ thật thế nào?

Làm theo sáu bước dưới đây, khoảng mười phút. Đoạn code trong bài không phải Java mà là TLA+, ngôn ngữ để mô tả hệ thống, và nó không chạy trong sản phẩm nào cả. Công cụ kiểm tra tên là TLC. TLC được viết bằng Java, nên bạn chỉ cần Java để chạy TLC.

**Bước 1: cài Java 11 trở lên.** Chạy `java -version` trước. Nếu máy báo chưa có lệnh này, hoặc số đầu tiên nhỏ hơn 11, hãy mở hướng dẫn:

**Cài Java trên Windows, macOS và Ubuntu**

**Windows**, trong PowerShell:

```powershell
winget install EclipseAdoptium.Temurin.21.JDK
```

Nếu máy không có `winget`, hãy tải bộ cài JDK 21 từ [trang Eclipse Temurin](https://adoptium.net/temurin/releases/). Cài xong, mở một cửa sổ PowerShell mới để máy nhận lệnh `java`. Chúng tôi chưa thử các bước Windows trên máy thật. Chúng tôi chỉ xác nhận gói này có trong kho winget.

**macOS**, cần có [Homebrew](https://brew.sh/):

```bash
brew install --cask temurin@21
```

Chúng tôi xác nhận gói này có trên Homebrew, và chạy các bước sau đó trên Mac với OpenJDK 25 đã có sẵn, không chạy lại lệnh cài.

**Ubuntu**:

```bash
sudo apt update
sudo apt install -y default-jre-headless
```

Chúng tôi đã chạy toàn bộ các bước trong bài trên Ubuntu 24.04 sạch, gói này cài Java 21.

**Kiểm tra trên cả ba máy**, số đầu tiên phải từ 11 trở lên:

```bash
java -version
```



**Bước 2: tạo một thư mục trống.** Lệnh này giống nhau trên cả ba hệ điều hành:

```bash
mkdir tla-demo
cd tla-demo
```

**Bước 3: lưu hai file vào thư mục đó.** Tên file phải đúng từng chữ. File đầu tên `LostUpdate.tla`:

```text
---- MODULE LostUpdate ----
\* Hai tab cộng vào một số đã lưu. Mỗi lần lưu đọc trước, ghi sau.
EXTENDS Integers
CONSTANTS Tabs, Answers
VARIABLES disk, read, done

Init == disk = 0 /\ read = [t \in Tabs |-> -1] /\ done = [t \in Tabs |-> 0]

Read(t) ==
  /\ read[t] = -1 /\ done[t] < Answers
  /\ read' = [read EXCEPT ![t] = disk]
  /\ UNCHANGED <<disk, done>>

Write(t) ==
  /\ read[t] # -1
  /\ disk' = read[t] + 1
  /\ read' = [read EXCEPT ![t] = -1]
  /\ done' = [done EXCEPT ![t] = @ + 1]

Next == \E t \in Tabs : Read(t) \/ Write(t)

\* Luật: khi không tab nào đang lưu dở, mọi câu trả lời đều đã lưu.
RECURSIVE Sum(_)
Sum(S) == IF S = {} THEN 0 ELSE LET t == CHOOSE x \in S : TRUE IN done[t] + Sum(S \ {t})
NothingLost == (\E t \in Tabs : read[t] # -1) \/ disk = Sum(Tabs)
====
```

File thứ hai tên `LostUpdate.cfg`. Nó cho TLC biết có bao nhiêu tab, bao nhiêu câu trả lời, và cần kiểm tra luật nào:

```text
CONSTANTS
  Tabs = {t1, t2}
  Answers = 2
INIT Init
NEXT Next
INVARIANT NothingLost
```

**Bước 4: tải TLC.** Đây là một file khoảng 2,3 MB. Trên Windows, trong PowerShell, hãy gõ `curl.exe` thay cho `curl`.

```bash
curl -LO https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
```

**Bước 5: chạy.**

```bash
java -cp tla2tools.jar tlc2.TLC -deadlock LostUpdate
```

TLC sẽ báo luật bị phá và in đường dẫn tới lỗi. Với TLC 2.19, phần chính trông như sau, chúng tôi lược bớt các trạng thái ở giữa:

```text
Error: Invariant NothingLost is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ done = (t1 :> 0 @@ t2 :> 0)
/\ read = (t1 :> -1 @@ t2 :> -1)
/\ disk = 0
State 2: <Read line 10, col 3 to line 12, col 29 of module LostUpdate>
...
State 5: <Write line 15, col 3 to line 18, col 39 of module LostUpdate>
/\ done = (t1 :> 1 @@ t2 :> 1)
/\ read = (t1 :> -1 @@ t2 :> -1)
/\ disk = 1
```

Hãy đọc từ trên xuống: hai tab cùng đọc `disk = 0`, rồi lần lượt ghi 1. Dòng cuối có `done` là một câu cho mỗi tab, tổng hai câu, nhưng `disk` chỉ còn 1. Đây chính là một câu trả lời bị mất. TLC cũng tạo một thư mục `states`, bạn có thể xoá.

**Bước 6: sửa lỗi rồi chạy lại.** Trong `LostUpdate.tla`, thay dòng `Next` bằng đoạn dưới đây, để đọc và ghi diễn ra trong cùng một bước. Rồi chạy lại lệnh ở bước 5.

```text
Save(t) ==
  /\ done[t] < Answers
  /\ disk' = disk + 1
  /\ done' = [done EXCEPT ![t] = @ + 1]
  /\ UNCHANGED read

Next == \E t \in Tabs : Save(t)
```

TLC đi qua 9 trạng thái và báo:

```text
Model checking completed. No error has been found.
```

Lúc này hãy nhớ điều bài đã nói: kết quả xanh chỉ nói về bản mô tả này. Code thật của bạn có đọc và ghi trong một bước hay không thì TLC không biết.

Nếu gặp lỗi:

| Thông báo | Nguyên nhân | Cách sửa |
| --- | --- | --- |
| `command not found: java`, hoặc `'java' is not recognized` | Chưa cài Java, hoặc cửa sổ dòng lệnh mở từ trước khi cài | Cài theo bước 1, rồi mở cửa sổ mới |
| `Could not find or load main class tlc2.TLC` | `tla2tools.jar` không nằm trong thư mục hiện tại | Chạy `cd tla-demo` rồi làm lại bước 4 |
| `Cannot find source file for module LostUpdate` | Sai tên file, thường do trình soạn thảo thêm đuôi `.txt` | Đổi tên thành đúng `LostUpdate.tla` |

Chúng tôi đã chạy các bước này ngày 4/11/2026 với TLC 2.19, trên Ubuntu 24.04 sạch với Java 21 và trên macOS với OpenJDK 25.

## Những lỗi hay gặp

- **Coi xanh là xong.** Hãy thêm một dòng: lần xanh này không bao phủ điều gì.
- **Để cùng một agent viết code, test và model rồi tin cả ba.** Hãy buộc check báo đỏ một lần, và dùng tác nhân độc lập cho phần rủi ro.
- **Model có một lần đọc, code có hai.** Mỗi bước trong model phải trỏ tới code thật, với đúng số lần đọc và ghi.
- **Tin bug path của model ngay.** Hãy chạy lại bằng đầu vào thật trước khi xếp mức độ nghiêm trọng.
- **Đuổi theo độ phủ 100%.** Độ phủ cho biết chỗ chưa được test, không cho biết test có tốt không.
- **Review không kèm lệnh chạy.** Một phát hiện không tái hiện được chỉ nên ghi là chưa được chứng minh.
- **Dùng verify hình thức cho mọi thứ.** Nó không giúp gì cho hiệu năng hay giao diện, và tốn công với phần ít rủi ro.

## Giao việc này cho AI thế nào?

Chép đoạn dưới, điền vào chỗ trống rồi đưa cho agent:

```text
Thay đổi: [mô tả thay đổi]
Rủi ro: [dữ liệu người dùng, tiền, đồng thời, giao diện, ...]

Trước hoặc trong khi viết code:
1. Viết ra các luật thay đổi này phải giữ, bằng lời đơn giản. Dừng lại để tôi duyệt nếu có luật cần tôi quyết định.
2. Với mỗi luật, chọn check phù hợp: test thuộc tính hoặc vét cạn cho logic thuần; model checking cho retry, race, lưu và hoàn tác; E2E cho luồng người dùng.
3. Nếu dùng model: mỗi bước phải trỏ tới code thật, với đúng số lần đọc và ghi.

Trước khi báo xong:
4. Với mỗi check, đưa lỗi trở lại hoặc bỏ đoạn bảo vệ, cho tôi thấy nó đỏ, rồi khôi phục.
5. Chạy lại mọi bug path của model bằng đầu vào thật. Nếu không tái hiện được, nói rõ.
6. Báo cáo bắt đầu bằng lệnh đã chạy và kết quả, rồi mới tới tóm tắt.
7. Thêm một dòng: các check này KHÔNG bao phủ điều gì.
8. Liệt kê các giới hạn bạn đề nghị chấp nhận và lý do, để tôi quyết định.

Một phát hiện không có lệnh tái hiện thì ghi là chưa được chứng minh, và không sửa theo nó.
```

## Kiểm tra lại

1. Model TLA+ của bạn báo xanh, nhưng code đọc bộ nhớ hai lần còn model chỉ đọc một lần. Kết quả xanh đó nói gì về code?
   Xem đáp án: Mô tả đúng với luật đã viết, còn code thì chưa nói được gì ở chỗ khác mô tả. Model checking chứng minh về mô tả, không phải về code. Ở chỗ code làm khác mô tả, kết quả xanh không còn áp dụng. LexiLoop đã gặp đúng trường hợp này.
2. Agent viết xong code và test, tất cả đều xanh. Bước nào tăng độ tin cậy của bộ test nhiều nhất?
   Xem đáp án: Đưa lỗi trở lại code và xem test có đỏ không. Test viết cùng lúc với code có thể mang cùng lỗi tư duy, hoặc không thể fail. Đưa lỗi trở lại kiểm tra chính bộ test. Độ phủ thì chỉ tương quan thấp đến vừa với khả năng phát hiện lỗi, theo Inozemtseva và Holmes.
3. Hệ thống của bạn chậm dần khi tải tăng vì client thử lại liên tục, dù không có lỗi logic. Nên dùng gì trước?
   Xem đáp án: Thử tải và đo trên hệ thống chạy thật. Paper của AWS xếp suy giảm hiệu năng kéo dài vào phần đặc tả hình thức không làm tốt: hệ thống vẫn tiến triển nên không có lỗi logic để tìm. Việc này cần đo trên hệ thống thật.
4. Nghiên cứu năm 2017 về ba hệ thống phân tán đã chứng minh hình thức tìm thấy 16 lỗi. Các lỗi đó không nằm ở đâu?
   Xem đáp án: Trong giao thức phân tán đã được chứng minh. Tác giả không tìm thấy lỗi nào trong phần giao thức, trong khi hệ thống chưa chứng minh thì có nhiều. Lỗi nằm ở ranh giới với phần không được chứng minh. Vì vậy chứng minh có giá trị thật, và test ở ranh giới vẫn cần.
5. Hai tab lưu trong cùng 1 đến 2 mili giây có thể mất một câu trả lời, và khoá mọi lần lưu lại tạo một rủi ro khác. Ai nên quyết định chấp nhận hay sửa?
   Xem đáp án: Con người chịu trách nhiệm cho sản phẩm, sau khi agent đưa ra lỗi tái hiện được và các phương án. Check chỉ cho biết luật bị vi phạm khi nào. Việc rủi ro này có đáng sửa hay không là đánh đổi về sản phẩm, và cần người chịu trách nhiệm cho quyết định đó.

## Nguồn

- [Newcombe và cộng sự (2015): How Amazon Web Services Uses Formal Methods](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf)
- [Fonseca và cộng sự (2017): An Empirical Study on the Correctness of Formally Verified Distributed Systems](https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf)
- [Yang và cộng sự (2011): Finding and Understanding Bugs in C Compilers](https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf)
- [Inozemtseva và Holmes (2014): Coverage Is Not Strongly Correlated with Test Suite Effectiveness](https://www.cs.ubc.ca/~rtholmes/papers/icse_2014_inozemtseva.pdf)
- [Goldstein và cộng sự (2024): Property-Based Testing in Practice](https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf)
- [Petrović và cộng sự (2021): Practical Mutation Testing at Scale](https://arxiv.org/abs/2102.11378)
- [Can we find bugs using LLM-generated oracles? (2024)](https://arxiv.org/abs/2410.21136)
- [Mutation-Guided LLM-based Test Generation at Meta (2025)](https://arxiv.org/abs/2501.12862)
- [DafnyBench: A Benchmark for Formal Software Verification (2024)](https://arxiv.org/abs/2406.08467)
- [A benchmark for vericoding: formally verified program synthesis (2025)](https://arxiv.org/abs/2509.22908)
- [Martin Kleppmann (2025): Prediction: AI will make formal verification go mainstream](https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html)
- [METR (2025): Measuring AI Ability to Complete Long Software Tasks](https://arxiv.org/abs/2503.14499)
- [METR (2025): Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity](https://arxiv.org/abs/2507.09089)
- [METR (2026): We are Changing our Developer Productivity Experiment Design](https://metr.org/blog/2026-02-24-uplift-update/)
- [Lauren Tan (@poteto): bài đăng trên X ngày 3/11/2026, đọc qua ảnh chụp màn hình](https://x.com/poteto)
- [pstack: skill interrogate](https://github.com/cursor/plugins/tree/main/pstack)