agenticraft_foundation.specifications.consensus_spec

Formal consensus properties — Agreement, Validity, Integrity, and Termination.

Formal specifications for consensus protocols.

This module provides executable formal specifications for verifying consensus protocol correctness, based on distributed systems theory.

Key properties verified: - Safety: Agreement, Validity, Integrity - Liveness: Termination

References: - Fischer, Lynch, Paterson (1985) - Impossibility of consensus - Castro & Liskov (1999) - PBFT - Lamport (1998) - Paxos Made Simple

PropertyType

Bases: str, Enum

Types of formal properties.

PropertyStatus

Bases: str, Enum

Status of property verification.

PropertyResult dataclass

Result of property verification.

ATTRIBUTE	DESCRIPTION
property_name	Name of the property checked TYPE: str
property_type	Type of property (safety, liveness, etc.) TYPE: PropertyType
status	Verification status TYPE: PropertyStatus
message	Human-readable message TYPE: str
counterexample	Counterexample if violated TYPE: Any | None
trace	Execution trace leading to violation TYPE: list[str]
timestamp	When verification was performed TYPE: float

is_satisfied()

Check if property was satisfied.

ConsensusState dataclass

Bases: Generic[T]

State of a consensus instance.

ATTRIBUTE	DESCRIPTION
instance_id	Unique identifier for this consensus instance TYPE: str
participants	Set of participant IDs TYPE: set[str]
proposed_values	Values proposed by each participant TYPE: dict[str, T]
decisions	Final decisions by each participant TYPE: dict[str, T]
messages	Messages exchanged TYPE: list[dict[str, Any]]
round	Current round number TYPE: int
is_terminated	Whether consensus has terminated TYPE: bool
metadata	Additional state metadata TYPE: dict[str, Any]

FormalProperty

Bases: ABC, Generic[T]

Base class for formal properties.

Properties are executable specifications that can be checked against consensus states.

__init__(name, property_type)

Initialize property.

PARAMETER	DESCRIPTION
name	Property name TYPE: str
property_type	Type of property TYPE: PropertyType

check(state) abstractmethod

Check if property holds for given state.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[T]

RETURNS	DESCRIPTION
PropertyResult	PropertyResult with verification outcome

Agreement

Bases: FormalProperty[Any]

Agreement property: No two correct processes decide differently.

Formally: For all correct processes p and q, if p decides v and q decides v', then v = v'.

__init__(correct_processes=None)

Initialize Agreement property.

PARAMETER	DESCRIPTION
correct_processes	Set of correct (non-faulty) process IDs. If None, all participants are assumed correct. TYPE: set[str] | None DEFAULT: None

check(state)

Check Agreement property.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
PropertyResult	PropertyResult indicating if Agreement holds

Validity

Bases: FormalProperty[Any]

Validity property: Decided value was proposed by some process.

Formally: If a correct process decides v, then v was proposed by some process.

__init__(correct_processes=None)

Initialize Validity property.

PARAMETER	DESCRIPTION
correct_processes	Set of correct process IDs TYPE: set[str] | None DEFAULT: None

check(state)

Check Validity property.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
PropertyResult	PropertyResult indicating if Validity holds

Integrity

Bases: FormalProperty[Any]

Integrity property: A process decides at most once.

Formally: For all correct processes p, p decides at most once. This is implicitly tracked by the decision being final.

__init__(decision_history=None)

Initialize Integrity property.

PARAMETER	DESCRIPTION
decision_history	Historical decisions per process TYPE: dict[str, list[Any]] | None DEFAULT: None

check(state)

Check Integrity property.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
PropertyResult	PropertyResult indicating if Integrity holds

Termination

Bases: FormalProperty[Any]

Termination property: Every correct process eventually decides.

This is a liveness property that requires eventual progress. Formally: Every correct process eventually decides some value.

__init__(correct_processes=None, timeout_rounds=100)

Initialize Termination property.

PARAMETER	DESCRIPTION
correct_processes	Set of correct process IDs TYPE: set[str] | None DEFAULT: None
timeout_rounds	Maximum rounds before timeout TYPE: int DEFAULT: 100

check(state)

Check Termination property.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
PropertyResult	PropertyResult indicating if Termination holds/progresses

ConsensusSpecification

Complete specification for consensus protocols.

Combines all consensus properties and provides verification API.

__init__(correct_processes=None, custom_properties=None)

Initialize specification.

PARAMETER	DESCRIPTION
correct_processes	Set of correct process IDs TYPE: set[str] | None DEFAULT: None
custom_properties	Additional custom properties to check TYPE: list[FormalProperty[Any]] | None DEFAULT: None

verify(state)

Verify all properties against state.

PARAMETER	DESCRIPTION
state	Consensus state to verify TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
list[PropertyResult]	List of PropertyResults for all properties

verify_safety(state)

Verify only safety properties.

PARAMETER	DESCRIPTION
state	Consensus state to verify TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
list[PropertyResult]	List of PropertyResults for safety properties

verify_liveness(state)

Verify only liveness properties.

PARAMETER	DESCRIPTION
state	Consensus state to verify TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
list[PropertyResult]	List of PropertyResults for liveness properties

is_valid(state)

Check if state satisfies all safety properties.

PARAMETER	DESCRIPTION
state	Consensus state to check TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
bool	True if all safety properties satisfied

summary(state)

Generate verification summary.

PARAMETER	DESCRIPTION
state	Consensus state to summarize TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
str	Human-readable summary

InvariantChecker dataclass

Runtime invariant checker for consensus protocols.

Monitors state transitions and checks invariants are maintained.

add_invariant(invariant)

Add an invariant to check.

PARAMETER	DESCRIPTION
invariant	Invariant property to monitor TYPE: FormalProperty[Any]

check(state)

Check all invariants against current state.

PARAMETER	DESCRIPTION
state	Current consensus state TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
bool	True if all invariants hold

get_violations()

Get all recorded violations.

RETURNS	DESCRIPTION
list[PropertyResult]	List of violation results

clear()

Clear violation history.

create_byzantine_spec(n, f)

Create specification for Byzantine fault tolerant consensus.

Requires n >= 3f + 1 for safety.

PARAMETER	DESCRIPTION
n	Total number of processes TYPE: int
f	Maximum Byzantine failures TYPE: int

RETURNS	DESCRIPTION
ConsensusSpecification	ConsensusSpecification configured for BFT

create_crash_spec(n, f)

Create specification for crash fault tolerant consensus.

Requires n >= 2f + 1 for safety.

PARAMETER	DESCRIPTION
n	Total number of processes TYPE: int
f	Maximum crash failures TYPE: int

RETURNS	DESCRIPTION
ConsensusSpecification	ConsensusSpecification configured for CFT

hash_state(state)

Compute hash of consensus state for verification.

PARAMETER	DESCRIPTION
state	State to hash TYPE: ConsensusState[Any]

RETURNS	DESCRIPTION
str	SHA256 hash of state