2026-08-28·by Sijie Wang#cybernetics#principles

lcf-for-labor

The true category of vibe-linter. Its nodes are not behavior-specified processes (a workflow says "what happens"); they are internally stochastic — the graph only describes what counts as done + the dependency order of completion-proofs. Steps are existentially quantified: "∃ an execution that makes the validator pass." So the net is a structure of proof obligations.

The 50-year-old precedent is the LCF architecture (HOL, Isabelle): proof search is untrusted (any tactic, even neural), but thm is an abstract data type whose only constructors are the trusted kernel's inference rules. Mapping:

agent = tactic · validator = kernel inference rule · token = thm

Node semantics = a Hoare triple {hold these tokens} stochastic-blackbox {validator passes}, with fuel/timeout/escalation as the ontological semantics of failure (completion is only a hope). "The closest relative isn't Airflow, it's Isabelle — a logician went in a big circle and came back to building a proof assistant, except this time the tactic spends money."

This is also why it's a recognizer, not a generator → recognizer-not-generator.

Up: vibe-linter

about this entry

One of sijie's wiki entries. The AI on this site is grounded in the same corpus and answers in sijie's voice, with citations back to entries like this one — answering costs sijie money, so it waits behind a code: enter an access code →