Roadmap
Legend
Completed
In Progress
Last Updated: April 17th, 2025
+
-
Reset
AleoBFT
Leo
AleoVM
Provers
Completed
2025
2025
Goals
Future
Future
Goals
P2P
networking
Node implementation
Narwhal +
Bullshark
Formal verification
AleoBFT
non-forking
Syncing
Dynamic committees
Stress test
infrastructure
Formal verification
AleoBFT syncing
Automated ephemeral
test environments
Optimize
caching
Speed up
cryptographic
primitives
Optimize Deserialization
Increase batch size &
limits
2x faster confirmation
times
100+ L1 TPS
40+ Validators
Formal verification
AleoBFT liveness
Explore new SNARK-
friendly hash function
Batch verification
SNARK-based light
clients
Explore
preconfirmations
Streamline transaction
propagation
Fast & trust-
minimized data
access
1000+ L1 TPS
100+ validators
Synthesis acceleration
Batch proposal spend
limits
Program upgradability
FFT
BLS12-337 &
edwards-BLS12
Elliptic Curves
Powers of Tau trusted
setup
Priority fees
Batch Proving &
Verification
Lineval
Field, Group
& Scalar
element types
Arrays
Adress &
Signature types
Core Virtual Machine
Varuna SNARK
Fee Metering
credits.aleo
Async-await
Delegable
ZK proofs
Support for
interoperable DeFi
Support for paymaster
2**22 sized circuits
10x lower fees
Dynamic
base-fees
Flagged opcodes
Snark.verify opcode
Native Merkle
tree opcodes
Formally verify
all opcodes
Formally verify Virtual
Machine
Explore programs over
shared
private state
Explore account
abstraction
Explore tradsig
verification gadgets
Data relays
Program function
interfaces
Dynamic dispatch
Permissionless token
contract
Enable fee abstraction
Chain interoperability
Flexible, secure and
cheap account access
2**28 sized
expressive circuits
Formally verified VM
Compile time function
evaluation
Constant-folding
Array and struct
assignment
Leo Test Framework
Leo debugger
Parser
Semantic
analysis
Optimizations
Code generation
Futures
Leo deploy & execute
Program Upgradability
Const generics
Leo tx verification
Double speed of
development
Complete ABNF
grammar
Increase Leo
expressiveness
Leo core libraries
Assertion codegen
ergonomics
Sum types
E2E ALC2 pipeline
Formally verifying
complier
World-class developer
experiance
Formal model Parser
Language ergonomics
& type interference
Dynamic collections
Dynamic dispatch
Circom-Leo transpiler
Most intuitive ZK-
native development
Delegated synthesis
ZPrize
MSM prover puzzle
Syntesis prover puzzle
Increase #
and type of
instructions
Formal verification
puzzle semantics
Biggest delegated
proof generation
market
SNARK ASICs
Proving Marketplace
Full SNARK prover
puzzle (ARC-43)
After the successful formal verification of consensus, syncing logic is formally modeled to
assure safety under all possible network conditions and attack vectors.
On every new Aleo release, a wide variety of network simulations will be run in a fully
automated way to continue the stability achieved by the Aleo network since launch.
A holistic evaluation of consensus operations will ensure maximising and
timing CPU utilization, further improving scalability.
Program Upgradability is the capacity to modify or enhance a deployed program,
and enabling it in Aleo fosters dynamic improvements, better security
and longevity for decentralized applications.
Spend limit checks at the construction of batch proposals in the AleoBFT mechanism.
This enables lower transaction costs while maintaining security.
Deployed program sizes are bottlenecked by slow synthesis; accelerating this is key to unlock
scalability and to support large program sizes on the Aleo network.
Lets you assign and manipulate arrays or structs directly for simpler data handling.
Provides interactive debugging to spot and fix errors quickly.
Try out the first version today using leo debug!
Simplifies testing with a unified environment for checking program behavior.
Speeds up execution by evaluating constant expressions at compile time.
Executes functions at compile time for faster, optimized code.
In the road to updating Aleo's existing synthesis puzzle to a full SNARK prover puzzle,
we are first tackling the computational and potentially game theoretic challenge
of delegated synthesis - allowing validators to outsource synthesis to a fast, external prover
https://github.com/ProvableHQ/ARCs/discussions/77
