• --

title: About AXEL Protocol description: Attested eXecution Language - Formally verified protocol execution author: Jonathan D.A. Jewell date: 2026-01-30

• --

AXEL Protocol

Attested eXecution Language - A formally verified protocol for attested execution with mathematical guarantees.

What is AXEL?

AXEL is a protocol execution language with formal verification guarantees. Every execution is:

• Attested - Cryptographically signed proof of execution
• Verified - Formally proven correct at compile-time
• Traceable - Complete audit trail of all operations
• Type-safe - Idris2 dependent types prevent runtime errors

Core Concepts

Attested Execution

Every protocol execution generates an attestation - a cryptographic proof that:

• The protocol was executed correctly
• All inputs were validated
• All outputs are type-safe
• The execution trace is complete

Formal Verification

AXEL uses Idris2 dependent types to prove:

```idris data ValidProtocol : String -> Type where MkValidProtocol : (proto : String) -> {auto 0 wellFormed : So (isWellFormedProtocol proto)} -> {auto 0 typesSafe : So (allTypesSafe proto)} -> ValidProtocol proto ```

Properties Proven:

• Protocol well-formedness
• Type safety of all operations
• Memory safety (no buffer overflows)
• No null pointer dereferences

Protocol Validation

Before execution, AXEL validates:

• Domain validation - Domains are well-formed
• Port validation - Ports are in valid range (1-65535)
• Method validation - HTTP methods are valid
• URL validation - URLs are proven safe with ProvenSafeUrl

Execution Attestation

After execution, AXEL generates:

```json { "attestation_id": "550e8400-e29b-41d4-a716-446655440000", "protocol": "https", "domain": "example.com", "executed_at": "2026-01-30T20:00:00Z", "signature": "3045022100...", "proof": "Type-level proof included" } ```

Architecture

TEA (The Elm Architecture)

AXEL uses The Elm Architecture for predictable state management:

``` User Action → Message → Update → New Model → View ```

All state transitions are pure functions with no side effects.

Three-Layer Validation

1. Syntax - Nickel contracts validate structure 2. Semantics - ReScript validates business logic 3. Proofs - Idris2 proves correctness

Use Cases

API Protocol Verification

• Validate REST API calls before execution
• Generate attestations for audit trails
• Prove API calls were executed correctly

Smart Contract Execution

• Execute contracts with formal guarantees
• Prevent reentrancy and overflow attacks
• Generate cryptographic proofs of execution

Distributed Systems

• Coordinate distributed protocols
• Verify message ordering and delivery
• Attest to system state transitions

Compliance & Auditing

• Generate audit-ready execution logs
• Cryptographically prove compliance
• Maintain tamper-proof execution records

Features

• Formally Verified - Idris2 proofs at compile-time
• Attested Execution - Cryptographic proofs of correctness
• Type-Safe - Dependent types prevent errors
• Protocol Agnostic - HTTP, WebSocket, gRPC, custom protocols
• Audit Trail - Complete execution trace
• Memory Safe - No buffer overflows possible

Example

```axel protocol { domain: "api.example.com", port: 443, method: GET, path: "/users/123", attestation: required } ```

Compile-time guarantees:

• Domain is well-formed
• Port is in valid range (1-65535)
• Method is valid HTTP method
• Path is a valid URL path

Runtime attestation:

• Execution trace
• Cryptographic signature
• Timestamp
• Result validation

Learn More

• AXEL Specification
• Proven Library
• Idris2 Documentation
• ReScript TEA

• --

AXEL Protocol - Execution you can prove.