sqlite3 vdbe formalization

Stream: new members

[Nikita Sivukhin]

Hi everyone!

I am very new to lean4 but since I learned about it I was always excited about possibility to apply verification methods to the real problems at my work.

I working very closely with SQLite last days and its virtual machine always looked like a good candidate for verification, because VM programs usually pretty short, so proof can be generated either manually or with LLM help. Also, as SQLite VM programs are guided by SQL queries - they are usually have simple shape, so that potentially manageable set of predefined tactics can prove different properties automatically for most of the cases.

As an attempt to move towards the goal of formalized SQLite VDBE I translated simple select query and proved it's termination. To expand the goal, I collected few more queries and created repo where proving progress can be tracked: https://github.com/sivukhin/sqlite3-lean-proofs

I will be glad to work on this more, but I am newbie in Lean. So, if anyone has some suggestions, want to join the effort or maybe there are some components which can help with this work - I will glad to hear this feedback!