sly-probe 🔬🛰️

Language-agnostic code verification at microscopic resolution.

sly-probe is a universal code analysis and formal verification engine powered by LLMs and formal backends like Dafny, Lean4, and Coq. It bridges the gap between practical static analysis tools like mypy and rigorous proof assistants—providing developers with an extensible, modular, and programmable verification interface across all major programming languages.

Think of it as mypy++ for every language—with a ghost-mode microscope.

---

🧠 What It Does

• 🚀 Analyze code for security issues, runtime safety, undefined behavior, and logical gaps
• 📜 Extract and verify pure, total functions via formal methods (Dafny, Lean4, etc.)
• 🔍 Lint with purpose — structured output like UV201: division by zero, UV401: UB: pointer aliasing
• 🧩 Works with anything — Rust, Python, Ada, C/C++, TypeScript, etc.

---

📦 Features

• Multi-language support via Tree-sitter and LLM parsing
• Contract suggestion and verification with formal tool backends
• Security + runtime + logical consistency analysis in one CLI
• Configurable via toml or CLI flags
• Pluggable verification engines (--tools=dafny, lean4, coq)
• LLM + caching engine to reduce redundant runs

---

🚀 Examples

# Comprehensive check (like a super-linter)
sly check src/

# Extract and verify a pure Rust function using Dafny
sly verify src/safe_sort.rs --tool=dafny

# Run UB detection on a C codebase
sly check src/ --analysis=ub --languages=c,cpp

# Focused input validation scan for web code
sly check src/ --focus=input-validation

---

📂 Repository Structure

examples/
├── rust/
│   ├── safe_sort.rs
│   ├── generated_dafny.dfy
│   └── verify.sh
├── ada_spark/
│   ├── abs.ads
│   ├── abs.adb
│   ├── abs_exported.dfy
│   └── verify.sh

---

🎯 Analysis Categories

Code	Category	Example
UV0xx	Specification gaps	Missing pre/post conditions, loop invariants
UV1xx	Security vulnerabilities	SQL injection, unsafe crypto, XSS
UV2xx	Runtime safety	Division by zero, out-of-bounds
UV3xx	Error handling	Missing try/catch, ignored return values
UV4xx	Undefined behavior	Pointer aliasing, UB in release builds
UV5xx	Domain consistency	Float in discrete math, type-domain mismatch

---

⚗️ Philosophy

sly-probe treats code like a living system:

• Types are telescope resolution (mypy)
• Proofs are microscope resolution (sly)
• With annotations and contracts as your lens settings

It’s backwards-compatible with legacy code, forward-compatible with formal methods, and written to scale across industries—from indie projects to aerospace.

---

📚 Coming Soon

• VS Code plugin
• Inferred contract suggestion mode
• Reverse-verification loop (Dafny → SPARK reconstructor)
• Domain-specific plugins (e.g., cryptographic checks, embedded-safety mode)

---

🧠 Credits

Inspired by:

• Dafny
• SPARK Ada
• Rust + Prusti
• [Coq, Lean, Lean4]
• Star Control II's Slylandro Probe 🛰️

---

🛸 License

MIT, GPL, or GPL unless you're Ur-Quan.

---

🤖 Try It

pip install sly-probe  # (or cargo install, or pipx run once ready)
sly check your_code/

---

“Never send a human to do a proof assistant’s job.” — sly