Tutorials, interactive labs, and one question: what does it mean to justify a claim about software?

State machines, abstraction, counterexamples, CEGIS, and the boundaries between heuristics and proofs. Start inside a card counter's head, then zoom out.

Why some "different abstractions" are the same thing in different clothes, and how to move problems into better toolchains.

Read and write small executable specifications by listing invariants first, then letting a solver produce behaviors that satisfy them.

Why internal models are more than prediction, why test-time learning is powerful, and why invariants matter when the model can drift.

Start from arcade, ATM, and vending-machine intuition, then compress those shared shapes into states and invariants.

Build Presburger arithmetic from zero and successor, and see why excluding multiplication makes every question decidable.

Compare proof by exhaustive search with sum-over-histories, then extend to action, weighted futures, and intelligent planning.

Use seL4 as a case study for shrinking the trusted core, proving small local contracts, and widening assurance through checked composition.

Put logical refutation and Popperian falsification side by side. Separate proof in a closed formal world from corroboration in an open empirical one.

If consciousness is a nontrivial semantic property of computation, then no general Turing-machine detector can decide it from arbitrary encodings.

Recover missing requirements from witness structure, observation quotients, and minimal separator policies.

Learn branch exploration as witness search: concrete execution gives one real path, symbolic path constraints steer the next run.

Structured witness search over grammars. See why syntax preservation reallocates budget into semantic execution.

Define Church synthesis precisely, trace what is decidable, then use decomposition-plus-invariants against the complexity wall.

What separates a proof that checks from a proof that communicates, and how to curate a proof library for reviewer trust.

The difference between a collection of checking proofs and a library that an expert reviewer can navigate, trust, and extend.

Why the clopen algebra of Cantor space is the unique countable atomless Boolean algebra, and what its completion adds.

The Boolean-algebra machinery behind TABA, read step by step: quantifier-elimination and guarded-successor formulas.

Pointwise revision, fixed-point semantics, runnable demos, and the boundary between this prototype and full TABA tables.

Why Tau qelim optimization is a fragment-dispatch problem, and how guarded BDD and CNF-native routes speed up scoped formulas.

How bounded LTL-style operators fit Tau, why finite-horizon temporal formulas are decidable, and the new optimizer layer this creates.

Certificate-carrying optimizers: search for aggressive rewrites while accepting only candidates whose certificates pass a trusted checker.

Detect blowup risk before solving, compress unused variables, and use route prediction without replacing proof certificates.

Ohad Asor's upstream Tau LTL(ABA) design, compared to the bounded Temporal Tau fragment.

Turn one readable governance sentence into a checked two-variable counting formula, then prove the translation is sound.

Model two-player bounded games as Tau tables, inspect winning regions, and see the boundary between bounded games and unbounded ones.

Bridge neural proposal distributions and Boolean-algebraic constraints inside Tau, and inspect where the bridge holds and where it breaks.

Use EML trees to generate, rank, and test symbolic hypotheses with bounded guarantees, then separate the hypothesis lane from the proof lane.

Generate symbolic hypotheses from EML trees and quotient networks, then verify them against bounded Tau specs.

Sparse impact factor solving: identify which variables actually matter for a given query, and skip the rest.

Energy-based route telemetry: measure which optimizer routes work, and feed the measurements back into route selection.

A tiny energy scorer ranks bounded candidate sets for Tau and ZenoDEX. Verifier authority stays separate.

How Tau-checked formulas become measured route labels, how a small energy ranker improves checker order, and how the demo stays replayable.

Split a Tau-facing assistant into LLM interface, TauEnergy ranking, TauJEPA failure pressure, and Tau verification.

A user-centered framework for the agentic era: provenance-agnostic quality, diamond-rule engineering, and best-practice rails for safe systems.

How entropy reduction connects living systems, computational systems, and the boundary where consciousness might enter.

Frame software hardening as a thermodynamic-style process: each gate, test, and proof reduces the reachable state space of failure.

What survives into a trained model, what does not, and how safety gates at training time differ from gates at inference time.

Learning, whether in animals, humans, or AI, is the process of adjusting behavior probabilities based on reward signals. Those reward signals are set by a market for behaviors. Five layers: behavioral spectrum, incentive map, market, training as compression, alignment as market design. With an interactive lab.