---
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](https://github.com/hyperpolymath/axel-protocol)
- [Proven Library](https://github.com/hyperpolymath/proven)
- [Idris2 Documentation](https://idris2.readthedocs.io/)
- [ReScript TEA](https://github.com/hyperpolymath/rescript-tea)

---

*AXEL Protocol - Execution you can prove.*
