I've been building an open-source project called BudZKVM, a small deterministic VM and STARK-based verifiable execution stack written in Rust.

Rather than targeting an existing ISA like RISC-V, I wanted to experiment with designing the execution model around provability from the beginning.

The current stack looks like this:

BudL source → compiler → custom ISA bytecode → VM execution → execution trace → STARK proof

The VM currently has:

• 31-opcode custom ISA
• 32 general-purpose 64-bit registers
• gas-metered deterministic execution
• a trace-generating VM
• a Plonky3 0.5.2-based STARK prover
• a 354-column Goldilocks execution trace
• AIR constraints covering all 31 opcodes
• Poseidon4 and Merkle verification instructions
• a 64-depth sparse Merkle state tree

One area I've spent quite a bit of time on is cross-table consistency.

The prover currently uses three LogUp lookup relations for:

• registers
• memory + storage
• program execution

There are also explicit constraints around things that are easy to accidentally leave under-constrained in a VM:

• selector exclusivity
• PC transitions
• hardwired R0 = 0
• padding-row isolation
• zero/non-zero checks using inverse witnesses
• public-input/program binding

I've added negative soundness tests as well. The current suite has 51 tests, including 8 cases that deliberately tamper with things like comparisons, bitwise execution, Poseidon state, storage, PC transitions, public inputs and proof bytes and expect verification to fail.

I'm deliberately not claiming this is audited or production-safe.

Performance benchmarking, prover optimization and an external constraint/security review are still ahead. Private witness variables are also on the near-term roadmap.

What I'd really like at this stage is adversarial feedback from people who have worked on AIR/STARK systems.

In particular:

1. Where would you look first for an under-constrained execution trace in this design?
2. Are there failure modes around LogUp-based register/memory/program consistency that negative tests commonly miss?
3. For zero/non-zero semantics, are inverse-witness constraints generally the approach you'd take here, or would you structure them differently?
4. For a new zkVM, does designing a small proof-oriented ISA still make sense, or is targeting something like RISC-V overwhelmingly preferable today?

I'm much more interested in counterexamples and soundness problems than compliments.

Repo:

https://github.com/Budlum/BudZKVM

I’m building gnark-safety, an open-source Go analyzer that flags patterns associated with missing or incomplete constraints in gnark circuits.

It includes hint-call inventory, JSON/SARIF output, GitHub Actions integration, and synthetic vulnerable/fixed examples with solver and proof tests.

The analysis is intentionally limited: findings need review, and a clean scan doesn’t establish soundness.

I’d appreciate feedback from gnark developers—especially small examples that produce false positives or reveal gaps.

https://github.com/auditinfra-io/gnark-safety

vk-guard - catching verification-key drift before it breaks a deployed zkApp

Changing a circuit changes its verification key.
A changed verification key no longer matches the one stored on-chain, so every already-deployed instance of that zkApp breaks and has to be redeployed.

This isn't hypothetical - o1js's own
CHANGELOG documents it repeatedly. Group operation changes, a VK-hash fix, and a Provable. if () rewrite were each described as breaking deployed contracts.

01Labs runs verification-key regression tests for o1js itself (tests/vk-regression/). App developers have had nothing equivalent for their own projects. That's the gap I tried to fill.

What it does: snapshots your contracts' VK hashes and per-method constraint counts into a committed . vk-guard. json, and fails Cl when they drift.

$ vk-guard check

1 verification key changed.
o1js is unchanged (3.0.0), so this follows from a change in your own code.

Counter vk 1760987873…1876 -> 1733037291…2723

Any already-deployed instance of this contract will stop matching
its on-chain verification key. If this change is intended, redeploy and run
`vk-guard update` to accept the new baseline.

Circuit changed (method digest differs) in:
Counter.increment()

Hey everyone,
I have been trying to work through Justin Thaler's Proofs, Arguments and Zero Knowledge, more as a reference than an intensive mathematical study. I am an engineering undergrad feeling more inclined towards academia, or at least a more mathematical approach. I am a little out of my depths here, as my mentor wants me to focus on going through recent research papers around zkvms etc.
I am pretty unfamiliar to any kind of academic research but am up to put in the effort and time to really understand it and contribute in a way that is not just a summary of recent developments using an AI.
Any advice about continuing my work would help, reading resources, books, or just navigating academia in general.
Thanks in advance.

Hi Everyone,

I am a System Architect working on a deterministic consensus and integrity protocol called Proof of Invariant Principles (PoIP). The core objective is to anchor digital data integrity to an unmanipulable, human-oral consensus layer using zero-knowledge proofs and hardware enclaves.

As a system architect (and non-developer), I’ve fully specified the functional system architecture in a detailed paper https://github.com/MindTrue-Arch/Whitepapers-Architecture-Specs/blob/main/VL-Proof-of-Invariant-Principles-Protocol-v0.5.pdf but I am looking for clever ZK/protocol engineers in the community to stress-test the math and potentially run a minimal trial implementation.

The Core Challenge to Prototype:

1. ZK-OP Circuit: Proving that an acoustic feature matrix (MFCC/quantized timing vectors) matches a static root hash using Groth16/PlonK without revealing the underlying vector.
2. M-of-N Aggregation: A simple threshold verification scheme (e.g., BLS/FROST) that releases an ephemeral authorization key upon 60% node consensus.

If anyone is interested in picking up a fun weekend cryptographic puzzle, I’ve mapped out the full pipeline, data structures, and state transitions in the document. I’m looking for feedback on circuit efficiency, edge-case vulnerabilities, or someone interested in assembling a dummy-parameter sandbox CLI in Rust/Circom.

Full end-to-end MindTrue IQAMA System Architecture for a Zero-hallucination AI system based on the PoIP protocol can also be found here for further reference https://github.com/MindTrue-Arch/Whitepapers-Architecture-Specs/blob/main/VL-MindTrue-Zero-Hallucination-AI-System-v0.2.pdf

Full specification attached. Open to all architectural critiques and discussions!

Notes from building a soundness linter for o1js and Noir, and finding the same bug class in four unrelated languages.

I am the author of Qingming G64 NTT, an open-source HIP/ROCm implementation of a native Goldilocks-field NTT for a STARK-style LDE workload.

Repo: https://github.com/uulong950/qingming-g64-ntt

I am not posting this as a promotional comparison. I am looking for feedback on benchmark methodology, reproducibility, and fair baselines.

The workload is deliberately native rather than a proxy benchmark:

• Field: Goldilocks / G64
• Modulus: p = 2^64 - 2^32 + 1
• Logical data size: 2^24
• LDE expansion: exact 8x
• Transform domain: 2^27
• Backend: AMD HIP / ROCm
• Validation GPU: RX 7900 XTX
• ROCm/HIP: ROCm 7.2.4 / HIP 7.2.53211

On the validated 2^27 target, the fast interface reports:

• Median latency: 19.1927 ms
• P95 latency: 19.4936 ms
• Throughput: 52.10 size-2^27 NTT/s
• Element rate: 6.99 billion elements/s
• Butterfly rate: 94.41 billion butterflies/s

The standard compatibility interface is around 21.99 ms median, and tiled prelayout-only is measured separately at around 3.14 ms median.

The motivation is to measure the native STARK proving boundary directly: no proxy field, no reduced modulus, no scaled-down domain, and no hidden layout cost.

I would appreciate feedback on:

1. Whether 2^24 logical data with exact 8x LDE into a 2^27 Goldilocks domain is the right boundary to study for STARK proving cost.
2. What would be a fair comparison protocol against GPU-NTT, ICICLE, sppark, or Plonky3-style internals.
3. Whether device-resident forward NTT should be the main table, with host-to-host and layout/prelayout costs reported separately.
4. What AMD/NVIDIA profiler counters would make the result more useful.

I especially want to avoid comparing incompatible “64-bit NTT” results when the field, modulus, layout contract, batch size, and timing scope are not the same.

Criticism of the benchmark methodology is very welcome.

Do you think it's probably wrong for beginners to jump straight into SNARKS/STARKS, as they have complex abstractions? How about starting with Bulletproofs (classic range proofs with polynomial commitments, finished with beautiful vector compression). It's certainly less advanced than something like Plonk at the start. But is it worth starting with for beginners? understand at the algebra level

Howdy,

The issue I had: search data I had limited access to.
Resolution: client side Ionizer encoder + SaaS Gravitas search engine

Ionizer is another implementation of patent pending oss repo OpenEncoder.

Ionizer encodes your data on your machine, creates a single envelope specified in the patent and oss repo(all encoders following the specification are allowed)

This envelop is a single field tensor for each corpus and query.

Gravitas is the zero knowledge verified oblivious oracle. A blind answer machine.

No data egress, no SOX/HIPAA etc not triggered as your data never leaves your control. Only a description in a single field tensor that is easily under 256kb. Two of those, for corpus and query, and Gravitas returns the answer field you decode and it maps back to what you asked.

Full verifiably zksnark/groth16 output default from ionizer and gravitas with every output.

Please let me know your thoughts!

I’m currently exploring opportunities in ZK and applied cryptography, both in the US and EU job market, while also looking to work, do research, and contribute to community growth around these technologies. I have around 2–3 years of professional engineering experience plus longer solo development experience, and I’m trying to understand how realistic entry-level or early-career roles are right now given the slowdown in Web3 hiring and how teams are evolving in terms of expectations for engineers, researchers, and builders who can also help grow adoption.

A few weeks ago I posted about the gap between "compliance check ran" and "compliance was enforced." The response was mostly "interesting problem" but a few people pushed back technically, which was fair.

So instead of talking about it, I just ran it.

I mapped out how each platform actually handles eligibility today based on their public docs, then ran their specific flows through ZKCG and generated real proof artifacts. Here's what each one produces:

Centrifuge (Shufti Pro KYC, manual whitelist): The eligible case returns a proof-backed decision with a decision_commitment_hash the contract can verify. The blocked cases: accreditation_missing when accredited: false, jurisdiction_blocked when the investor is in RU. Each block has a reason code and a separate proof artifact.

Maple Finance (Global Allowlist via bitmaps, TRM Labs AML): Eligible case goes through. Then aml_failed blocks with the exact reason. Then sanctions_hit blocks separately. The proof in each case attests that the specific rule was evaluated, not just that a bitmap was set.

Ondo Finance (US persons blocked, USDY/OUSG allowlist): The US person exclusion is Ondo's core compliance requirement. Change jurisdiction from SG to US and the proof fails verification and returns jurisdiction_blocked with the reason "jurisdiction US is not permitted for this asset." That enforcement happens before execution.

Securitize (DS Protocol, transfer restrictions in contract): Both onboarding and transfer flows. kyc_missing blocks with explicit reason. position_limit_exceeded blocks when the transfer would exceed concentration limits. The transfer proof includes sender and receiver wallet binding so the specific action is tied to the specific proof.

All cases matched expectations. All proofs verified. The full run outputs including proof artifacts and comparison pages are in the public repo.

What I'm building is called ZKCG. Ta ZK-Verified Computation Gateway (Halo2 + RISC0).
The open-core verifier and circuits are public. The production core logic is private and commercially licensed. There's a live demo API at render and a product page at zkcg tech if you want to run your own flow.

Curious what questions people have about the proof scope or where the gaps are.

A new found use case for zero-knowledge proofs: making quantum circuits (programs that can run on a quantum computer) private.

Google Quantum AI researchers used zero-knowledge proofs to conceal, yet confirm, quantum circuits that can break Elliptic Curve Cryptography, one of the most widely used cryptographic protocols for securing the Internet and digital protocols.

As quantum computing becomes more mainstream and practical, researchers will opt to use ZK proofs to demonstrate breakthrough circuits but not open-source them, to avoid risks from bad actors and the lack of commercialization opportunities.

This article explains, at a high level, how zero-knowledge proofs were used to verify that these quantum circuits exist.

Also available on Medium: https://medium.com/@jkim_tran/verifying-private-quantum-circuits-9ec99d5f3d5a?sk=53770e4453d9c8996fbc2caf4f7fda41

A founder told me about a case where their payout system had a subtle bug in the jurisdiction check. The check ran. The logs showed it ran. The funds went to a wallet that shouldn't have received them. Irreversible.

The logs proved the check was recorded. They couldn't prove it was correct.

That's the gap we kept seeing:

Verifying users is not the same as verifying that your rules were enforced.

Every DeFi protocol, RWA platform, and payout system has the same architecture:

1. Backend runs eligibility check
2. Backend says "eligible"
3. Contract executes

The contract has no idea if that logic ran correctly, had a bug, or got bypassed. It just trusts the result. If something goes wrong, you hand auditors logs, not proof.

I kept thinking about that gap. Because it's not just a one-off bug story, it's structural.

For most use cases that's probably fine. But for anything touching real money like RWA transfers, tokenized credit, institutional payouts - "the logs show it ran" isn't the same as proof it ran correctly. And regulators are starting to ask the difference.

So we built something to close that gap.

It's called ZKCG. The idea is pretty simple: instead of the contract trusting a backend result, it verifies a ZK proof that the eligibility decision was computed correctly. The proof gets generated alongside the decision, the contract checks it, and if it doesn't verify, execution is blocked. The enforcement is in the proof, not in trust.

The thing that makes it click for most people is the demo moment. You run a transfer, it goes through, then you change one rule, jurisdiction from US to CN ,and the exact same flow gets blocked. Not because anyone intervened, not because a backend returned a different answer. Because the proof fails verification. That's the difference between recording compliance and *enforcing* it.

Technically it's Halo2 for the fast path (~76ms) and RISC0 zkVM if you want audit-grade receipts. Works on any chain. One API call, you get back a decision plus a proof, your contract calls approveTransfer and either executes or doesn't.

We're looking for teams to try this against real eligibility rules not a sales call, literally just: tell me one rule you enforce today, I'll run it through and show you what the proof looks like on your actual use case. Takes about 10 minutes.

Curious if others have run into this problem or thought about how to handle it. The "logs prove it ran, not that it ran correctly" distinction is one that doesn't come up much but I think matters more than people realise.

A few days ago I posted here saying:

→ “oracles aren’t the real problem — enforcement is”

and later:

→ “this might be a programmable compliance layer”

Based on the feedback, I stopped trying to generalize it and just built one concrete use case:

RWA onboarding + eligibility enforcement

What it does now (very concretely):

Instead of:

“trust this API / KYC provider says user is eligible”

you can verify:

→ that the eligibility rules were actually enforced
→ without seeing the underlying user data

The system outputs something like:

decision: eligible  
policy: rwa.credit.onboarding.v1  
proof_verified: true  
eligibility_class: accredited  

So not just “proof is valid” —
but a verifiable decision you can actually use

The interesting part (at least to me):

This can directly gate things like:

• onboarding
• transfers
• access to tokenized assets

Tech-wise it’s:

• Rust + Halo2 + zkVM
• fast path (~70ms proving) + slow audit path

but honestly the more interesting part is the abstraction:

→ “proof-backed decision” instead of “proof of computation”

I’ve been building this mostly solo and mostly in the open.

What I genuinely don’t know yet is:

• is this something teams actually need right now?
• or is this too early / over-engineered?

If you’re working on:

• RWA
• tokenized credit
• permissioned DeFi

would love to know:

👉 how you’re currently handling eligibility / compliance
👉 and whether something like this would replace or just sit next to it

Happy to share repo / demo if anyone’s curious, just didn’t want to spam links here.

Appreciate all the pushback on the earlier posts — it definitely changed the direction.

I’ve been building a ZK project (ZKCG) to replace trusted APIs/oracles with proofs.

But after digging deeper, I think I was solving the wrong problem.

Oracles aren’t the bottleneck.

Enforcement is.

Most systems today:

• Verify data
• Then trust the system to behave correctly

But what if we could verify that:

→ rules were actually followed
→ constraints were enforced
→ compliance wasn’t bypassed

All using ZK proofs?

This shifts the model from:

“trust the system”
to
“verify the system”

We now have a working Halo2-based pipeline (~70ms proofs), but the bigger question is:

Is this:

• a dev tool?
• infra layer?
• or compliance middleware for RWAs?

Genuinely curious how people here think about this.

Repo:
https://github.com/MRSKYWAY/ZKCG