Savvi Studio

Formal Verification

Status: 📋 Future Research Project
Last Updated: 2024-11-28

Overview

Formal verification of the codegen type system is a long-term research goal that would provide mathematical certainty about PostgreSQL to Zod type conversions.

Project Location

This research project has been set up in Forge:

→ docs/forge-home/formal-verification/

The project includes:

  • Detailed research plan
  • Task breakdown
  • Reference documentation on type algebra
  • Coq formalization approach

Why a Separate Project?

This is exploratory research work that:

  • Requires 4-6 weeks of dedicated effort
  • Involves formal proof assistants (Coq/Agda)
  • Is not required for production use
  • May be completed as a research publication

Current Status

The current codegen implementation provides practical type safety without formal proof, which is sufficient for most use cases.

For research details, see: docs/forge-home/formal-verification/