Skip to content

Commit eca25bf

Browse files
Jonathan D.A. Jewellclaude
Jonathan D.A. Jewell
and
claude
committed
chore: sync template files and configuration
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
1 parent 9fc0d0c commit eca25bf

1 file changed

Lines changed: 113 additions & 0 deletions

File tree

‎PROVEN-INTEGRATION.md‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
# Proven Library Integration Plan
2+
3+
This document outlines how the [proven](https://github.com/hyperpolymath/proven) library's formally verified modules integrate with the Next-Gen Languages ecosystem.
4+
5+
**Note:** Several Next-Gen Languages (especially Anvomidav and Duet) have formal verification as core features. The proven library provides shared verification infrastructure.
6+
7+
## Per-Language Integration
8+
9+
### Anvomidav (Formal Verification Focus)
10+
11+
| Module | Use Case | Formal Guarantee |
12+
|--------|----------|------------------|
13+
| `SafeThm` | Theorem statement management | Well-typed propositions |
14+
| `SafeLinear` | Linear type enforcement | Resource linearity |
15+
| `SafeSession` | Session type checking | Protocol conformance |
16+
| `SafeRealTime` | WCET analysis | Bounded execution time |
17+
18+
Anvomidav's type system directly corresponds to proven modules:
19+
- `Linear<T>` → SafeLinear
20+
- `Session<Protocol>` → SafeSession
21+
- `@sched(EDF)` → SafeRealTime
22+
23+
### Duet (AI-Assisted Verification)
24+
25+
| Module | Use Case | Formal Guarantee |
26+
|--------|----------|------------------|
27+
| `SafeProperty` | Property synthesis targets | Valid specifications |
28+
| `SafeThm` | AI-generated proof validation | Proof soundness |
29+
| `SafeOracle` | AI verification oracle | Trusted computation |
30+
31+
Duet's `@verify` and `@synth` annotations use proven as the verification backend.
32+
33+
### Phronesis (AI Ethics/Alignment)
34+
35+
| Module | Use Case | Formal Guarantee |
36+
|--------|----------|------------------|
37+
| `SafePolicy` | Ethical policy specification | Policy consistency |
38+
| `SafeConstraint` | Value constraint checking | Constraint satisfaction |
39+
| `SafeProvenance` | Decision audit trails | Accountability |
40+
41+
Phronesis agents use SafePolicy for ethical framework specification.
42+
43+
### Oblíbený (Secure Code)
44+
45+
| Module | Use Case | Formal Guarantee |
46+
|--------|----------|------------------|
47+
| `SafeBounded` | Turing-incomplete enforcement | Termination guarantee |
48+
| `SafeFlow` | Information flow control | No data leakage |
49+
| `SafeCrypto` | Cryptographic operations | Correct algorithm usage |
50+
51+
Oblíbený's `(forbid recursion)` maps to SafeBounded's termination proofs.
52+
53+
### Eclexia (Resource-Constrained)
54+
55+
| Module | Use Case | Formal Guarantee |
56+
|--------|----------|------------------|
57+
| `SafeResource` | Resource budget tracking | Budget compliance |
58+
| `SafeEnergy` | Energy consumption proofs | Bounded energy use |
59+
| `SafeMetric` | Resource metric validation | Valid measurements |
60+
61+
Eclexia's `(energy budget ...)` uses SafeEnergy for compile-time verification.
62+
63+
### Solo (Foundation Language)
64+
65+
| Module | Use Case | Formal Guarantee |
66+
|--------|----------|------------------|
67+
| `SafeContract` | Pre/post conditions | Contract satisfaction |
68+
| `SafeConcurrent` | Concurrency safety | Race-freedom |
69+
| `SafeEffect` | Effect tracking | Effect containment |
70+
71+
Solo's `where { pre: ..., post: ... }` uses SafeContract.
72+
73+
### Ensemble (AI-Native)
74+
75+
| Module | Use Case | Formal Guarantee |
76+
|--------|----------|------------------|
77+
| `SafeOracle` | AI model invocation | Trusted AI calls |
78+
| `SafeEffect` | AI effect isolation | Effect boundaries |
79+
| `SafeSchema` | Prompt validation | Well-formed prompts |
80+
81+
### WokeLang (Human-Centric)
82+
83+
| Module | Use Case | Formal Guarantee |
84+
|--------|----------|------------------|
85+
| `SafeConsent` | Consent tracking | Explicit consent |
86+
| `SafePrivacy` | Privacy enforcement | Data protection |
87+
| `SafeAccessibility` | A11y compliance | Accessibility checks |
88+
89+
## Shared Infrastructure
90+
91+
All Next-Gen Languages share these proven modules:
92+
93+
| Module | Shared Use Case |
94+
|--------|-----------------|
95+
| `SafeAST` | Common AST representation |
96+
| `SafeType` | Type system foundations |
97+
| `SafeCompile` | Compilation pipeline |
98+
| `SafeError` | Error handling patterns |
99+
100+
## Implementation Strategy
101+
102+
1. **Core types**: Define common types in proven (SafeAST, SafeType)
103+
2. **Per-language extensions**: Each language adds its specific modules
104+
3. **Shared backend**: Compile proven modules to target runtimes
105+
4. **Cross-language proofs**: Use proven as proof interchange format
106+
107+
## Status
108+
109+
- [ ] Define SafeAST for common representation
110+
- [ ] Implement SafeLinear for Anvomidav
111+
- [ ] Add SafePolicy for Phronesis
112+
- [ ] Integrate SafeBounded for Oblíbený
113+
- [ ] Create SafeEnergy for Eclexia

0 commit comments

Comments
 (0)