The README makes claims. This file backs them up.
Phronesis is a neuro-symbolic, agentic language designed to formalize ethical reasoning in autonomous systems. It fuses the precision of Symbolic AI with the adaptability of neural networks, enforcing provable safety and fault tolerance through a dedicated BEAM VM runtime.
Phronesis is a compiled policy language, not a library. The pipeline is:
source text → Phronesis.Lexer → Phronesis.Parser → AST → Phronesis.Compiler
→ bytecode (.phrc files) → Phronesis.Interpreter. The Elixir implementation
lives in lib/phronesis/. The language has 15 keywords including ACCEPT,
REJECT, REPORT, and EXECUTE, plus probabilistic type literals
(BeliefFunction, ProbabilityDistribution) and a mandatory REPORT action
for flagging model-reality inconsistencies (the "map-territory mandate"). Running
on the BEAM gives fault tolerance via OTP supervisor trees.
OTP Design Principles
Caveat: The production Rust/BEAM compiler is Phase 2 roadmap. The current
implementation is the Elixir prototype. Probabilistic types are represented as
runtime values, not statically checked by the type checker at this stage.
Consensus (Raft) is a TLA+ spec in formal/ and a skeleton in
lib/phronesis/consensus/; it is not yet a deployable runtime.
-
Lexer:
lib/phronesis/lexer.ex -
Parser:
lib/phronesis/parser.ex,lib/phronesis/parser/ -
Type checker:
lib/phronesis/type_checker.ex -
Compiler:
lib/phronesis/compiler.ex -
Interpreter:
lib/phronesis/interpreter.ex -
Learn more: https://en.wikipedia.org/wiki/Phronesis
BEAM/Raft Architecture: BEAM VM + Raft consensus for ethical loop execution. Ensures fault-tolerant, distributed reasoning.
formal/PhronesisConsensus.tla is a TLA+ specification of the Raft-based
consensus protocol for multi-node Phronesis execution. formal/PhronesisConsensus.cfg
is the TLC model checker configuration. These are model-checked artefacts, not
executable code, but they are the authoritative spec from which the
lib/phronesis/consensus/ Elixir implementation derives.
TLA+
Caveat: The Elixir consensus implementation in lib/phronesis/consensus/
is a scaffold. The TLA+ spec has not been formally published or independently
reviewed.
-
Spec:
formal/PhronesisConsensus.tla -
Config:
formal/PhronesisConsensus.cfg -
Implementation:
lib/phronesis/consensus/ -
Test:
test/consensus_test.exs
Strong Static Typing: Prevents runtime errors in safety-critical systems.
lib/phronesis/incremental_lexer.ex and lib/phronesis/incremental_parser.ex
support re-parsing only the changed portion of a document — the critical path
for the LSP integration. The incremental infrastructure feeds lib/phronesis/lsp/
which provides hover, completion, and diagnostics to editors. Incremental
correctness is verified in test/incremental_lexer_test.exs and
test/incremental_parser_test.exs.
Caveat: Incremental reparsing is bounded by expression boundaries. Edits spanning multiple top-level policy blocks still trigger a full re-parse.
-
Implementation:
lib/phronesis/incremental_lexer.ex,lib/phronesis/incremental_parser.ex -
LSP:
lib/phronesis/lsp/ -
Tests:
test/incremental_lexer_test.exs,test/incremental_parser_test.exs,test/lsp_integration_test.exs
Running all ethical scenarios is the definitive measure of correctness.
lib/phronesis/stdlib/ provides the built-in policy predicates and ethical
reasoning primitives. lib/phronesis/library/ contains reusable policy modules.
lib/phronesis/package_manager.ex and lib/phronesis/package_manager/ implement
a Phronesis-native package system for distributing policy modules. The conformance
test suite in test/conformance_test.exs and conformance/ exercises the
mandatory ethical scenario set.
Caveat: The package registry is local-only. There is no hosted registry or cryptographic signing for packages yet.
-
Standard library:
lib/phronesis/stdlib/ -
Package manager:
lib/phronesis/package_manager.ex,lib/phronesis/package_manager/ -
Conformance suite:
conformance/,test/conformance_test.exs
Reflexion Design Layer: Judgement-Evidence Graph + Invariant-Path Equivalence Engine that records why a design is valid and gates regressions.
lib/phronesis/reflexion/ turns compiler, runtime, and proof artefacts into
explicit claims, records why a design is considered valid, compares
justification-paths across versions, and emits design obligations that gate
changes — without ever auto-mutating the language’s semantics. The pipeline is
Build → Extract → Graph → Compare → Classify → Reevaluate → Gate, exposed via
the Phronesis.Reflexion.review/2 façade (Phronesis.Reflexion.demo/0 runs the
worked example).
The anchor example: ClaimExtractor emits a :safety_preservation claim
("policy P preserves REPORT-adequacy") whenever a policy’s action subtree
contains a {:report, _} node (the map-territory mandate, real in ast.ex).
A later version that drops that REPORT step classifies as :weakening, which
gates the change with a prove / mark-intentional / reject obligation. Two policy
strings in → classification + obligation + hash-chained ledger entry out.
Caveat: The equivalence engine is heuristic. The formal invariant-path
equivalence check is stubbed and currently falls through to :unresolved;
compiler/proof/bench ingestion beyond the AST walk is # TODO. Reflexion is a
called library (like Analyzer), not part of the OTP supervision tree.
-
Façade:
lib/phronesis/reflexion.ex -
Claim model:
lib/phronesis/reflexion/claim.ex,claim_extractor.ex -
Graph + paths:
lib/phronesis/reflexion/judgement_evidence_graph.ex,invariant_path.ex -
Comparison + gating:
lib/phronesis/reflexion/equivalence.ex,revaluation.ex,design_obligation.ex -
Append-only ledger:
lib/phronesis/reflexion/design_ledger.ex -
Tests:
test/reflexion_test.exs,test/reflexion/ -
Design doc:
docs/REFLEXION.adoc
| Technology | Also Used In |
|---|---|
Elixir / BEAM |
https://github.com/hyperpolymath/http-capability-gateway, https://github.com/hyperpolymath/burble |
TLA+ formal spec |
https://github.com/hyperpolymath/ephapax (Raft consensus for linear type proofs) |
LSP integration |
https://github.com/hyperpolymath/universal-language-server-plugin |
Incremental parsing |
https://github.com/hyperpolymath/tree-sitter-k9 (grammar-level incremental parse) |
Containerfile (Podman) |
https://github.com/hyperpolymath/session-sentinel, https://github.com/hyperpolymath/stapeln |
| Path | Proves |
|---|---|
|
Tokenises Phronesis source: 15 keywords, IPv4/6 literals, DateTimes, probabilistic type tokens |
|
Recursive-descent parser producing typed AST nodes |
|
Static type checker (probabilistic types, scope resolution) |
|
AST → |
|
Tree-walking interpreter for prototyping and REPL use |
|
Interpreter with execution trace hooks for debugger/profiler |
|
Incremental re-lexing for LSP edit support |
|
Incremental re-parsing bounded by expression boundaries |
|
Language Server Protocol implementation (hover, completion, diagnostics) |
|
Built-in policy predicates and ethical reasoning primitives |
|
Reusable distributable policy modules |
|
Package manager entry point |
|
Package resolution, fetching, caching |
|
Error reporting with source spans |
|
Interactive debugger and trace viewer |
|
Execution profiler |
|
Live policy reload without process restart |
|
Elixir Raft consensus scaffold |
|
Reflexion design layer: claims, judgement-evidence graph, equivalence gating, hash-chained design ledger |
|
TLA+ Raft consensus specification (model-checked) |
|
TLC model checker configuration |
|
Ethical scenario conformance test fixtures |
|
Lexer unit tests |
|
Parser unit tests |
|
(via phronesis_test.exs) Type checker coverage |
|
Compiler bytecode tests |
|
Interpreter execution tests |
|
Mandatory ethical scenario suite |
|
LSP integration tests |
|
End-to-end pipeline tests |
|
Supplementary source assets (non-Elixir) |
|
Language specification documents |
|
Syntax highlighting definitions |
|
Editor plugin scaffolds |
|
Podman container definition (Chainguard base) |
|
A2ML state, meta, ecosystem files |
|
Test results narrative |
|
LSP feature coverage summary |
|
Reflexion design-layer architecture and 8-class equivalence taxonomy |