@argot.org.bsky.social
Non-profit, independent collective building and maintaining the core infrastructure for Ethereum applications. visit argot.org
We'd love feedback from the formal methods & smart contract security community.
Reach out via act@argot.org 💛
Who is act for?
Security researchers and smart contract engineers who want stronger guarantees than audits alone can provide. If you care about provable correctness for Ethereum contracts, act is for you.
📦 Repo + release: github.com/argotorg/ac...
4️⃣ Documentation & Tooling:
Complete documentation including installation guide, language reference, tutorials, and examples.
5️⃣ Supporting Features:
CLI with SMT solver integration (Z3, CVC5, Bitwuzla) and Rocq project templates.
3️⃣ Verification backends:
• Automatically check equivalence between implementation and act specification at the bytecode level via symbolic execution and hevm (currently supporting Solidity and Vyper)
• Interactive theorem proving of high-level properties with Rocq
2️⃣ Type-Checking System:
Formally verified sound static type-checking combined with SMT-based semantic verification (arithmetic bounds, preconditions, case exhaustiveness) and automatic aliasing checks.
v0.2.0 is a complete rework and significant extension of the initial prototype (v0.1.0) and here's what we're shipping:
1️⃣ The act Specification Language:
A high-level specification language for EVM smart contracts with support for interleaved contracts (reasoning about multiple contracts together)
Why act?
Audits and tests catch bugs, but they don't prove correctness.
act bridges human-readable specs and EVM bytecode by formally verifying their equivalence, enabling high-assurance contracts across Solidity, Vyper, and beyond.
We're excited to announce the first official release of act (v0.2.0):
a formal specification language and verification framework for Ethereum smart contracts, built within the Argot Collective.
This is a major step in our research toward safer on-chain systems. ↓✨
3️⃣ Verification backends:
• Automatically check equivalence between implementation and Act specification at the bytecode level via symbolic execution and hevm (currently supporting Solidity and Vyper)
• Interactive theorem proving of high-level properties with Rocq
2️⃣ Type-Checking System:
Formally verified sound static type-checking combined with SMT-based semantic verification (arithmetic bounds, preconditions, case exhaustiveness) and automatic aliasing checks.
v0.2.0 is a complete rework & significant extension of the initial prototype (v0.1.0) and here's what we're shipping:
1️⃣ The Act Specification Language:
A high-level specification language for EVM smart contracts with support for interleaved contracts (reasoning about multiple contracts together)
Why Act?
Audits and tests catch bugs, but they don't prove correctness.
Act bridges human-readable specs and EVM bytecode by formally verifying their equivalence, enabling high-assurance contracts across @solidity_lang, @vyperlang, and beyond.
If you value open-source compiler infrastructure and accountable public-goods stewardship, consider supporting Argot.
Donations directly fund core contributor work and help ensure the long-term sustainability of critical Ethereum tooling.
➡️ Read the full report here: www.argot.org/reports/tra...
We are grateful to our early supporters, including the @ethereumfndn, @OctantApp, @ENS_DAO, @Optimism, and @gitcoin.
While EF provides initial runway, diversifying funding is essential for Argot’s long-term independence and resilience.
And of course our budget and expenses:
From July 1 to Dec 31, 2025, total expenditures were $2,443,067.
Salaries represent the largest share of spending, reflecting our focus on direct contributor support.
A detailed project-level breakdown is available on our website: argot.org/reports
The report includes administrative updates:
• Argot's incorporation
• Transfer of employment contracts and operations from EF to Argot
• Projects migration from the Ethereum GitHub org to Argot’s org
• New hires (ops, fundraising, Solidity engineer)
We commit to publishing detailed disclosures of internal and external expenditures every six months.
This first report covers the period after our incorporation in July 2025, with primary expenses supporting continued work on Solidity, Sourcify, hevm, Fe, ethdebug, and act.
Today, we are publishing our first Transparency Report.
Financial and organizational transparency is a core value for us: public-goods stewardship must be grounded in openness, traceability, and clear responsibility.
Visit our blog to read about recent milestones and upcoming work of
Solidity, Sourcify, Fe, ethdebug, Act, and hevm: www.argot.org/blog/2026-0...
Our bi-annual roadmap update is live:
a recap of what Argot delivered across the collective in the second half of 2025, and a forward-looking outlook into the first half of 2026. ✨
Find the link below ↓
Explore hevm v0.57.0 now and check out the full change log here:
👉 github.com/argotorg/he...
And as always: thanks to everyone who contributed and reported issues - your feedback drives these improvements ❤️
In addition, hevm can now handle symbolic powers of 2 without giving up.
An important step toward full support for symbolic exponentiation. 💫
hevm v0.57.0 also includes several under-the-hood improvements:
a simplified internal rewriting framework with a bug fix to ensure more accurate results, and a new RPC cache so analysis is no longer slowed down by repeated RPC requests. ✨
We also introduced more controlled parallelism.
hevm is now far less likely to exhaust system resources when analyzing complex contracts with large branching factors. 🔥🔥
The biggest performance gains come from improved infeasible path pruning.
hevm can now detect some infeasible paths earlier, significantly reducing the search space and delivering much faster results on real-world contracts. 🔥
hevm is starting the year strong: v0.57.0 just landed 🚀
The release delivers meaningful improvements to the performance and reliability of symbolic exploration, with a clear impact on real-world contract analysis.↓
We’re finishing the final pieces now.
Expect the long-awaited Fe release toward the end of Q1 2026. 🥳
In the meantime, join the discussion and get the latest updates here: fe-lang.zulipchat.com/join/dqvssg...
💪 To note:
Research developed through Sonatina (as prev. outlined here: www.argot.org/blog/2025-r...) will carry forward into Core Solidity research as its core contributor transitions to the Solidity team - showcasing the strength of the collective, where work on one project informs another.
The old contract model was replaced with a new message-passing syntax that feels native to the EVM: cleaner, safer, & free of the structural issues that haunted earlier versions.
On top of that: a native package manager, a robust LSP, a strict formatter, & a new fe-lang.org with comprehensive docs.
Major language upgrades:
• A fully overhauled type system
• Generics, Traits, and Higher-Kinded Types
• So expressive the Fe standard library is written in Fe itself
