Apodeixis.jl

Table of Contents

• What exists today
• Quick start
• Design and implementation
• Development status
• License

Apodeixis.jl is an early-stage Julia verification toolchain project. Its goal is to connect Julia source contracts and compiler-specialized code with explicit numeric semantics, memory/FFI proofs, and independently checked proof certificates. The long-term design targets JuliaSyntax.jl, typed SSA from code_typed / Core.Compiler, and an Idris2 + Zig boundary integrated with Why3/SMT, Dedukti, Coq, and Lean.

Important

Verification status: the current executable is a source-policy audit, not a formal verifier. A POLICY CLEAN result does not prove a contract, bounds safety, type stability, allocation behavior, ABI correctness, or functional safety. The typed-SSA analysis, VC generation, solver integration, and Warrant-to-Receipt pipeline are planned work, not implemented features.

What exists today

• A Julia package using JuliaSyntax.jl to parse source without expanding or executing user macros.

• A fail-closed policy audit for selected unsafe constructs, unmodeled foreign calls, unknown macros in @verified functions, and @inbounds placement.

• A CLI at scripts/apodeixis.jl and focused package tests.

• Architecture and implementation-plan documents describing the intended frontend, numeric tiers, array/FFI seam, proof evidence, and staged roadmap.

• Idris2 ABI and Zig build scaffolding under src/interface/; these are starting points, not yet a complete, target-validated Julia FFI proof seam.

Quick start

Julia 1.9 or newer is declared in the package compatibility bounds. Runtime validation of the package is pending; see the implementation plan.

julia --project=. -e 'using Pkg; Pkg.instantiate()'
julia --project=. -e 'using Pkg; Pkg.test()'
julia --project=. scripts/apodeixis.jl --help
julia --project=. scripts/apodeixis.jl audit path/to/source.jl

For a source file containing @inbounds, the initial policy checker also requires a mutation-score percentage:

julia --project=. scripts/apodeixis.jl audit --mutation-score 97.5 path/to/source.jl

This caller-supplied percentage currently satisfies only a policy gate. It is not authenticated test evidence and does not discharge a bounds verification condition. @inbounds remains unverified until the planned typed-SSA and VC passes exist.

Design and implementation

• Verification architecture — hybrid frontend, four numeric tiers, memory discipline, FFI seam, worked example, and proof lifecycle.

• MVP implementation plan — existing package slice, ordered implementation work, and acceptance gates.

• Ultra-plan — dependency-ordered work packages, acceptance gates, risks, and contributor handoff protocol.

• ABI interface scaffolding — current Idris2 ABI files and their limitations.

The numeric design keeps mathematical integers/rationals, fixed-width bitvectors, strict IEEE-754 values, and probabilistic evidence separate. Statistical warrants are never treated as deterministic functional-safety proofs. Full details and unsupported boundaries are recorded in the design document.

Development status

This is research-stage software with an intentionally narrow first slice. Julia package tests have been added but must be run in a Julia-enabled environment before the package is treated as runtime-validated. Each implementation phase must add adversarial negative tests and preserve explicit UNKNOWN / UNSUPPORTED outcomes; tests, JET reports, mutation scores, and benchmarks are evidence and gates, not formal proofs.

License

Code and configuration are licensed under MPL-2.0. Documentation is licensed under CC-BY-SA-4.0. See LICENSE and the texts under LICENSES/.