Vera: Ngôn ngữ lập trình được thiết kế riêng cho các Mô hình Ngôn ngữ Lớn (LLM)

Vera (phát âm là v-ERR-a) là một ngôn ngữ lập trình được thiết kế đặc biệt cho các Mô hình Ngôn ngữ Lớn (LLM) để viết code. Tên gọi bắt nguồn từ tiếng Latin "veritas" (sự thật). Các chương trình viết bằng Vera sẽ được biên dịch sang WebAssembly và có thể chạy trực tiếp trên dòng lệnh hoặc trình duyệt.

Vera Social Preview

Tại sao lại cần Vera?

Các ngôn ngữ lập trình luôn cùng tiến hóa cùng với người dùng. Assembly ra đời từ các ràng buộc phần cứng, C cho hệ điều hành, và Python cho nhu cầu năng suất. Tuy nhiên, nếu các mô hình AI trở thành tác giả chính của code, thì các ngôn ngữ cũng cần thích ứng để phục vụ chúng.

Bằng chứng cho thấy vấn đề lớn nhất mà các mô hình AI gặp phải không phải là cú pháp, mà là tính nhất quán trên quy mô lớn. Các mô hình thường gặp khó khăn trong việc duy trì các bất biến (invariants) trên toàn bộ codebase, hiểu được tác động lan truyền của các thay đổi, và lý luận về trạng thái theo thời gian. Chúng là những bộ khớp mẫu tối ưu hóa cho tính hợp lý cục bộ, chứ không phải là những kiến trúc sư nắm giữ toàn bộ hệ thống trong tâm trí.

Vera giải quyết vấn đề này bằng cách làm cho mọi thứ trở nên minh bạch và có thể kiểm chứng được. Mô hình không cần phải hoàn toàn đúng ngay lập tức, nó chỉ cần để có thể kiểm tra được.

Đặc điểm chính của Vera

Không có tên biến

Trong Vera, không tồn tại khái niệm đặt tên biến. Thay vào đó, ngôn ngữ này sử dụng các tham chiếu cấu trúc. Ví dụ, @Int.0 là liên kết Int gần nhất, và @Int.1 là liên kết trước đó. Điều này giúp loại bỏ các lỗi liên quan đến việc đặt tên sai hoặc nhầm lẫn biến mà AI thường mắc phải.

Hợp đồng bắt buộc (Mandatory Contracts)

Mọi hàm trong Vera đều phải khai báo các mệnh đề requires (điều kiện tiên quyết), ensures (điều kiện hậu kiểm) và effects (tác động). Trình biên dịch sẽ kiểm tra điều kiện tiên quyết tại mọi điểm gọi hàm, và một trình giải SMT (như Z3) sẽ chứng minh tĩnh điều kiện hậu kiểm.

Ví dụ về hàm chia an toàn:

public fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
ensures(@Int.result == @Int.0 / @Int.1)
effects(pure)
{
@Int.0 / @Int.1
}

Chia cho zero trong Vera không phải là lỗi runtime, mà là lỗi kiểu dữ liệu (type error). Nếu bất kỳ điều kiện nào sai, code sẽ không biên dịch được.

Tác động rõ ràng (Explicit Effects)

Vera mặc định là thuần túy (pure). Một hàm gọi LLM phải khai báo rõ ràng trong chữ ký của nó. Người gọi không cho phép tác động IO sẽ không thể gọi nó. Điều này giúp kiểm soát chặt chẽ các tác động phụ của chương trình.

Lỗi là hướng dẫn cho AI

Khác với các trình biên dịch truyền thống chỉ đưa ra thông báo lỗi cho con người, Vera tạo ra các hướng dẫn sửa lỗi dành riêng cho mô hình đã viết code đó. Mỗi lỗi bao gồm mô tả sai sót, lý do, cách sửa với ví dụ code cụ thể và tham chiếu đến tài liệu kỹ thuật.

Hiệu suất và Công nghệ

Vera hiện đang trong giai đoạn phát triển tích cực (phiên bản v0.0.127). Trình biên dịch tham chiếu được viết bằng Python, bao gồm trình phân tích cú pháp, kiểm tra kiểu, trình xác minh hợp đồng (sử dụng Z3), và trình tạo mã WebAssembly.

Một điểm nổi bật là VeraBench — một bộ chuẩn hóa gồm 50 vấn đề trên 5 cấp độ khó. Kết quả cho thấy mô hình Kimi K2.5 đạt 100% độ chính xác khi chạy trên Vera, đánh bại cả Python (86%) và TypeScript (91%). Điều này cho thấy tiềm năng lớn của Vera trong việc giảm thiểu lỗi do AI tạo ra.

Bắt đầu với Vera

Để sử dụng Vera, bạn cần Python 3.11+ và Git. Quy trình cài đặt và sử dụng khá đơn giản:

git clone https://github.com/aallan/vera.git
cd vera
python -m venv .venv
source .venv/bin/activate
pip install -e ".[dev]"

Bạn có thể kiểm tra, xác minh và chạy các tệp Vera bằng các lệnh như vera check, vera verify và vera run. Đặc biệt, vera compile --target browser có thể tạo ra một gói độc lập (wasm + JS runtime + HTML) chạy trên bất kỳ trình duyệt nào mà không cần bước build phức tạp.

Vera là một dự án mã nguồn mở dưới giấy phép MIT, hứa hẹn mở ra một hướng đi mới nơi con người thiết kế đặc tả và AI chịu trách nhiệm viết code dựa trên những ràng buộc chặt chẽ đó.