Skip to content

Comments

Add CLI, safety proofs, and TLA+ consensus model#2

Merged
hyperpolymath merged 1 commit intomainfrom
claude/phronesis-network-grammar-BQTIM
Dec 16, 2025
Merged

Add CLI, safety proofs, and TLA+ consensus model#2
hyperpolymath merged 1 commit intomainfrom
claude/phronesis-network-grammar-BQTIM

Conversation

@hyperpolymath
Copy link
Owner

CLI/REPL (lib/phronesis/cli.ex):

  • phronesis run <file> - Execute policy files
  • phronesis parse <file> - Show AST
  • phronesis check <file> - Validate syntax
  • phronesis repl - Interactive REPL with state management
  • Build with mix escript.build

Safety Proofs (docs/safety_proofs.md):

  • Sandbox Isolation: Policies cannot escape execution environment
  • Capability Enforcement: Operations require explicit grants
  • Byzantine Fault Tolerance: Safety with N >= 3f + 1 agents
  • Combined security analysis and attack surface review

TLA+ Consensus Model (formal/PhronesisConsensus.tla):

  • Formal specification of PBFT-style consensus protocol
  • Safety properties: Agreement, Validity, Non-repudiation
  • Liveness properties: EventualDecision, Progress
  • Configuration for TLC model checker included

Also updates mix.exs with escript configuration.

CLI/REPL (lib/phronesis/cli.ex):
- `phronesis run <file>` - Execute policy files
- `phronesis parse <file>` - Show AST
- `phronesis check <file>` - Validate syntax
- `phronesis repl` - Interactive REPL with state management
- Build with `mix escript.build`

Safety Proofs (docs/safety_proofs.md):
- Sandbox Isolation: Policies cannot escape execution environment
- Capability Enforcement: Operations require explicit grants
- Byzantine Fault Tolerance: Safety with N >= 3f + 1 agents
- Combined security analysis and attack surface review

TLA+ Consensus Model (formal/PhronesisConsensus.tla):
- Formal specification of PBFT-style consensus protocol
- Safety properties: Agreement, Validity, Non-repudiation
- Liveness properties: EventualDecision, Progress
- Configuration for TLC model checker included

Also updates mix.exs with escript configuration.
@hyperpolymath hyperpolymath merged commit d081c42 into main Dec 16, 2025
1 check failed
@hyperpolymath hyperpolymath deleted the claude/phronesis-network-grammar-BQTIM branch December 16, 2025 03:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants