PolyglotFormalisms.jl

PolyglotFormalisms.jl

Cross-Language Formal Verification in Julia

Julia reference implementation of aggregate-library with formal verification, designed for cross (programming) language verification.

What is PolyglotFormalisms.jl?

PolyglotFormalisms.jl is a Julia-based framework for building and verifying formal specifications across multiple programming languages. It enables:

• Cross-language formal verification: Prove properties about code written in different languages.

• Aggregate library design: Reuse verified components across Julia, Idris2, Zig, and more.

• ABI/FFI standards compliance: Seamless integration with foreign function interfaces.

• Mathematical guarantees: Compile-time proofs for memory safety, type correctness, and interface compliance.

using PolyglotFormalisms

# Define a verified interface
@formal interface SafeDOM
    function mount(element::String, content::String) :: Bool
        @ensure element ≠ "" && content ≠ ""
        @prove ∀x. mount(x, "") == false
    end
end

# Generate bindings for other languages
generate_bindings(SafeDOM, languages=[:zig, :idris])

Features

Cross-Language Verification

Verify properties across language boundaries:

@formal contract SafeMemory
    function allocate(size::Int) :: Ptr
        @ensure size > 0
        @prove ∀s. s > 0 ⇒ allocate(s) ≠ C_NULL
    end
end

# Generate Idris2 and Zig bindings
generate_abi(SafeMemory, "memory_abi.h")

ABI/FFI Standards

All foreign function interfaces follow the Hyperpolymath Universal Standard:

• Idris2: Type definitions with dependent type proofs.

• Zig: C-compatible, memory-safe implementations.

• Auto-generated C headers: Bridge between Idris2 and Zig.

Directory Structure

project/
├── src/abi/          # Idris2 ABI definitions
├── ffi/zig/          # Zig FFI implementation
├── generated/abi/    # Auto-generated C headers
└── bindings/         # Language-specific wrappers

AI CLI Integration

• Use ai-cli-crash-capture/ for automated verification.

• Mirror 6SCM files into .machine_readable/.

• Check /var$REPOS_DIR/proven for "unbreakable" Idris libraries.

Quick Start

Installation

using Pkg
Pkg.add("PolyglotFormalisms")

Hello World

using PolyglotFormalisms

# Define a verified interface
@formal interface MathOps
    function add(a::Int, b::Int) :: Int
        @ensure add(a, b) == a + b
    end
end

# Generate bindings
generate_bindings(MathOps, languages=[:zig])

Why PolyglotFormalisms.jl?

The Problem

Cross-language projects often suffer from: - Undetected memory errors - Type mismatches at runtime - Unverified foreign function interfaces

The Solution

PolyglotFormalisms.jl provides: | Issue | Traditional FFI | PolyglotFormalisms.jl | |----------------------|-----------------|-----------------------| | Memory safety | Runtime crashes | Compile-time proofs | | Type correctness | Manual checks | Dependent types | | Interface compliance | Ad-hoc testing | Formal verification |

Project Structure

PolyglotFormalisms.jl/
├── src/               # Julia source
│   ├── abi/          # ABI definitions
│   ├── ffi/           # FFI implementations
│   └── verification/  # Proof system
├── generated/         # Auto-generated headers
└── bindings/          # Language wrappers

Roadmap

• ✅ v0.1: Core framework, Idris2/Zig integration

• ⬜ v0.2: Expanded language support (Rust, ReScript)

• ⬜ v0.3: Advanced proof automation

• ⬜ v1.0: Industry-ready certification

Acknowledgments

Built on: - Idris2 for dependent types - Zig for memory safety - Julia for expressive DSLs