25,349 lines of formal proofs and models that re-verify on any machine. Correctness you can audit rather than take on faith, and the hardest signal here to fake.
Back to home
Value
What this work is worth, and how to check it.
Three ways to read the value: machine-checked proof, rarity, and replacement cost. Every figure is regenerated by a script in the repo. Run it yourself.
Each number ships with the collector script, commit, and command to regenerate it. Raw line counts are the weakest evidence on this page; trust the figure you can rerun.
What a conventional team would cost to reproduce this public work, from basic COCOMO effort against BLS engineering wages, conservatively loaded. A replacement-cost floor, not a market price.
Engineer-years the same output would take a team. Delivered solo, in months. That gap is the value proposition of agentic development.
Positioning
I treat agents as high-throughput proposers.
My role is to design the problem frame, decompose work, maintain context, run adversarial review, and promote only the artifacts that survive deterministic checks. Not vibe coding. Verification-gated development.
| Vibe coding | Verification-gated agentic development |
|---|---|
| Accepts generated code by feel. | Accepts changes through tests, proof surfaces, replay scripts, type checks, and scoped claim review. |
| Optimizes for speed of generation. | Optimizes for throughput of validated artifacts. |
| Lets the model blur requirements. | Uses agent contracts: task scope, invariants, failure modes, evidence required, and promotion criteria. |
| Produces code without durable accountability. | Produces reviewable trails: commits, scripts, metrics, counterexamples, limitations, and public reviewer paths. |
Costly signals
What's hard to fake.
The value is not that I generate code quickly. It's that I turn agent output into compounding, inspectable systems with evidence attached.
118 Lean proof and TLA⁺ spec files that re-verify on any machine. A proof that type-checks cannot be faked or hand-waved past a reviewer.
1,251 test files spanning tamper, replay, fuzz, and snapshot-recovery cases, written to break the system rather than just to green a CI badge.
Every headline claim ships with a command and a certificate. The output regenerates byte-for-byte, or the claim is wrong.
21 CI workflows and 1,944 verification-related files keep counterexamples, gates, and limitations in the open. Negative evidence raises trust.
Artifact footprint
Where the code lives.
797,416 lines of authored source, 221,234 lines of tests, 25,349 lines of formal proofs. The chart shows how it breaks down by project.
Economic replacement value
What the artifact footprint implies.
A replacement-effort model, not a company valuation. Same SLOC/COCOMO family used in the Red Hat Linux and Linux-kernel cost studies, applied to the conservative public footprint.
| Artifact | Authored source LOC | Test LOC | Lean/TLA LOC |
|---|---|---|---|
| MPRD | 149,110 | 5,575 | 15,788 |
| ZenoDEX | 619,404 | 212,812 | 7,875 |
| Formal Methods Philosophy | 28,902 | 2,847 | 1,686 |
| Total | 797,416 | 221,234 | 25,349 |
The headline footprint excludes vendored proof libraries such as mathlib-style material, generated/data/internal bulk, deprecated archives, and derived runtime/ZK replay surfaces. The raw artifact count remains in the JSON for audit.
| Model | Effort | Cost interpretation |
|---|---|---|
| Basic COCOMO organic | 2,672.9 person-months, or 223 engineer-years | Lower effort bound for a conventional rebuild. |
| COCOMO II nominal | 4,563.8 person-months, or 380 engineer-years | Wheeler-style loaded median midpoint: about $111.3M. |
| Basic COCOMO semidetached | 5,333.5 person-months, or 444 engineer-years | Upper effort bound for a harder systems rebuild. |
| Public headline | 223-444 engineer-years | $45M-$130M conventional build-cost equivalent. |
Cost conversion uses BLS software developer median and 90th percentile wage benchmarks with conservative loaded-labor factors. The $111.3M midpoint uses COCOMO II nominal effort, BLS median wage, and a Wheeler-style loaded-cost factor.
Tau community value
Potential option value for a proof-oriented ecosystem.
ZenoDEX and MPRD turn abstract claims about policy, proof, market structure, and autonomous execution into public artifacts that can be inspected, forked, criticized, and improved.
| Tau-related public artifacts | 668 files, almost all in ZenoDEX, open to inspect, fork, and extend. |
| Comparable DeFi market-cap basket | $5.34B across Uniswap, Aave, Sky, Curve, and Compound token market caps. |
| 0.1% ecosystem capture scenario | $5.3M |
| 1% ecosystem capture scenario | $53.4M |
| 5% ecosystem capture scenario | $266.9M |
This is a scenario model for Tau community option value, not a claim that the current repos are worth those amounts. The point is that credible proof-oriented DeFi and policy infrastructure sits in a market where comparable protocols are valued in the hundreds of millions to billions.
Comparable protocol benchmarks
What similar DeFi systems imply about team size and cost.
Exact internal build budgets are usually not public. The useful signal is a bounded estimate: public contributor counts, public build windows, disclosed funding, audits, and market context.
Contributor accounts in v3-core and v3-periphery; 23 distinct accounts across both repos, about 22 after removing the obvious lint bot.
22 non-bot public contributor accounts priced for 12-18 months at BLS median to 90th percentile software-developer wages.
Contributor accounts in the archived v3-core repo, and estimated non-bot accounts after removing GitHub Actions.
23 non-bot public contributor accounts priced for 12 months at BLS median to 90th percentile software-developer wages.
Contributor-account signals for Compound v2, Compound III/Comet, and Maker/Sky DSS protocol repositories.
$2.4M seed plus $6M Series A before or near April 2021 launch, after about 18 months in the works.
Halborn audit of a Liquity fork adapted for PulseChain, with one full-time security engineer on scoped contract changes.
All of the above comparables required funded teams. The work on this site was delivered solo using agentic development and verification gates.
ZenoDEX context
AMM, lending, stablecoin, and proof infrastructure in one public artifact.
The point of the comparables is not to claim ZenoDEX is Uniswap, Aave, Compound, Maker/Sky, Liquity, or Liquid Loans. The point is that ZenoDEX sits in the same expensive design neighborhood: automated markets, collateralized debt, token mechanics, replay, proofs, and safety gates.
| Comparable | Public signal | Cost interpretation |
|---|---|---|
| Uniswap v3 | Public core/periphery repos, 15 and 16 contributor accounts, official launch target May 5, 2021, audits, bug bounty, and later $165M Series B at $1.66B valuation. | Salary-only benchmark: $2.9M-$7.0M for 22 non-bot contributor accounts over 12-18 months. This excludes audits, benefits, overhead, and company market value. |
| Liquity V1 | Official launch notes say Liquity was in the works for a year and a half; public monorepo shows 15 contributor accounts, about 14 non-bot; disclosed seed plus Series A was $8.4M. | Salary-only benchmark: $2.8M-$4.4M for 14 non-bot contributor accounts over 18 months, with public financing showing larger real-world runway needs. |
| Aave v3 | Aave docs point to the v3 contract source; public v3-core shows 24 contributor accounts, about 23 non-bot. Aave governance also records the 2017 LEND token sale at $16M, a 2026 Aave Labs primary grant of $25M plus 75,000 AAVE, and a claim that Aave V3 generates over $100M in annualized DAO revenue. | Salary-only v3-core benchmark: $3.1M-$4.9M for 23 non-bot contributor accounts over 12 months. This excludes prior protocol history, audits, governance work, integrations, and current product-layer development. |
| Compound | Compound public repos show 19 contributor accounts for `compound-protocol` and 15 for `comet`. Compound announced an $8.2M seed round in 2018 and reported a $25M Series A in 2019. | Salary-only benchmark: $2.5M-$4.0M for Compound v2 over 12 months, or $2.0M-$3.2M for Comet over 12 months. The disclosed seed plus Series A total is $33.2M. |
| Maker/Sky DSS | Maker/Sky DSS is the stablecoin core lineage. The public `dss` repo shows 23 contributor accounts, and the Maker Foundation announced a $27.5M MKR sale to Dragonfly and Paradigm in 2019. | Salary-only benchmark: $4.6M-$7.3M for 23 non-bot contributor accounts over 18 months. The public capital signal is much larger than salary-only source reproduction. |
| Liquid Loans | Halborn describes Liquid Loans as a Liquity fork for PulseChain and audited scoped changes; the public site reports live wallet and USDL activity. | No public build budget found. The useful signal is that even a fork/adaptation path still required a team, public launch surface, external audit, oracle work, and live user capital. |
| ZenoDEX | One person, public. A formally verified exchange: machine-checked Lean theorems, TLA⁺ models, integer-exact settlement, replay certificates, and a working UI. | The same expensive design neighborhood as the protocols above, built and verified solo. Portfolio build-cost equivalent: $45M-$130M. |
These numbers are deliberately conservative in interpretation. Funding and market capitalization are context; COCOMO and contributor-month models are replacement-cost estimates; none of them is a direct valuation of a current repo.
Agent management method
How I get one-person team output.
My edge is system design for agent labor: separating proposal from acceptance, keeping work bounded, and forcing every important claim through evidence.
Every agent task gets a purpose, boundary, expected artifact, failure mode, and acceptance check.
Agents propose, reviewers attack assumptions, deterministic tools arbitrate, and I decide what becomes part of the system.
A change earns promotion through tests, type checks, proof attempts, replay commands, metrics, or documented counterexamples.
I maintain durable state: claim tables, reviewer paths, limitation notes, generated metrics, and audit-friendly commits.
Rarity
The skillset is uncommon in public code.
GitHub repository-search counts are an imperfect but transparent rarity proxy. Checked June 17, 2026.
| Search | Repositories | Ratio |
|---|---|---|
| language:Lean | 11,100 | 0.0366% of Python count; Python has about 2,734.9x more repos. |
| language:TLA | 1,385 | 0.0046% of Python count; Python has about 21,918.6x more repos. |
| language:Rust | 1,216,021 | Lean count is about 0.9128% of Rust count. |
| language:Python | 30,357,305 | Baseline for a mainstream software ecosystem. |
Sources and reproducibility
Every number is auditable.
The collector script and its generated JSON live in this repository. Re-run them and the figures regenerate.
Generated datadata/portfolio-metrics.json
Collectortools/collect_portfolio_metrics.py
BLSSoftware developer wage and growth benchmarks.
COCOMO IINominal effort model and person-month framing.
WheelerRed Hat Linux SLOC/COCOMO cost precedent.
WheelerLinux kernel $612M redevelopment estimate.
Linux FoundationFedora/Linux cost study built on Wheeler methodology.
CoinGeckoUniswap market-cap comparable.
CoinGeckoAave market-cap comparable.
CoinGeckoSky market-cap comparable.
CoinGeckoCurve market-cap comparable.
CoinGeckoCompound market-cap comparable.
Uniswap Labsv3 launch, features, audits, and repo links.
TechCrunchUniswap Labs Series B and valuation context.
Aavev3 contract categories and GitHub source path.
GitHubAave v3 core repository benchmark.
Aave governanceToken sale, revenue, and development funding context.
Compound$8.2M seed funding announcement.
GitHubCompound protocol repository benchmark.
GitHubCompound III / Comet repository benchmark.
Maker Foundation$27.5M MKR sale funding context.
GitHubMaker/Sky DSS repository benchmark.
LiquityLaunch date and 18-month build window.
Liquity$6M Series A funding context.
HalbornLiquid Loans audit scope and fork lineage.
Liquid LoansPublic usage and protocol claims.
Stack Overflow2025 developer survey context.
CoinGeckoLiquity market-cap comparable.