Humanity+
Member of the futurist network formerly known as the World Transhumanist Association, founded by Nick Bostrom and David Pearce.
Engineer · philosopher · futurist
Dana Edwards
I use computation to help people make informed decisions and shape the systems they depend on. My work brings together intelligence augmentation, governance, and formal verification.
I build systems that let people and AI agents research, create, and participate in markets. Checkers enforce specified rules, and fees from actual use can fund tasks with clear payment terms.
Current research · September 2026
Neurosymbolic training for constitutional behavior.
At a fixed training budget, does symbolically checked, counterexample-directed training improve constitutional behavior compared with ordinary LLM-generated training data?
By constitutional behavior, I mean following explicit behavioral rules, such as respecting permissions, reporting uncertainty, and supporting claims with evidence, while still completing useful work.
How I develop the question
I use neurosymbolic workflows to connect creative search with explicit checks. LLMs help me arrive at new research questions, propose hypotheses, explore abstractions, and search for counterexamples. My custom Research Kernel Protocol MCP records the questions, evidence, dependencies, and failures so the investigation can be inspected and continued.
This connects my Formal Methods Philosophy work with A Market for Behaviors: make the incentive structure explicit, then test which behaviors it selects for.
Status: study in development. The current demonstrator uses finite-state models and tabular learning. The neural fine-tuning comparison remains to be run.
Background
How I got here.
I began with a question about involuntary ignorance: how can technology help people get the information they need to decide well? That led me to intelligence augmentation, network states, autonomous agents, and systems that check actions against explicit rules.
In 2015, I argued that cognitive bias, bounded rationality, and information asymmetry cause involuntary errors in human decision-making, and that intelligence augmentation could mediate them. In 2017, the Pangea whitepaper introduced Lucy, an autonomous agent designed to evolve into an exocortex. MPRD applies that thinking to AI actions: models propose actions, and deterministic checks enforce the rules. I use formal methods, experiments, and practical tests to assess whether the systems behave as intended.
The exocortex concept evolved from Ray Kurzweil's work on brain augmentation. I took that idea and built on it: a wisdom engine, a search engine but for decision support. The problem it was designed to solve was involuntary ignorance. For democracy to produce better governance, you need a wiser, more informed voter, a wiser lawmaker, and smarter institutions. Lucy was a prototype for what we now see with modern AI assistants, but its role was to empower each network citizen, not unlike what Sam Altman later described as "building a brain for the world" that is "extremely personalized and easy for everyone to use."
Sam Altman, "The Gentle Singularity", the parallel to Lucy, seven years later.
Influences
Two works shaped my thinking on technological unemployment and intelligence augmentation. I. J. Good's 1965 paper framed the stakes: if an ultraintelligent machine can design better machines, human intelligence is left behind. James Albus's Path to a Better World showed that automation need not produce mass poverty if the economic surplus is distributed intelligently. From Albus and Good, I developed two ideas over a decade ago: a Citizen's Income and a Citizen's Dividend, the latter modeled on the Alaska Permanent Fund. These were philosopher-level discussions in 2013; they are mainstream political discourse now. The thread from there to MPRD is the same: if automation changes who can act, governance must change how action is constrained.
"Let an ultraintelligent machine be defined as a machine that can far surpass all the intellectual activities of any man however clever. Since the design of such machines is one of these intellectual activities, an ultraintelligent machine could design even better machines; there would then unquestionably be an 'intelligence explosion,' and the intelligence of man would be left far behind. Thus the first ultraintelligent machine is the last invention that man need ever make."
I. J. Good, Speculations Concerning the First Ultraintelligent Machine (1965)
Bitnation
Helped design the network state with founder Susanne Tarkowski Tempelhof. The project was covered by The Atlantic, The Economist, and the Wall Street Journal, and awarded a UNESCO/Netexplo Grand Prix in 2017.
Cyborgization and human decision-making
Co-authored essay with Alexander J. Karran, published on Transpolitica. Argues that cognitive bias, bounded rationality, and information asymmetry cause involuntary errors in human decision-making, and that intelligence augmentation can mediate them. The motivation that runs through everything after. Read it.
Pangea Whitepaper: Lucy AI and the Exocortex
Co-authored the Pangea whitepaper with Susanne Tarkowski Tempelhof and others. Credited in footnotes for developing the reputation distribution mechanism and initial thinking on Nomic Law integration. Section 2.3 introduced Lucy, an autonomous agent designed to evolve into an exocortex, an external cognitive augmentation system. Seven years before the AI agent boom.
LUCY: Your AI Governance Operating System
The Lucy concept from the 2017 whitepaper, evolved into a full AI governance operating system. Co-authored book with Susanne Tarkowski Tempelhof. Available on Amazon.
MPRD, ZenoDEX, PopperPad, ZenoFCIS, Research Kernel MCP
Tools for checking AI actions, exchange settlement, scientific claims, and software behavior, with a shared research memory. Formal Methods Philosophy explains the methods through public tutorials and labs.
Selected work
Public systems you can inspect, run, and re-verify.
The project cards link to public repositories, proofs, specifications, replay commands, and tutorials. Formal Methods Philosophy is the companion publication, with the reasoning and methods presented for readers.
MPRD: Model Proposes, Rules Decide
An AI model proposes an action. The executor requires a verified receipt showing that the proposed action passed the specified policy checks.
- Typed execution interfaces and transcripts that carry proof evidence.
- Policy, state, action, and receipt commitments.
- Explicit distinction between implementation status, bounded claim, and production claim.
A way to check proposed AI actions against specified rules before execution. The executor requires a verified receipt; Lean proofs cover stated properties of the design.
ZenoDEX: Replayable Assurance Case
A formally constrained DEX/tokenomics stack organized around functional cores, replayable certificates, Lean proof artifacts, disaster-state witnesses, and public assurance replay.
- Claim registry vocabulary: release-backed, public replay, disputed, authorization-complete.
- Public replay commands with clearly stated coverage and limits.
- Lean theorems about canonical winners, settlement, and routing.
Integer-exact settlement, TLA⁺ models, and replayable certificates help check arithmetic and state transitions. The case study explains what those checks cover and what remains unverified. Cost scenarios are on the value page.
Append-only scientific memory
Claim
Evidence
Replay
Status
PopperPad: Scientific Memory
A ledger that works offline and records hypotheses, evidence, counterexamples, and reproducible checks. It keeps the history of attempts to refute each claim.
- Content-addressed objects and a hash-chained log preserve provenance.
- Supported, falsified, and disputed states are derived from replayable verifier evidence.
- Local trust, decentralized anchoring, and falsification markets can coexist without turning truth into a vote.
Verifiers decide scoped results. PopperPad preserves the evidence, provenance, and challenge history that make those results inspectable.
Pure core · atomic shell
Input
Pure core
Commit
ZenoFCIS: High-Assurance Functional Systems
A Rust library family for functional-core and imperative-shell systems. Immutable inputs enter a pure, total transition; the shell validates the exact candidate and publishes effects atomically.
- Canonical values, patches, plans, receipts, and commitments make boundaries explicit.
- Crash-atomic SQLite, idempotent replay, and cross-language evidence cover the effect boundary.
- A bounded ZenoDEX mount retains Python and Rust parity evidence.
The library provides concrete reference implementations and checked boundaries. It does not claim audit completion, production authorization, or unrestricted system coverage.
Formal Methods Philosophy
A tutorial and lab site on modeling, abstraction, symbolic tools, counterexamples, verification, and what it means to justify a claim about software.
Public tutorials and interactive labs teach the verification methods above. You can follow the explanation and try the checks yourself.
Research Kernel MCP: Research Memory
Research memory for AI assistants: questions, hypotheses, evidence, and failed approaches stay connected across sessions. The kernel records changes and enforces explicit evidence requirements before a claim can be marked supported.
- Typed atoms (claim, evidence, question, result, risk, counterexample) and typed edges (supports, refutes, contradicts, reformulates).
- Fail-closed promotion: a claim cannot become SUPPORTED without support evidence, a refutation attempt, dependencies, provenance, and a rationale.
- Content-addressed artifacts (SHA-256), persistent SQLite state, and an append-only event log for external ledger ingestion.
Models suggest ideas. The kernel checks whether the required evidence records are present; the attached proof or experiment supplies the support for the claim.
More public work
Other repos worth a look.
Explore more of my projects: automation that responds to events, research on witness spaces, Tau Language experiments, and tools for reviewing code.
Rust
Helix
A platform I can host myself to automate tasks in response to events. It coordinates agents through an architecture written in Rust.
Python · Apache-2.0 What-If Witness SpacesA preprint on what-if witness spaces and neurosymbolic disaster loops, with artifacts and instructions for reproducing the results.
Python TauLang ExperimentsEducational experiments with Tau Language: proven optimizations, math proofs, and code snippets produced with neurosymbolic assistance.
Python QualiaGuardianCode quality optimizer for metric-based agentic workflows. Measures and enforces quality gates in automated development pipelines.
Python · MIT Intelligent Daemon InterfaceDevelopment toolkit for creating, training, and deploying intelligent Tau Language agents with Q-learning and zero-knowledge proofs.
Python · MIT Alignment TheoremThe Tau Alignment Theorem: economic incentives align to produce ethical transactions when utility is community-defined.
Writing
Tutorials, interactive labs, and one question.
What does it mean to justify a claim about software? Each tutorial starts with a concrete picture, then tightens into a model tools can manipulate. The labs turn abstract claims into something visible.
- 01Approximate state tracking
State machines, abstraction, counterexamples, CEGIS, and the boundary between heuristics and proofs.
- 02MPRD and the Algorithmic CEO
The neurosymbolic gate turned into production architecture. Models propose, rules decide.
- 03Resolution, refutation, and falsification
Proof in a closed formal world vs corroboration in an open empirical one.
- 04Consciousness, computationalism, and Rice's theorem
If consciousness is a nontrivial semantic property, no general detector can decide it.
- 05A Market for Behaviors: What Learning Is
Learning is adjusting behavior probabilities based on reward signals. Those signals are set by a market. Five layers from behavioral spectrum to alignment as market design, with an interactive lab.
- TrackZenoFCIS learning path
A guided path from immutable values and pure transitions to deterministic composition, atomic effects, and idempotent replay.
Contact
I'm Dana. I work with people who want to build a better future with technology.
I bring together ideas from governance, philosophy, computation, and education to explore what people and machines can do together. If you have a question to explore, an idea to develop, or something useful to build, write to me.
This site brings together my projects, writing, and capabilities as I develop them. Follow the links to see what I have made and how it was checked.