# Formal Verification with `ruchy provability`
**World's First**: Mathematical correctness guarantees built into a programming language.
## Overview
The `ruchy provability` tool provides formal verification capabilities that mathematically prove properties about your code. This revolutionary feature enables you to guarantee correctness, termination, memory safety, and other critical properties without external tools.
## Features
### Function Purity Analysis
Detects side effects and determines if functions are pure (deterministic, no side effects).
### Recursive Function Identification
Identifies recursive patterns and analyzes their complexity.
### Termination Proofs
Mathematically proves that loops and recursive functions terminate.
### Memory Safety Verification
Proves absence of array bounds violations and null pointer dereferences.
### Contract Verification
Verifies pre-conditions, post-conditions, and invariants.
## Usage
### Basic Analysis
```bash
# Basic provability analysis
ruchy provability script.ruchy
```
Output:
```
🔬 Provability Analysis for script.ruchy
Pure Functions: 8/10 (80%)
Recursive Functions: 2 detected
Provability Score: 85/100
✅ All functions verified to terminate
✅ No array bounds violations detected
⚠️ 2 functions have side effects
```
### Full Verification
```bash
# Complete formal verification
ruchy provability script.ruchy --verify --verbose
```
Output:
```
🔬 Full Formal Verification for script.ruchy
Function: fibonacci(n: u64) -> u64
✅ Pure: No side effects detected
✅ Termination: Proven via structural recursion
✅ Complexity: O(2^n) - exponential
📊 Provability: 100/100
Function: quicksort(arr: &mut [i32])
⚠️ Impure: Mutates input array
✅ Termination: Proven via decreasing measure
✅ Memory Safety: All array accesses verified safe
📊 Provability: 90/100
```
### Specific Verification Modes
```bash
# Verify contracts (pre/post conditions)
ruchy provability --contracts script.ruchy
# Check loop invariants
ruchy provability --invariants script.ruchy
# Prove termination
ruchy provability --termination script.ruchy
# Verify array bounds
ruchy provability --bounds script.ruchy
```
## Examples
### Example 1: Pure Function Verification
```ruchy
// Pure function - no side effects
fun add(x: i32, y: i32) -> i32 {
x + y
}
// Impure function - has side effects
fun print_sum(x: i32, y: i32) -> i32 {
let sum = x + y
println(f"Sum is {sum}") // Side effect!
sum
}
```
Analysis:
```bash
ruchy provability example.ruchy
```
Output:
```
Function 'add': ✅ Pure (100/100)
Function 'print_sum': ⚠️ Impure - I/O side effect detected (60/100)
```
### Example 2: Termination Proof
```ruchy
fun factorial(n: u64) -> u64 {
if n <= 1 {
1
} else {
n * factorial(n - 1)
}
}
fun countdown(mut n: i32) {
while n > 0 {
println(n)
n = n - 1
}
}
```
Verification:
```bash
ruchy provability --termination example.ruchy
```
Output:
```
✅ factorial: Termination proven
- Ranking function: n
- Decreases on each recursive call
- Base case: n <= 1
✅ countdown: Termination proven
- Loop variant: n
- Strictly decreasing: n = n - 1
- Termination condition: n <= 0
```
### Example 3: Memory Safety
```ruchy
fun safe_access(arr: [i32], index: usize) -> Option<i32> {
if index < arr.len() {
Some(arr[index])
} else {
None
}
}
fun unsafe_access(arr: [i32], index: usize) -> i32 {
arr[index] // Potential bounds violation!
}
```
Verification:
```bash
ruchy provability --bounds example.ruchy
```
Output:
```
✅ safe_access: Memory safe
- All array accesses guarded by bounds check
❌ unsafe_access: Potential bounds violation
- Line 8: arr[index] may exceed array bounds
- Suggestion: Add bounds check or use safe indexing
```
## Advanced Features
### Contract Specification
```ruchy
#[requires(n >= 0)]
#[ensures(result >= 1)]
fun factorial(n: u64) -> u64 {
if n == 0 {
1
} else {
n * factorial(n - 1)
}
}
```
### Loop Invariants
```ruchy
fun sum_array(arr: [i32]) -> i32 {
let mut sum = 0
let mut i = 0
#[invariant(sum == arr[0..i].sum())]
while i < arr.len() {
sum += arr[i]
i += 1
}
sum
}
```
## Output Formats
### JSON Output
```bash
ruchy provability script.ruchy --json
```
```json
{
"file": "script.ruchy",
"provability_score": 85,
"functions": [
{
"name": "fibonacci",
"pure": true,
"termination": "proven",
"complexity": "O(2^n)",
"score": 100
}
],
"issues": [],
"suggestions": []
}
```
### Report Generation
```bash
ruchy provability script.ruchy --output report.md
```
Generates a detailed Markdown report with:
- Executive summary
- Function-by-function analysis
- Identified issues
- Improvement suggestions
- Verification certificates
## Integration with CI/CD
```yaml
# GitHub Actions
- name: Formal Verification
run: |
ruchy provability src/ --verify --threshold 80
if [ $? -ne 0 ]; then
echo "Verification failed"
exit 1
fi
```
## Performance
- Basic analysis: <100ms for typical files
- Full verification: <500ms for complex functions
- Contract checking: <200ms
- Memory analysis: O(n) where n is number of array accesses
## Limitations
Currently, the provability tool:
- Cannot verify concurrent/parallel code
- Limited support for higher-order functions
- Requires explicit contracts for complex properties
- May timeout on very complex recursive functions
## Future Enhancements
- SMT solver integration for advanced proofs
- Concurrent program verification
- Refinement type support
- Automated invariant generation
- Integration with Coq/Isabelle
---
*Revolutionary formal verification - only in Ruchy v0.10.0*