Adrien Champion
AdrienChampion
Independent R&D Engineer in Lean 4 and Rust (and OCaml if I have to)
Languages
Repos
56
Stars
71
Forks
12
Top Language
Rust
Loading contributions...
Top Repositories
Repositories
56No description provided.
A Rust hashconsing library.
Type-safe indexing library.
Experimenting with lean4
A Horn Clause ICE engine.
Safe indexing in Rust.
Standard Library for Lean 4
A date and time library for Lean 4
Tactics for discharging Lean goals into SMT solvers.
Testing dynamic term loading in Lean 4.
Fast expressions.
Theorem Proving in Lean 4
Information about my GitHub profile
Type-erased Serialize, Serializer and Deserializer traits
Interact with SMT-LIB 2 compliant solvers in Lean 4
Tagless parser library in Lean 4.
Benchmark easily with `benchi`
A manager for TLA+ projects.
No description provided.
No description provided.
Empowering everyone to build reliable and efficient software.
No description provided.
TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
A simple induction and BMC engine.
Work in progress mathlib port for lean 4
Lean 4 programming language and theorem prover
A small Rust library providing a helper macro for implementing common traits.
Induction as a formal program verification technique for the uninitiated.
No description provided.
A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.