Verified execution bridging traditional code and LLM-native runtimes
Vesper enables a future where software is developed at the intent level rather than implementation level. It provides:
- Semantic Specification: A high-level, LLM-native way to express software behavior
- Dual-Path Execution: Run the same semantic specification through both proven Python implementations and experimental optimized runtimes
- Gradual Migration: Shift from traditional code to direct execution based on empirical verification
- Verification-First: Prove correctness through differential testing before trusting new implementations
Current software development is constrained by human-centric programming languages designed decades ago. As LLMs become capable of understanding intent directly, we need representations optimized for:
- LLM reasoning - Semantic graphs, contracts, and capabilities rather than imperative code
- Automatic optimization - Runtimes that can reoptimize based on actual behavior
- Formal verification - Provable correctness through contracts and properties
- Evolution - Systems that adapt without manual refactoring
But we can't abandon proven technology. We need a hedged bet: maintain traditional implementations while building toward an LLM-native future.
┌─────────────────────────┐
│ Vesper Spec (.vsp) │ ← Single source of truth
│ Intent + Contracts │
└────────────┬────────────┘
│
┌─────────┴─────────┐
│ │
▼ ▼
┌──────────────┐ ┌──────────────┐
│ Python Path │ │ Direct Path │
│ (Proven) │ │ (Optimized) │
└──────┬───────┘ └──────┬───────┘
│ │
└────────┬────────┘
▼
┌─────────────────┐
│ Verification │ ← Compare outputs
│ Dashboard │
└─────────────────┘
- ✅ Write intent, not implementation - Express what you want, not how to do it
- ✅ Automatic verification - Both paths must produce identical outputs
- ✅ Gradual migration - Start Python-only, migrate to direct runtime as confidence grows
- ✅ Confidence-based routing - Route traffic based on empirical reliability
- ✅ Rich debugging - Debug at semantic level across both runtimes
- ✅ Performance visibility - Know exactly how much faster the optimized path is
Current Phase: initializing
- Architecture design
- Vesper specification v0.1
- Python code generator (in progress)
- Direct runtime core (planned)
- Differential testing framework (planned)
- First production deployment (planned)
- Architecture Overview - System design and dual-path execution
- Vesper Specification - Complete format reference
vesper/
├── README.md # This file
├── docs/ # Documentation
│ ├── ARCHITECTURE.md
│ ├── VESPER_SPEC.md
├── spec/ # Vesper format definitions
│ ├── v0.1/
│ │ ├── schema.json
│ │ └── examples/
├── python/ # Python implementation
│ ├── vesper_compiler/ # Vesper → Python code generator
│ ├── vesper_runtime/ # Python execution runtime
│ └── tests/
├── rust/ # Direct runtime (Rust)
│ ├── vesper_core/ # Core semantic interpreter
│ ├── vesper_jit/ # JIT compiler
│ └── tests/
├── tools/ # CLI and utilities
│ ├── cli/ # `vesper` command-line tool
│ ├── dashboard/ # Web UI for verification
│ └── profiler/ # Performance analysis
├── examples/ # Example semantic nodes
│ ├── hello_world/
│ ├── payment_handler/
│ └── data_pipeline/
└── tests/
├── differential/ # Differential testing
├── integration/
└── property/ # Property-based tests
We welcome contributions! This is a research project exploring the future of software development.
See CONTRIBUTING.md for guidelines.
- 🔨 Python code generator - Converting Vesper to idiomatic Python
- 🦀 Rust runtime - Building the direct execution path
- 🧪 Testing frameworks - Differential and property-based testing
- 📚 Documentation - Examples, tutorials, best practices
- 🎨 Tooling - IDE plugins, debuggers, visualizations
This project explores several open questions:
- Can LLMs reason more effectively with semantic specifications than traditional code?
- What's the performance overhead of semantic interpretation vs JIT compilation?
- At what confidence threshold can we safely migrate from Python to direct runtime?
- How do we maintain debuggability without human-readable code?
- Can semantic specifications enable automatic optimization based on runtime behavior?
- LLVM IR - Proven intermediate representation for compilers
- WebAssembly - Portable compilation target with security properties
- TLA+ - Formal specification language for distributed systems
- Dafny - Verified programming language
- NormCode - Semi-formal language for AI planning
MIT License - see LICENSE for details.
If you use this work in research, please cite:
@software{vesper_framework,
title = {Vesper: Verified Execution Framework for LLM-Native Software},
author = {Witlox},
year = {2025},
url = {https://github.com/witlox/vesper}
}- GitHub: github.com/witlox/vesper
- Issues: GitHub Issues
- Discussions: GitHub Discussions
Vesper - Guiding the transition from traditional to LLM-native software development