aletheia

README

Aletheia (Ἀλήθεια)

Formally verified CAN frame analysis with Linear Temporal Logic

Aletheia provides mathematically proven tools for verifying automotive software by applying Linear Temporal Logic (LTL) over traces of CAN frames.

Features

• Formally Verified: Core logic implemented in Agda with correctness proofs — eliminates signal extraction bugs entirely, not just for tested inputs
• CAN Frame Processing: Proven correct encoding/decoding guarantees roundtrip correctness for valid DBC specifications
• LTL Verification: Streaming model checker with O(1) memory — verified 1.08× growth across a 100× trace increase. Single-bus streaming tops out in the six-figure-fps range on the C++ binary FFI path; see PROJECT_STATUS.md § Key Metrics for the per-binding / per-lane / per-property-shape throughput table and methodology.
• Four Interface Tiers: Check API (engineers), YAML (CI/CD), Excel (technicians), and full LTL DSL (developers) — choose the level that fits your team
• Python, C++, and Go Interfaces: All run in-process via shared library (ctypes/dlopen FFI) — no subprocess, no IPC overhead
• Verified DBC Parsing: Agda parser with a universal roundtrip theorem (∀ d → WellFormedDBC d → parseText (formatText d) ≡ inj₂ d); handles multiplexed signals, 29-bit IDs, signed integers, value tables, attributes, environment variables, and comments. Exercised by an 8-fixture cross-binding corpus under python/tests/fixtures/dbc_corpus/ (covering 21 IssueCode validation rejections; see PROTOCOL.md § Error Code Reference)

Quick Start

Installation

# Quick build (see BUILDING.md for detailed instructions)
cabal run shake -- build

For complete build instructions, troubleshooting, and development workflow, see Building Guide.

Command-line usage (no Python required)

The fastest way to run checks — no code to write. After installing, run aletheia from any shell against a CAN log:

# Run YAML/Excel-defined checks against a recorded trace
aletheia check --dbc vehicle.dbc --checks checks.yaml drive.blf

# Other subcommands: validate a DBC, extract one frame, list signals, …
aletheia validate --dbc vehicle.dbc
aletheia signals --dbc vehicle.dbc

Exit code 0 = all checks passed, 1 = violations found, 2 = error. Full subcommand + flag reference: CLI Guide.

Basic Usage

Which style should I use? New users should start with the Check API or YAML/Excel loaders shown under Higher-Level Interfaces below — they cover the common cases. The raw DSL (Signal, set_properties) shown here is the escape hatch for full LTL control (e.g., metric operators, custom predicates). See the Interface Guide for an end-to-end comparison.

from aletheia import AletheiaClient, Signal
from aletheia.dbc import dbc_to_json
from aletheia.can_log import iter_can_log  # installed via `pip install aletheia[can]`

# Load DBC specification (converts .dbc to JSON)
dbc_json = dbc_to_json("vehicle.dbc")

# Define temporal properties using fluent DSL (raw LTL)
speed_limit = Signal("Speed").less_than(220).always()
brake_check = Signal("BrakePressed").equals(1).eventually()

# Stream CAN frames from a .blf / .asc / .log / .mf4 trace and check properties.
# iter_can_log() yields CANFrameTuple(timestamp_us, can_id, dlc, data, extended,
# brs, esi) — seven fields. timestamp_us is microseconds (int), can_id is the
# raw 11- or 29-bit arbitration ID, dlc is the DLC code (0–8 for CAN 2.0B, 0–15
# for CAN-FD), data is bytes/bytearray of length dlc_to_bytes(dlc), extended is
# True for 29-bit IDs, brs/esi are CAN-FD Bit Rate Switch / Error State
# Indicator (None on CAN 2.0B frames). The unpack below ignores the trailing
# three fields for brevity.
with AletheiaClient() as client:
    client.parse_dbc(dbc_json)
    client.set_properties([speed_limit.to_dict(), brake_check.to_dict()])
    client.start_stream()

    for timestamp_us, can_id, dlc, data, _extended, _brs, _esi in iter_can_log("drive.blf"):
        response = client.send_frame(timestamp_us, can_id, dlc, data)
        # A frame that produces verdicts returns a property_batch envelope;
        # each fails entry is a violation. timestamp is an int (microseconds).
        if response.get("type") == "property_batch":
            for entry in response["results"]:
                if entry.get("status") == "fails":
                    print(f"Violation at {entry['timestamp']}us")

    client.end_stream()

See Python API Guide for the complete DSL reference.

Higher-Level Interfaces

For users who don't need full LTL control, Aletheia provides three higher-level interfaces that compile to the same verified core (recommended entry point for new users):

from aletheia import checks, load_checks, load_checks_from_excel

# Check API — industry vocabulary
checks.signal("Speed").never_exceeds(220)
checks.when("BrakePedal").exceeds(50).then("BrakeLight").equals(1).within(100)

# YAML — declarative config files
check_list = load_checks("checks.yaml")

# Excel — spreadsheet templates for technicians
check_list = load_checks_from_excel("checks.xlsx")

See Interface Guide for end-to-end workflows.

Signal Operations

AletheiaClient also provides signal extraction and frame building:

with AletheiaClient() as client:
    client.parse_dbc(dbc_json)

    # Build a frame from signal values
    frame = client.build_frame(can_id=0x100, dlc=8, signals={"Speed": 72.0})

    # Extract signals from a frame
    result = client.extract_signals(can_id=0x100, dlc=8, data=frame)
    speed = result.get("Speed")  # Fraction(72) — extraction values are exact Fractions

    # Update specific signals in a frame
    modified = client.update_frame(can_id=0x100, dlc=8, frame=frame, signals={"Speed": 130.0})

Async client and lazy iter

For asyncio code, aletheia.asyncio.AletheiaClient mirrors the sync surface as async def methods, cancellable via asyncio.CancelledError. Both clients expose send_frames_iter for processing frames lazily one at a time — useful when the source is a live producer (queue, socket, generator) and full materialization is wasteful or impossible.

import asyncio
from aletheia.asyncio import AletheiaClient

async def watch(timeout_s: float):
    async with AletheiaClient() as client:
        await client.parse_dbc(dbc_json)
        await client.set_properties([prop.to_dict()])
        await client.start_stream()
        try:
            async with asyncio.timeout(timeout_s):
                async for r in client.send_frames_iter(live_frames()):
                    if r.violation is not None:
                        handle(r.violation)
        except TimeoutError:
            pass  # committed prefix is durable
        await client.end_stream()

See Cancellation contract for the behavioral parity guarantees Python / Go / C++ all share.

Project Structure

aletheia/
├── src/Aletheia/        # Agda core (formal verification)
├── haskell-shim/        # Minimal I/O layer
├── include/             # C header (aletheia.h)
├── python/              # Python API
├── cpp/                 # C++23 binding
├── go/                  # Go binding
├── benchmarks/          # Cross-language benchmarks
├── docs/                # Documentation
└── examples/            # Sample DBC files and demos

Documentation

📚 Complete Documentation Index - Full navigation guide

Getting Started

• Tutorials - End-to-end walkthroughs by role (start here if new to Aletheia)
• Quick Start - 5-minute walkthrough (assumes built library)
• Building Guide - Setup and installation

Guides

• Cookbook - Problem-driven recipes

Reference

• Interface Guide - Check API, YAML, Excel loaders
• Python API Guide - Raw DSL and AletheiaClient reference
• C++ API Guide - AletheiaClient, Check API, and the ltl:: DSL
• Go API Guide - Client, Check API, and the LTL DSL
• CLI Reference - aletheia subcommands

Architecture & Design

• Design Overview - Three-layer architecture
• JSON Protocol - Low-level protocol specification
• Cancellation Contract - Cross-binding cancellation semantics
• cgo Notes - Go binding's cgo + dlopen rationale

Operations

• Runbook - Symptom → cause → action
• Stability Bench - RSS / FD drift detection
• Mutation Testing - Per-binding mutation testing

Development

• Local CI - Three-layer CI architecture
• Release Guide - Tag / sign / publish procedure
• Parity Plan - Cross-binding feature parity roadmap

Contributing

• Contributing Guide - How to contribute
• CLAUDE.md - AI-assisted development
• Project Status - Current phase and roadmap
• CHANGELOG - Public-API change log

Additional

• Project Pitch - Why Aletheia?
• Examples - Sample DBC files and demos

Project Status

Current Phase: See PROJECT_STATUS.md for current phase and detailed status

Complete information on deliverables, quality gates, and roadmap available in PROJECT_STATUS.md.

Contributing

Contributions are welcome! Please read CONTRIBUTING.md to understand what kinds of contributions belong upstream, extension points for customization, and submission guidelines.

License

This project is licensed under the BSD 2-Clause License. See LICENSE.md for details.

License Philosophy

BSD 2-Clause was chosen to allow broad adoption (including proprietary use) while encouraging collaboration through architecture and process rather than legal compulsion.

Etymology

Aletheia (Ἀλήθεια) - Greek for "truth" or "disclosure". In philosophy, it represents the uncovering or revealing of truth, which aligns with our goal of formally verifying correctness.