Các cổng xác minh hình thức cho vòng lặp mã hóa AI

series: shen-backpressure /0 Áp lực ngược cấu trúc vượt trội hơn các tác nhân thông minh hơn Các cổng xác minh hình thức cho các vòng lặp mã hóa AI, bằng ngôn ngữ bạn đang sử dụng. Ngày 20/4/2026. Một số lỗi phần mềm nghiêm trọng nhất cũng là những lỗi nhàm chán nhất. Người dùng không được phép đọc dữ liệu của người thuê khác. Không ai phản đối điều này, không ai đứng lên trong buổi đánh giá thiết kế để bảo vệ việc Alice đọc hồ sơ của Bob, nhưng kiểm soát truy cập bị lỗi vẫn là hạng mục số 1 trong OWASP Top 10. Những lỗi này xuất hiện vì quy tắc đã được đặt sai vị trí trong hệ thống. Nó nằm trong một lời nhắc, trong một danh sách kiểm tra đánh giá, trong kỳ vọng chung rằng mọi kỹ sư tương lai, và giờ đây mọi lần gọi mô hình tương lai, sẽ ghi nhớ bất biến và áp dụng lại nó một cách chính xác. Giả định đó vốn đã yếu, và với việc AI tạo ra hầu hết mã, nó hoàn toàn thất bại. Bạn có thể làm tất cả những điều hiển nhiên: đặt quy tắc vào CLAUDE.md, viết một lời nhắc hệ thống cẩn thận, thêm "ủy quyền RẤT QUAN TRỌNG" vào hướng dẫn của tác nhân, và bạn nên làm tất cả những điều đó. Nhưng sau khi mô hình đã viết mười sáu nghìn dòng, câu hỏi thực sự vẫn còn: làm thế nào để bạn biết mã làm những gì bạn muốn? Các bài kiểm tra có ích, nhưng các bài kiểm tra mang tính thực nghiệm. Chúng kiểm tra các trường hợp mà bạn và mô hình đã nhớ để viết, và chúng không thể nói thay cho trình xử lý mà ai đó sẽ thêm vào tuần tới. Tôi muốn kéo một đòn bẩy khác. Đặt cược của tôi, nói một cách thẳng thắn, là: đối với một lớp phần mềm sản xuất rộng lớn, áp lực ngược cấu trúc vượt trội hơn những cải tiến gia tăng trong trí thông minh của tác nhân. Các mô hình hiện có đã có thể viết gần như toàn bộ mã của bạn. Yếu tố hạn chế là liệu bạn có thể biết rằng chúng đã làm những gì bạn muốn hay không, và kiến thức đó đến từ nền tảng mà chúng viết ra, chứ không phải từ việc chờ đợi một mô hình thông minh hơn. Shen-Backpressure là công cụ và phương pháp mà tôi đã xây dựng để khám phá đặt cược đó. Tôi sẽ trình bày những gì nó làm thông qua một bản demo đang chạy, và sau đó chỉ ra cách kết nối cùng một vòng lặp vào dự án của riêng bạn. Cổng hành vi và cổng cấu trúc Hầu hết các ràng buộc cấp độ lời nhắc là cổng hành vi. Chúng ta nói với mô hình "không bỏ qua ủy quyền", "xác thực đầu vào", "sử dụng trình trợ giúp chung". Các mô hình tuân theo các hướng dẫn này đủ thường xuyên để hữu ích và thất bại đủ thường xuyên để làm cho toàn bộ sắp xếp trở nên không ổn định. Một cổng hành vi phụ thuộc vào việc mô hình ghi nhớ quy tắc, nhận ra nơi nó áp dụng, chống lại lực hút của ngữ cảnh cục bộ, và sau đó là một người đánh giá duy trì cùng một bất biến trên toàn bộ cơ sở mã. Các cổng cấu trúc thì khác. Một trình biên dịch, một trình kiểm tra kiểu, một trình chạy thử nghiệm, một trình kiểm tra lỗi cú pháp, một trình kiểm tra bằng chứng. Mỗi cái tạo ra một câu trả lời cụ thể về hiện vật trước mặt nó. Câu trả lời không hoàn hảo, nhưng nó là thật, và trong phạm vi của nó, nó từ chối khi mã sai. Sự từ chối đó là điểm mấu chốt. Nó cho phép chúng ta chuyển công việc ra khỏi không gian hướng dẫn của mô hình và vào nền tảng mà mô hình đang xây dựng. Thay vì tốn token để cầu xin mô hình ghi nhớ một bất biến, chúng ta sắp xếp mã sao cho bất biến khó bị vi phạm một cách tình cờ: lấy thuộc tính bạn quan tâm nhất, thể hiện nó dưới dạng máy có thể kiểm tra, chiếu nó vào triển khai và để vòng lặp bật ra khỏi kiểm tra đó cho đến khi hiện vật mới nổi thỏa mãn nó. Đây là điều làm cho áp lực ngược (backpressure), theo cách Geoff Huntley sử dụng thuật ngữ này trong Ralph và bài luận Don’t Waste Your Backpressure, trở nên mạnh mẽ. Khi các lỗi trước đó được đưa vào vòng lặp tiếp theo, một cổng xác định cung cấp cho vòng lặp một cơ sở vững chắc hơn là cảm tính để đẩy tới. Vòng lặp đó không còn là một ý tưởng chuyên biệt: Codex CLI hiện đã tích hợp /goal, phiên bản Ralph loop của OpenAI, duy trì một mục tiêu xuyên suốt các lượt và không dừng lại cho đến khi mục tiêu đó được đáp ứng. **Sự dịch chuyển của Substrate** Các bất biến đáng được thực thi thường dễ dàng được phát biểu một cách chính xác. Người dùng chỉ có thể truy cập tài nguyên nếu được xác thực, là thành viên của tenant và tài nguyên thuộc về tenant đó. Đó là một quy tắc hoàn chỉnh, có giới hạn. Tiếng Anh đơn giản là phương tiện không phù hợp để thực thi nó. Shen-Backpressure sử dụng Shen, một ngôn ngữ Lisp nhỏ, được gõ tĩnh với hệ thống kiểu tính toán tuần tự, để viết loại quy tắc đó dưới dạng mà máy có thể chiếu vào substrate: các kiểu ngôn ngữ đích, hàm tạo và lệnh cổng mà mô hình phải viết. Bạn viết đặc tả một lần; một trình tạo mã (shengen) sẽ chuyển nó thành các kiểu bảo vệ trong ngôn ngữ đích của bạn. Mô hình viết Go hoặc TypeScript không cần biết Shen tồn tại. Nó cần mã phải biên dịch và các cổng phải vượt qua. **Một chuỗi chứng minh cho xác thực đa tenant** Đây là phần cốt lõi của bản demo API đa tenant, một đoạn trích từ specs/core.shen: (datatype jwt-token X : string; (not (= X "")) : verified; ============================ X : jwt-token;) (datatype tenant-access Principal : authenticated-principal; Tenant : tenant-id; IsMember : boolean; (= IsMember true) : verified; ================================ [Principal Tenant IsMember] : tenant-access;) (datatype resource-access Access : tenant-access; Resource : resource-id; IsOwned : boolean; (= IsOwned true) : verified; ================================ [Access Resource IsOwned] : resource-access;) Dòng ngang thực hiện công việc. Các tiền đề phía trên dòng phải được thỏa mãn trước khi kết luận phía dưới có thể được xây dựng. Để có được một resource-access, bạn cần một tenant-access và bằng chứng tài nguyên thuộc sở hữu, và để có được một tenant-access, bạn cần một principal được xác thực và bằng chứng về tư cách thành viên. Chuỗi đầy đủ chạy jwt-token → authenticated-user → tenant-access → resource-access. Xem đặc tả đầy đủ để biết các quy tắc trung gian. Các kiểu này là các bằng chứng. Việc xây dựng một giá trị của một trong số chúng đòi hỏi phải giải phóng các tiền đề được khai báo trong quy tắc của nó. **Từ đặc tả đến kiểu bảo vệ** shengen chuyển đổi mỗi quy tắc thành một kiểu bảo vệ trong ngôn ngữ đích. Trong Go, các trường không được xuất, và hàm tạo được tạo là cách duy nhất để điền vào một trường: type TenantAccess struct { principal AuthenticatedPrincipal tenant TenantId isMember bool } func NewTenantAccess(principal Aut