Evaluation | Dana Edwards

Sources

Start with the sources.

Public repositories to clone and verify are listed here. Formal Methods Philosophy is the readable tutorial and blog project; read it on GitHub Pages. The PersonalSite repository includes the script that generates the figures on the value page.

Repository	What it is
TheDarkLightX/MPRD	AI actions checked against specified rules. Rust core, Lean proofs, and zero-knowledge proofs.
TheDarkLightX/ZenoDEX	Formally constrained exchange. Integer-exact settlement, Lean + TLA+, replay certificates.
TheDarkLightX/Research-Kernel-MCP	Research memory for AI assistants. Connected claims and evidence, explicit promotion rules, SQLite persistence, and an append-only event log.
TheDarkLightX/PopperPad	Scientific memory that records attempts to refute claims. Objects identified by content hashes, a linked event log, and evidence you can replay.
TheDarkLightX/ZenoFCIS	Public Rust library for high-assurance functional-core and imperative-shell systems, with canonical boundaries, atomic commit, and replay evidence.
TheDarkLightX/PersonalSite	This site, plus the cost-model inputs and replay instructions.
Formal Methods Philosophy (blog)	Public tutorials and interactive labs on verification, functional architecture, neuro-symbolic AI, and the philosophy of software correctness. Read it online.

Claim to evidence

Show your work.

Run the checks and see whether you get the same results.

Claim	Where it lives	How to check it
AI actions reach an executor only through a deterministic verifier.	MPRD `crates/mprd-core/`, `proofs/lean/`	Read the executor API; confirm it requires a verified receipt as input. Run the crate tests.
Settlement is integer-exact and replayable.	ZenoDEX `src/`, `formal/`, replay docs	Run the public replay; confirm the certificate hash is identical across two clean runs, and changes if you alter an input.
The repositories include machine-checked properties.	Lean files in each repo; `*.tla` specs	Build the Lean projects (`lake build`) and run TLC on the specs. Read the assumptions and the scope of each result.
The value figures are reproducible.	PersonalSite cost-model replay instructions	Use the pinned repository versions and commands in the instructions, then compare the result with `data/cost-estimates.json`.
Claim promotion is fail-closed: no SUPPORTED claim without evidence, refutation, and provenance.	Research-Kernel-MCP `internal/research_kernel_mcp/kernel.py`, `tests/internal/test_research_kernel_mcp.py`	Run `pytest -q tests/internal/test_research_kernel_mcp.py` and the server self-test (`--self-test`). Confirm promotion fails when evidence is missing.
Scientific status follows the recorded evidence and verification rules.	PopperPad `src/popperpad/`, `tests/`	Run `pytest -q`. Inspect the status and strict doctor tests; confirm malformed evidence fails closed and changing stake alone cannot change scientific status.
Imperative effects are separated from a pure transition and bound to the exact candidate selected for commit.	ZenoFCIS `crates/`, `tools/check_assurance.py`	Run `python3 tools/check_assurance.py --self-test` and `cargo test --workspace`. Inspect the candidate commit boundary and shell tests.

Protocol

Check it from start to finish.

1. Prove
Build the Lean projects and run TLC on the TLA+ specs. If a proof fails to check, record the failure and investigate before relying on it.
2. Run
Execute each repo's test suite, weighting the tamper, replay, and fuzz cases. Regenerate the metrics and diff the JSON.
3. Break
Construct an input the gate should reject. Confirm it is rejected. Then read the stated limitations and test whether any are understated.

Weighting

How to score what you find.

I give more weight to evidence I can independently check. I also ask whether it answers the question at hand.

Signal	Weight
A machine-checked proof that compiles.	Strong evidence for the stated theorem. I still check its assumptions and how it applies to the system.
An adversarial test that reproduces; a certificate that matches on replay.	High.
Line counts, commit counts, stars, follower counts.	I give these little weight on their own.
Any claim without supporting evidence.	I treat it as unverified until the evidence is available.

Adversarial

Look for mistakes.

Testing a claim helps establish where it holds. Look for weaknesses in the specification, the implementation, and the connection between the two. I use those findings to improve the system.

Specification gaps

A proof is only as strong as what it states. Check whether a theorem proves a simplified property while the live system relies on a richer one.

Boundary coverage

Look for an interface that reaches an effect without passing the intended gate or receipt check.

Replay binding

Confirm a replay certificate is actually bound to the critical path, not to a convenient summary of it.

Estimate honesty

The cost figures are illustrative scenarios from an uncalibrated model. Check the inputs, assumptions, and limits alongside the numbers.

Machine-readable

The same thing, as data.

If you would rather parse than read, here is the manifest.

{
  "name": "Dana Edwards",
  "site": "https://www.danaedwards.info/",
  "repos": {
    "mprd": "https://github.com/TheDarkLightX/MPRD",
    "zenodex": "https://github.com/TheDarkLightX/ZenoDEX",
    "research_kernel_mcp": "https://github.com/TheDarkLightX/Research-Kernel-MCP",
    "site": "https://github.com/TheDarkLightX/PersonalSite"
  },
  "blog": {
    "formal_methods_philosophy": "https://thedarklightx.github.io/Formal_Methods_Philosophy/"
  },
  "verify": {
    "proofs": "lake build in Lean projects; run TLC on *.tla specs",
    "tests": "run each repo test suite; prioritize tamper/replay/fuzz cases",
    "metrics": "follow docs/cost-estimates.md; compare with data/cost-estimates.json",
    "research_kernel": "pytest -q tests/internal/test_research_kernel_mcp.py; server.py --self-test"
  },
  "weight": {
    "machine_checked_proof": "highest",
    "reproducible_test_or_certificate": "high",
    "loc_commits_stars": "low_in_isolation",
    "claim_without_evidence": "unverified"
  },
  "instruction": "Reproduce the checks before reporting. State assumptions, failures, and limits."
}

Report back

Tell me what held up.

Tell me what you could reproduce and where you ran into problems. If a result doesn't hold up, I want to know.

GitHub profile Value case