Nguồn: Kiran Gopinathan’s blog
Tóm tắt
Formal verification được coi là công cụ mạnh nhất để đảm bảo tính đúng đắn của phần mềm — nếu một chương trình được Lean4 chứng minh là correct, về lý thuyết nó không thể có bug. Tuy nhiên, tác giả Kiran Gopinathan đã phát hiện ra một bug trong một stack implementation được formally verified, và bài viết này kể lại quá trình tìm bug đó.
Câu chuyện bắt đầu từ một bài viết trên HackerNews về cách viết formally verified code bằng Lean4. Tác giả đọc kỹ implementation và nhận ra một vấn đề tiềm ẩn: chứng minh chỉ xác nhận rằng code thực hiện đúng theo spec — nhưng nếu spec bản thân nó sai thì sao?
Đây là bài học cốt lõi về giới hạn của formal verification: công cụ này chỉ chứng minh code đúng với specification được cung cấp, không chứng minh specification đúng với intent thực sự của developer. Một buggy spec dẫn đến buggy code được “certified correct”. Khoảng cách giữa “what we wrote” và “what we meant” vẫn là lỗ hổng mà formal methods không thể tự động lấp đầy.
Bài viết nhấn mạnh tầm quan trọng của việc kiểm tra spec kỹ lưỡng ngoài code — specification testing, property-based testing, và review thận trọng vẫn là bước không thể bỏ qua ngay cả khi sử dụng formal verification.