Skolem: công cụ kiểm chứng câu lệnh SQL do AI sinh ra bằng Z3/SMT

Mục tiêu: Các công cụ AI thường sinh ra câu SQL trông đúng nhưng sai logic một cách âm thầm (ví dụ: LEFT JOIN bị đổi thành INNER JOIN làm mất dòng dữ liệu mà không báo lỗi). Skolem dùng bộ giải Z3 (SMT) để kiểm chứng và phát hiện những lỗi này. Công nghệ: Python, Z3/SMT solver, CLI, MCP server, REST API. Mình đã làm: - Xây dựng lõi kiểm chứng SQL bằng Z3, phát hiện lỗi logic trong câu SQL do AI sinh - Đóng gói thành nhiều dạng sử dụng: web workspace, công cụ dòng lệnh (CLI), MCP server và endpoint API để tích hợp vào CI - Ra mắt bản chạy được để người dùng thử Kết quả: Sản phẩm đã hoạt động, dùng được qua web, CLI, MCP và API trên cùng một bộ giải.