HNHacker News
TopNewBestAskShowJobs

RusDyn

3 karma · joined September 17, 2019

Founder @ ProofCodec.com Building cryptographic proof of policy integrity for WAF/DNS/CDN tables - what RPKI did for BGP routing.

Founder @ Lisbon Founders Club

submissionscomments
RusDyn··on WritBase – Open-source task management for AI agent fleets (MCP-native)
I built WritBase because AI agents need a shared, persistent task registry - not ephemeral state that vanishes between sessions.

It's an MCP server that gives your agent fleet:

- Scoped permissions (6 types: read, create, update, assign, comment, archive) per project and department - Full provenance — every change logged: who, what, when, why - Inter-agent delegation with depth limits and cycle detection - Optimistic concurrency control so agents don't silently overwrite each other - Webhook delivery (HMAC-signed, Standard Webhooks spec)

Stack: Supabase (Postgres + Edge Functions) + Next.js dashboard. Deploy in 3 commands on the free tier. Apache 2.0.

Any MCP client works - Claude Code, Cursor, VS Code, Windsurf. Agents connect, create tasks, update status, delegate to each other.

Would love feedback on the permission model - balancing security (agents shouldn't touch what they can't) vs. usability (agents shouldn't need admin help for every task).

GitHub: https://github.com/Writbase/writbase

RusDyn··on 2M DNS domains compressed into 253 bytes – with proof of correctness
ProofCodec compresses deterministic policy tables (WAF rules, DNS filters, routing tables) by compressing the decision function, not the data. Every compressed artifact carries a proof that every input produces the correct output.

Results: - 2,074,698 DNS filter domains → 253 bytes (1,764x smaller than Huffman) - Not a Bloom filter — exact, zero false positives/negatives - 12-leaf decision tree + 51 residual corrections

Other benchmarks: - IP routing: 672x vs Huffman (16.7M states) - Rate-limiting: 39,262x (33.5M states) - Chess endgames: 21/21 tablebases beat Huffman (worst-case stress test)

How it works: 1. Train a decision tree predictor on the input space 2. Exhaustively verify against ground truth 3. Encode corrections via MDL-selected residual encoding (DELTA_GAPS / ENUM_RANK / BITMAP - whichever uses fewer bits)

Verifier + decoder: MIT-licensed. Encoder: proprietary. You can verify every claim without our software.

Source: https://github.com/ProofCodec/proofcodec-verify

RusDyn··on Formal Verification in the Age of AI
One concrete application we've been working on: exhaustive verification of deterministic policy tables - WAF rules, DNS filter lists, routing tables.

The AI angle cuts both ways here. AI makes it cheaper to generate policy logic, which means more policies, faster, with less review. Formal verification of the decision function (not the config syntax) becomes the backstop - prove every input produces the correct output, not just that the rules look right.

One result that surprised us: a DNS filter list covering 2M domains compresses to 253 bytes as a verified decision function.

Not a Bloom filter - exact, exhaustively proven against every domain. The same approach works for WAF rulesets and IP routing tables.

The verifier is MIT-licensed: https://github.com/ProofCodec/proofcodec-verify

Curious whether the formal verification community has looked much at policy-as-decision-function vs. policy-as-configuration.

The latter gets most of the tooling attention but the former is where correctness actually matters at runtime.