Lasm: Viết ứng dụng web có kiểm chứng hình thức bằng Lean, chạy trên Node, serverless và edge

Lasm là một công cụ mới cho phép biên dịch các chương trình Lean 4 sang WebAssembly, mở ra khả năng xây dựng ứng dụng web hoàn chỉnh — từ frontend đến backend — chỉ bằng một ngôn ngữ duy nhất và có thể kiểm chứng hình thức (formal verification) các tính chất của mã nguồn trước khi triển khai. Dự án vừa xuất hiện trên Hacker News và nhanh chóng thu hút sự chú ý của cộng đồng lập trình viên quan tâm đến độ tin cậy của phần mềm.

Kiểm chứng hình thức — bước tiến tiếp theo của kỹ thuật phần mềm?

Tác giả của Lasm tin rằng kiểm chứng hình thức chính là hướng phát triển tiếp theo của kỹ thuật phần mềm và ngôn ngữ lập trình. Theo quan điểm này, làn sóng mới sẽ được thúc đẩy mạnh mẽ bởi các mô hình ngôn ngữ lớn (LLM) có khả năng hiểu và viết mã kiểm chứng hình thức.

Lean là một trong những ngôn ngữ phổ biến nhất cho phép kiểm chứng hình thức, và theo tôi đó là một công cụ cực kỳ mạnh mẽ vì nó là ngôn ngữ lập trình đa dụng với khả năng kiểm chứng được tích hợp trực tiếp.

Điểm khác biệt của Lasm nằm ở chỗ: một mã nguồn Lean duy nhất có thể biên dịch thành máy chủ Node, một hàm serverless hoặc edge, một module WASI/Fastly, hoặc một ứng dụng chạy trên trình duyệt. Và vì là Lean, lập trình viên có thể chứng minh các tính chất của chính đoạn mã sẽ được triển khai.

Ví dụ nổi bật: Conduit với 117 định lý được chứng minh

Ví dụ chủ lực của dự án là Conduit — phiên bản ứng dụng RealWorld (một bản sao của Medium) — được viết hoàn toàn bằng Lean, bao gồm REST API, ứng dụng trình duyệt render phía máy chủ và các chứng minh hình thức.

• 117 định lý về đoạn mã thực sự chạy, được kiểm tra không có sorry và chỉ dùng các tiên đề chuẩn của Lean.
• Các chứng minh bao phủ: phân quyền (chỉ tác giả mới sửa được bài viết và bình luận của mình), theo dõi và yêu thích, slug không bao giờ trùng lặp, phân trang không bỏ sót hay lặp lại, kiểm tra dữ liệu dùng chung giữa client và server, tính an toàn của liên kết Markdown.
• Bộ kiểm thử API chính thức của RealWorld vượt qua nguyên vẹn (13/13 tệp, 154 yêu cầu) trên Node, Cloudflare Workers và Bun.
• Bộ kiểm thử end-to-end Playwright chính thức cũng vượt qua không cần chạy lại trên Chromium, Firefox và WebKit.

Hỗ trợ đa nền tảng ấn tượng

Lasm hỗ trợ một danh sách dài các nền tảng triển khai, tất cả đều được kiểm thử trong CI:

• Máy chủ Node hoặc chương trình độc lập (Docker, Kubernetes, Cloud Run, Fly.io, Railway...)
• AWS Lambda, Lambda@Edge
• Vercel Functions, Vercel Edge
• Netlify Functions, Netlify Edge
• Azure Functions, Google Cloud Functions
• Cloudflare Workers, Deno Deploy, Supabase Edge Functions
• Fastly Compute, WASI, wasi-http, Spin
• Trình duyệt (Chrome, Edge, Firefox, Safari)

Đáng chú ý, với các bản dựng Node, chương trình có toàn bộ runtime của Lean (luồng, tệp, tiến trình, socket). Các bản dựng edge, Bun/Deno, WASI và trình duyệt chạy Lean đơn luồng, không có socket hay tiến trình.

Gọi JavaScript và npm từ Lean

Một trong những điểm mạnh của Lasm là khả năng tương tác với hệ sinh thái JavaScript. Mỗi hàm JavaScript cần gọi chỉ cần khai báo bằng một dòng:

import Lasm.JS
open Lasm.JS

/-- `await fetch(url, init)` (fetch toàn cục của Node) -/
@[js "globalThis" "fetch"] opaque fetch : String → Data → IO Value

Cú pháp @[js "module" "export"] cho phép ràng buộc các hàm từ gói npm, module tích hợp của Node hoặc biến toàn cục. Lasm cũng cung cấp sẵn các framework viết bằng Lean như Lasm.Fetch (HTTP), Lasm.UI (kiến trúc Elm cho trình duyệt), Lasm.RPC (API có kiểu dữ liệu), Lasm.Web (DOM và API web) và Lasm.KV.

Hiệu năng và giới hạn

Theo các số đo từ CI trên máy chủ GitHub miễn phí (4 nhân AMD EPYC):

• Node: Hono + handler Lean đạt 24.911 yêu cầu/giây, độ trễ p99 là 4,2 ms (so với 103.134 req/s của Node thuần).
• Khởi động lạnh đến phản hồi HTTP đầu tiên: 159 ms.
• Bundle Cloudflare Workers: 1,40 MiB, nén gzip còn 245 KiB.
• Trình duyệt: ứng dụng đếm đơn giản chỉ tải 152 KiB brotli, khung hình đầu tiên sau 30 ms.
• Thời gian biên dịch: bản dựng Hono sạch mất 4,7 giây, xây dựng lại sau khi sửa một dòng mất 2,0 giây.

Tuy nhiên, dự án cũng thẳng thắn nêu các hạn chế:

• Chỉ biên dịch ahead-of-time: chương trình đã triển khai không thể nạp dữ liệu module Lean hay biên dịch mã mới lúc chạy.
• Yêu cầu chính xác Lean 4.35.0.
• Ứng dụng Node cần tối thiểu 512 MB RAM và chiếm khoảng 22 GB không gian địa chỉ ảo.
• Chưa hỗ trợ Windows ARM64 và máy biên dịch Alpine/musl.
• Số học với số nguyên lớn (hàng nghìn chữ số) chậm hơn Lean gốc do không dùng GMP.

Xây dựng bởi AI, định hướng bởi con người

Một chi tiết thú vị: tác giả tự mô tả mình là một "agentic engineer" chuyên về kỹ thuật phần mềm, và Lasm phần lớn được xây dựng bởi Claude Opus 5.5 dưới sự chỉ đạo cấp cao của con người. Điều này phản ánh xu hướng ngày càng rõ rệt khi các LLM trở thành công cụ hỗ trợ đắc lực cho việc phát triển phần mềm phức tạp.

Dự án được phát hành dưới giấy phép MIT, mã khởi đầu (template, ví dụ) dưới MIT-0 — nghĩa là hoàn toàn thuộc về người dùng, không cần ghi công. Tác giả hiện đang kêu gọi tài trợ qua GitHub Sponsors với mục tiêu đầu tiên là 250 USD/tháng.

Ý nghĩa với cộng đồng lập trình viên Việt Nam

Với các nhóm phát triển tại Việt Nam đang quan tâm đến độ tin cậy của phần mềm, đặc biệt trong các lĩnh vực như fintech, thanh toán hay hệ thống yêu cầu độ chính xác cao, Lasm mở ra một hướng tiếp cận mới: thay vì chỉ kiểm thử để phát hiện lỗi, có thể chứng minh hình thức rằng mã nguồn thỏa mãn đặc tả ngay từ giai đoạn biên dịch. Việc hỗ trợ sẵn Cloudflare Workers và nhiều nền tảng edge cũng phù hợp với xu hướng triển khai ứng dụng phân tán, độ trễ thấp mà nhiều startup công nghệ trong nước đang theo đuổi.

Tuy công nghệ này vẫn còn khá mới và có rào cản học tập nhất định, Lasm là minh chứng cho thấy kiểm chứng hình thức đang dần bước ra khỏi phòng nghiên cứu để trở thành công cụ thực tiễn cho lập trình viên ứng dụng web.