- --

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.