Inspiration
Inspired by the common core of the formal language Alloy and the industrial gold standard of database queries, SQL - Relational Algebra, we are trying to build a deterministic intermediate representation (IR) to bridge them in the Vibe Coding Era for AI to get RLVR scaffolding and generate more reliable SQL queries.
What it does
From a non-technical perspective, it completes such a workflow: an interactive agentic generation of SQL queries, a deterministic mapping to Alloy and SAT4J that finds out the behaviors of such queries, and a Graphviz showing its form and an AI-generated explanation, with a swipe - swipe left if you want this effect to disappear, swipe right if this is part of your intention.
How we built it
We (me and the Greatest Researcher of All Time, Proud Backscene Writer of up to 40K submissions to ICLR '27, Claudius G.P.T. Slopius) vibe-coded it based on prior work on Alloy, SQL, and Lean 4, formally verified the core, and built a frontend with AI agents.
Challenges we ran into
We started with a scraped 276-query real-life dataset covering different syntax. Covering all typed SQL queries in the Lean-proven shared intermediate representation took tens of agent hours on GPT-6 Astra.
Accomplishments that we're proud of
We are formally verified!
What we learned
Verifying the slop is costly but worth it.
What's next for SQLolla
We intentionally built it with a Rust backend that follows Clean Code principles and mandatory functional enclosure, with side-effect prevention, so it isn't one-time "throwaway code". It could cover more semantics over time.
Built With
- alloy
- gpt
- java
- javascript
- lean
- rust
- typescript
