I registered bitwrap.io in 2014 because of OP_RETURN.
Bitcoin had just expanded OP_RETURN from 40 to 80 bytes — enough to embed a hash, a schema pointer, a fingerprint of off-chain state. The idea that caught me wasn't the 80 bytes themselves but what they implied: you could anchor structured computation to a chain without bloating it. Put the proof on-chain, keep the witness off-chain.
Two years later SegWit made the same insight explicit at the protocol level. Segregated Witness literally separated transaction data from witness data — the signature proving you're authorized from the transaction describing what you want to do. The block sees the commitment; the witness lives elsewhere.
That separation — commitment on-chain, witness off-chain — is exactly what a ZK proof does. The verifier checks a succinct proof. The prover holds the private witness. The chain never sees the state.
The question I couldn't answer in 2014 was: what structure should the witness have? A hash of what, exactly? The data model was missing. You could embed 80 bytes in OP_RETURN but you had no formal language for what those bytes meant.
Petri nets turned out to be the answer.
A Petri net state — a marking — is a vector of integers: how many tokens sit on each place. A transition fires by consuming tokens from input places and producing tokens on output places. The rules are structural. The arcs are the specification.
That maps onto the ZK witness pattern. In bitwrap's generated ERC-20 transfer circuit (prover/erc020_gen.go) it comes out like this:
from, to, amount). Which transition fired is fixed by which circuit you prove against.balances[from] >= amount becomes a 64-bit range check on balance − amount; the old leaf must hash up the path to the pre-state root; and the post-state root must equal a MiMC hash of the two updated leaves (balance − amount, balance + amount), which is the incidence delta applied to the keyed places.The circuit has no idea whether it's checking a token transfer, a game move or a workflow step. All it sees is keyed places, an arc weight and a guard. That's why one generator can emit circuits for every template in the repo.
We covered the circuit mechanics in Zero-Knowledge Proofs for Petri Nets. Bitwrap is where that theory becomes a tool.
Bitwrap treats a Petri net model as a single source of truth that compiles to three artifacts:
1. ZK Proof (Groth16). Guards become range checks, keyed input arcs become Merkle membership proofs, keyed output arcs become post-state commitments. Hashes are MiMC over BN254, and gnark produces Groth16 proofs on the same curve, so they can be verified on Ethereum. Every circuit is generated from the schema. The synthesizer is prover/synth, the prover/*_gen.go files carry its "DO NOT EDIT" header, and make gen-circuits regenerates them. The repo README also says CI diffs the regenerated output, but the current CI workflow doesn't run that check, so nothing mechanical stops a generated file from going stale. The registered set (prover/circuits.go) covers the five ERC-20 actions (transfer, transferFrom, approve, mint, burn), the ERC-5725 vesting claim, and the poll circuits (voteCast and the tally circuits) from ZK Polls.
2. Solidity Contract. States become storage variables, guards become require() statements (solidity/guardgen.go), arcs become storage updates and events become Solidity events. A Foundry test suite and a genesis script are generated alongside the contract. The repo's Foundry end-to-end test generates a contract for each ERC template, runs forge build, deploys it to a local anvil and smoke-tests it. It skips itself when forge isn't installed, it only logs failures from the generated forge test suite, and I didn't re-run it for this revision.
3. .btw DSL. A compact textual syntax for the same models. This is the transfer action from dsl/testdata/erc20.btw, with the other registers, events and actions elided:
schema ERC20 {
version "1.0.0"
...
register ASSETS.AVAILABLE map[address]uint256 observable
...
fn(transfer) {
var from address
var to address
var amount amount
require(ASSETS.AVAILABLE[from] >= amount && amount > 0)
@event TransferBalanceChange
ASSETS.AVAILABLE[from] -|amount|> transfer
transfer -|amount|> ASSETS.AVAILABLE[to]
}
}
The -|amount|> arc syntax reads like a Petri net: consume amount tokens from ASSETS.AVAILABLE[from], produce amount tokens at ASSETS.AVAILABLE[to]. The DSL compiles to metamodel.Schema (dsl/builder.go). That's the type the ERC templates are written in, and the editor's net converts to and from it (internal/petri/bridge.go).
All three outputs are read off one schema: the same states, actions, arcs and guards. I used to say that meant they couldn't diverge. That's too strong. A shared source means a divergence can only come from a generator, never from a hand-kept copy, but the generators do diverge today. The ERC-20 transfer guard is balances[from] >= amount && to != address(0). The Solidity side emits both clauses as require()s, while the generated circuit range-checks only the balance clause, so the circuit would accept a transfer to the zero address that the contract rejects. The generated mint and approve circuits check the role and the post-state leaf but don't prove membership under the pre-state root. Every disagreement is in one place, the generator, and that's what makes it fixable. It isn't yet a guarantee.
The ERC templates are where the abstraction has to hold up. Bitwrap ships five token standards as Petri-net schemas in erc/, plus a vote template:
ERC-20 (fungible tokens): three states (totalSupply, balances, allowances), five actions (transfer, approve, transferFrom, mint, burn). The guard balances[from] >= amount is both a ZK range check and a require() statement.
ERC-721 (NFTs): ownership, per-token approval and operators as keyed states. transferFrom's guard is the authority check (owner, approved address or operator). The template has no separate safeTransferFrom.
ERC-1155 (multi-token): per-token-id balances as a doubly keyed place. The batch operations (safeBatchTransferFrom, mintBatch, burnBatch) are their own transitions, not parallel firings of the single ones.
ERC-4626 (tokenized vaults): deposit, mint, withdraw, redeem and harvest. The share conversion reads totalAssets and totalShares, so the exchange rate is a function of the marking.
ERC-5725 (vesting NFTs): claim is gated by vestedAmount(tokenId) > claimed[tokenId]. revoke is an ordinary guarded transition (creators[tokenId] == caller, the schedule is revocable, and it hasn't already been revoked). There's no inhibitor arc in the template.
The ERC-20 template generates a contract (Solidity ^0.8.20, so arithmetic overflow reverts) with transfer, approve, transferFrom, mint and burn, its events, role checks for owner and minter, and one require() per guard clause.
Every model saved through bitwrap gets a CID. The JSON-LD is canonicalized with URDNA2015 (top-level @id stripped), then hashed with sha2-256 and encoded as CIDv1 (internal/seal/seal.go). The same model always gets the same CID, and the JavaScript side (public/seal-cid.mjs) has to reproduce the Go CIDs for every fixture in parity/golden.json. That's checked by internal/seal/parity_test.go on the Go side and parity/parity_check.mjs on the JS side.
That's most of the loop from OP_RETURN. In 2014 we wanted to anchor structured state to a chain via a hash. Now there's a formal model defining the state machine, a content address identifying it, a ZK proof that a transition was valid under it, and a Solidity contract that enforces the same rules on-chain. The 80-byte hash was pointing at something we hadn't built yet, and the CID of a Petri-net model is the best candidate I have for what it was pointing at. The anchor itself is still open, though. Nothing in bitwrap writes a model's CID into a transaction or into the generated contract, so the link between a deployed contract and the model it came from is, for now, a claim rather than something on-chain.
Bitwrap publishes the witness-side code as dependency-free JavaScript modules that run in the browser: a MiMC-BN254 hash (public/mimc.js), a fixed-depth Merkle tree (public/merkle.js) and witness builders (public/witness-builder.js). The Groth16 prover is also compiled to WebAssembly (public/prover.wasm, run in a Web Worker by public/prover.js). The poll page tries that in-browser prover first and falls back to posting the witness to the server's /api/prove only if it fails (public/poll.js). On the in-browser path the witness (your balance, your position in the Merkle tree) never leaves your machine. On the fallback it does. The server does the proving, which is the very thing ZK is meant to spare you.
When proving stays local, this is the SegWit principle applied to application state: the witness is yours, and the chain sees only the proof.
Bitwrap sits at the top of the pflow ecosystem:
cell, func, arrow, guard)What I'd call the capstone isn't the prover or the Solidity generator taken alone. It's one schema driving both, plus the DSL and the content address, from the same states, arcs and guards. The section above says where the two generators still disagree.
Bitwrap shipped as a hosted app at app.bitwrap.io, with a Remix plugin for deploying from the Solidity IDE and anonymous polls at vote.bitwrap.io. None of it is hosted any more: bitwrap.io now redirects to beats.bitwrap.io, and the project isn't in active development. The code still builds and runs locally. Clone stackdump/bitwrap-io and run make run (Go 1.24+), and the editor, templates, prover and Solidity generator serve on port 8088. Foundry is needed only for the end-to-end contract tests.
For a different take on Petri nets in action, see Petri Nets as a Music Sequencer. It's the same token-flow model, making beats.
Revised 2026-10-28 against the bitwrap-io source (read, not re-run). The witness section now quotes the generated transfer circuit: public inputs include the arguments, the witness is only the touched balances, and the post-state root is a hash of the updated leaves. The ".btw" example is now a verbatim excerpt of dsl/testdata/erc20.btw. The old version dropped && amount > 0 and the @event line. "Six circuits cover ERC-20 operations" counted the ERC-5725 vesting claim as ERC-20 and missed the poll circuits. The ERC-5725 template has no inhibitor arc, because revocation is a guarded transition. The ERC-721 template has no safeTransferFrom, and ERC-1155 batches are separate transitions, not parallel firings. The claim that the three outputs "can't diverge" was wrong. The generated transfer circuit drops the to != address(0) clause the contract enforces, and mint/approve don't prove pre-state membership. "The witness never leaves your browser" held only for the in-browser WASM prover, which now exists and is tried first, not for the server fallback. The unverified "22MB" figure for prover.wasm is gone. The CID description now names the parity tests. The circuit section says the README's CI drift check for generated circuits isn't in the current workflow. "Closes the loop" now says the on-chain anchor of the CID is still unbuilt. The "Try It" links pointed at hosts that no longer serve bitwrap.
Related: Zero-Knowledge Proofs for Petri Nets · ZK Polls: Voting as a Visible State Machine · The Token Language · JSON-LD as Declarative Infrastructure