A small C coordination runtime (~7100 lines) implementing decaying shared fields, k=7 topological neighbor election, heartbeat-based failure detection, and threshold consensus. The code avoids dynamic allocation and recursion, keeps loops bounded, and uses static configuration. Includes an Isabelle/AutoCorres verification session: the ballot evaluation core is machine-checked against a pure HOL spec (phase B2), the heartbeat init and health-transition lemmas are discharged (B1/B3), and a TLA+ model checks the consensus protocol's safety invariants above it (bounded model checking — see docs/tla/).
- POSIX build and test path is working today
- the runtime shape is compact enough to inspect quickly
- the ballot evaluation core (
ekk_consensus_eval_ballot) is machine-checked against a pure HOL spec (phase B2); the heartbeat lemmas are discharged too — B1 (init returnsEKK_OKtotally, zeroing loop terminates) and B3 (the C health-transition validator refines the abstract state machine) — with nosorry, noquick_and_dirty(see docs/VERIFICATION_PLAN.md) - a TLA+ model of the consensus protocol (docs/tla/) surfaced the inhibition/approval race now fixed in
on_vote; its safety invariants hold under bounded model checking (3 nodes, symmetry + state constraints, ~2 min; removing the fix makes the model fail in ~4s — the bound has teeth) - hardening and proof-readiness gaps are tracked explicitly rather than hidden
cmake -S . -B build
cmake --build build
ctest --test-dir build --output-on-failureThis is the shortest check that the repo builds and passes its tests.
- Field engine (
ekk_field) -- Decaying shared coordination fields with seqlock-protected publish/sample and gradient computation. - Topology (
ekk_topology) -- Event-driven k-nearest neighbor election under configurable distance metrics. - Heartbeat (
ekk_heartbeat) -- Liveness tracking with UNKNOWN/ALIVE/SUSPECT/DEAD state machine and inter-arrival timing. - Consensus (
ekk_consensus) -- Per-ballot threshold voting with early rejection, mutual inhibition, and Byzantine evidence framework. - Module (
ekk_module) -- Module-local coordination loop composing all subsystems into a single tick with three-way outcome contract.
docs/README.md- documentation entrypointdocs/KEY_COMPONENTS.md- subsystem mapdocs/SYSTEMS_REVIEW.md- current correctness and hardening gapsdocs/VERIFICATION_PLAN.md- proof-track scope and milestones
The docs/isabelle/ directory contains an Isabelle/AutoCorres session covering
the consensus voting logic and heartbeat state machine. Phase B2 is discharged:
ekk_consensus_eval_ballot_correct proves that the AutoCorres-lifted production
function ekk_consensus_eval_ballot (the same translation unit the runtime
compiles) returns exactly the pure HOL spec eval_ballot_spec — totally, with
every generated guard discharged — under the preconditions
yes_votes <= eligible_voters, total_votes <= eligible_voters,
eligible_voters <= 64, 0 <= threshold <= 65536. The heartbeat lemmas are
also discharged: B1 (ekk_heartbeat_init_verif_ok) proves the init path returns
EKK_OK totally, including termination of the 64-slot zeroing loop; B3 proves
the C validator health_transition_valid computes exactly the abstract
valid_health_edge relation, and that set_neighbor_health_verif writes only
the addressed neighbor's health field. The session builds without
quick_and_dirty; scripts/check-no-sorry.sh gates against regressions.
To build it, you need:
Then run:
<isabelle>/bin/isabelle build \
-d <l4v> \
-d docs/isabelle \
EkkVerificationReplace <isabelle> and <l4v> with paths to your local installations.
See docs/SYSTEMS_REVIEW.md for a detailed systems review covering correctness defects, undefined-behaviour paths, and verification-readiness gaps.
See DEVELOPMENT.md for the canonical smoke path and review posture.
- Code (
.c,.h,.thy,ROOT, build scripts): MIT - Documentation (
.md): CC-BY-SA-4.0
Copyright (c) 2026 mamut-studio.com