diff --git a/Cargo.toml b/Cargo.toml
index 4e06422..7bdf689 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,6 +4,7 @@ members = [
     "curve25519",
     "chacha20",
     "poly1305",
+    "poly1305-rust",
     "chacha20poly1305",
     "gimli",
     "sha256",
diff --git a/poly1305-rust/Cargo.toml b/poly1305-rust/Cargo.toml
new file mode 100644
index 0000000..0ea01a0
--- /dev/null
+++ b/poly1305-rust/Cargo.toml
@@ -0,0 +1,23 @@
+[package]
+name = "poly1305"
+version = "0.1.0"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "hacspec poly1305 message authentication code"
+readme = "README.md"
+repository = "https://github.com/hacspec/specs"
+
+[lib]
+path = "src/poly1305.rs"
+
+[dependencies]
+num-bigint = "0.4"
+natmod = { path = "./natmod" }
+
+[dev-dependencies]
+serde_json = "1.0"
+serde = { version = "1.0", features = ["derive"] }
+rayon = "1.3.0"
+criterion = "0.4"
+rand = "0.8"
diff --git a/poly1305-rust/natmod/Cargo.toml b/poly1305-rust/natmod/Cargo.toml
new file mode 100644
index 0000000..7cacd43
--- /dev/null
+++ b/poly1305-rust/natmod/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "natmod"
+version = "0.1.0"
+edition = "2021"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+
+[lib]
+proc-macro = true
+
+[dependencies]
+hex = "0.4.3"
+num-bigint = "0.4.3"
+quote = "1.0.28"
+syn = { version = "2.0.18", features = ["full"] }
diff --git a/poly1305-rust/natmod/src/lib.rs b/poly1305-rust/natmod/src/lib.rs
new file mode 100644
index 0000000..404a421
--- /dev/null
+++ b/poly1305-rust/natmod/src/lib.rs
@@ -0,0 +1,134 @@
+//! // This trait lives in the library
+//! pub trait NatModTrait<T> {
+//!     const MODULUS: T;
+//! }
+//!
+//! #[nat_mod("123456", 10)]
+//! struct MyNatMod {}
+
+use hex::FromHex;
+use proc_macro::TokenStream;
+use quote::quote;
+use syn::{parse::Parse, parse_macro_input, DeriveInput, Ident, LitInt, LitStr, Result, Token};
+
+#[derive(Clone, Debug)]
+struct NatModAttr {
+    /// Modulus as hex string and bytes
+    mod_str: String,
+    mod_bytes: Vec<u8>,
+    /// Number of bytes to use for the integer
+    int_size: usize,
+}
+
+impl Parse for NatModAttr {
+    fn parse(input: syn::parse::ParseStream) -> Result<Self> {
+        let mod_str = input.parse::<LitStr>()?.value();
+        let mod_bytes = Vec::<u8>::from_hex(&mod_str).expect("Invalid hex String");
+        input.parse::<Token![,]>()?;
+        let int_size = input.parse::<LitInt>()?.base10_parse::<usize>()?;
+        assert!(input.is_empty(), "Left over tokens in attribute {input:?}");
+        Ok(NatModAttr {
+            mod_str,
+            mod_bytes,
+            int_size,
+        })
+    }
+}
+
+#[proc_macro_attribute]
+pub fn nat_mod(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let item_ast = parse_macro_input!(item as DeriveInput);
+    let ident = item_ast.ident.clone();
+    let args = parse_macro_input!(attr as NatModAttr);
+
+    let num_bytes = args.int_size;
+    let modulus = args.mod_bytes;
+    let modulus_string = args.mod_str;
+
+    let mut padded_modulus = vec![0u8; num_bytes - modulus.len()];
+    padded_modulus.append(&mut modulus.clone());
+    let mod_iter1 = padded_modulus.iter();
+    let mod_iter2 = padded_modulus.iter();
+    let const_name = Ident::new(
+        &format!("{}_MODULUS", ident.to_string().to_uppercase()),
+        ident.span(),
+    );
+    let static_name = Ident::new(
+        &format!("{}_MODULUS_STR", ident.to_string().to_uppercase()),
+        ident.span(),
+    );
+    let mod_name = Ident::new(
+        &format!("{}_mod", ident.to_string().to_uppercase()),
+        ident.span(),
+    );
+
+    let out_struct = quote! {
+        #[derive(Clone, Copy, PartialEq, Eq)]
+        pub struct #ident {
+            value: [u8; #num_bytes],
+        }
+
+        //#[not_hax]
+        #[allow(non_snake_case)]
+        mod #mod_name {
+            use super::*;
+
+            const #const_name: [u8; #num_bytes] = [#(#mod_iter1),*];
+            static #static_name: &str = #modulus_string;
+
+            impl NatMod<#num_bytes> for #ident {
+                const MODULUS: [u8; #num_bytes] = [#(#mod_iter2),*];
+                const MODULUS_STR: &'static str = #modulus_string;
+                const ZERO: [u8; #num_bytes] = [0u8; #num_bytes];
+
+
+                fn new(value: [u8; #num_bytes]) -> Self {
+                    Self {
+                        value
+                    }
+                }
+                fn value(&self) -> &[u8] {
+                    &self.value
+                }
+            }
+
+            impl core::convert::AsRef<[u8]> for #ident {
+                fn as_ref(&self) -> &[u8] {
+                    &self.value
+                }
+            }
+
+            impl core::fmt::Display for #ident {
+                fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
+                    write!(f, "{}", self.to_hex())
+                }
+            }
+
+
+            impl Into<[u8; #num_bytes]> for #ident {
+                fn into(self) -> [u8; #num_bytes] {
+                    self.value
+                }
+            }
+
+            impl core::ops::Add for #ident {
+                type Output = Self;
+
+                fn add(self, rhs: Self) -> Self::Output {
+                    self.fadd(rhs)
+                }
+            }
+
+
+            impl core::ops::Mul for #ident {
+                type Output = Self;
+
+                fn mul(self, rhs: Self) -> Self::Output {
+                    self.fmul(rhs)
+                }
+            }
+        }
+    };
+
+    out_struct.into()
+}
diff --git a/poly1305-rust/natmod/tests/poly1305.rs b/poly1305-rust/natmod/tests/poly1305.rs
new file mode 100644
index 0000000..4e27590
--- /dev/null
+++ b/poly1305-rust/natmod/tests/poly1305.rs
@@ -0,0 +1,172 @@
+use natmod::nat_mod;
+
+/// This has to come from the lib.
+
+pub trait NatMod<const LEN: usize> {
+    const MODULUS: [u8; LEN];
+    const MODULUS_STR: &'static str;
+    const ZERO: [u8; LEN];
+
+    fn new(value: [u8; LEN]) -> Self;
+    fn value(&self) -> &[u8];
+
+    /// Add self with `rhs` and return the result `self + rhs % MODULUS`.
+    fn fadd(self, rhs: Self) -> Self
+    where
+        Self: Sized,
+    {
+        let lhs = num_bigint::BigUint::from_bytes_be(self.value());
+        let rhs = num_bigint::BigUint::from_bytes_be(rhs.value());
+        let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS);
+        let res = (lhs + rhs) % modulus;
+        let res = res.to_bytes_be();
+        assert!(res.len() <= LEN);
+        let mut value = Self::ZERO;
+        let offset = LEN - res.len();
+        for i in 0..res.len() {
+            value[offset + i] = res[i];
+        }
+        Self::new(value)
+    }
+
+    /// Multiply self with `rhs` and return the result `self * rhs % MODULUS`.
+    fn fmul(self, rhs: Self) -> Self
+    where
+        Self: Sized,
+    {
+        let lhs = num_bigint::BigUint::from_bytes_be(self.value());
+        let rhs = num_bigint::BigUint::from_bytes_be(rhs.value());
+        let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS);
+        let res = (lhs * rhs) % modulus;
+        let res = res.to_bytes_be();
+        assert!(res.len() <= LEN);
+        let mut value = Self::ZERO;
+        let offset = LEN - res.len();
+        for i in 0..res.len() {
+            value[offset + i] = res[i];
+        }
+        Self::new(value)
+    }
+
+    /// Returns 2 to the power of the argument
+    fn pow2(x: usize) -> Self
+    where
+        Self: Sized,
+    {
+        let res = num_bigint::BigUint::from(1u32) << x;
+        Self::from_bigint(res)
+    }
+
+    /// Create a new [`#ident`] from a `u128` literal.
+    fn from_u128(literal: u128) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from(literal))
+    }
+
+    /// Create a new [`#ident`] from a little endian byte slice.
+    fn from_le_bytes(bytes: &[u8]) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from_bytes_le(bytes))
+    }
+
+    /// Create a new [`#ident`] from a little endian byte slice.
+    fn from_be_bytes(bytes: &[u8]) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from_bytes_be(bytes))
+    }
+
+    fn to_le_bytes(self) -> [u8; LEN]
+    where
+        Self: Sized,
+    {
+        Self::pad(&num_bigint::BigUint::from_bytes_be(self.value()).to_bytes_le())
+    }
+
+    /// Get hex string representation of this.
+    fn to_hex(&self) -> String {
+        let strs: Vec<String> = self.value().iter().map(|b| format!("{:02x}", b)).collect();
+        strs.join("")
+    }
+
+    /// New from hex string
+    fn from_hex(hex: &str) -> Self
+    where
+        Self: Sized,
+    {
+        assert!(hex.len() % 2 == 0);
+        let l = hex.len() / 2;
+        assert!(l <= LEN);
+        let mut value = [0u8; LEN];
+        let skip = LEN - l;
+        for i in 0..l {
+            value[skip + i] = u8::from_str_radix(&hex[2 * i..2 * i + 2], 16)
+                .expect("An unexpected error occurred.");
+        }
+        Self::new(value)
+    }
+
+    fn pad(bytes: &[u8]) -> [u8; LEN] {
+        let mut value = [0u8; LEN];
+        let upper = value.len();
+        let lower = upper - bytes.len();
+        value[lower..upper].copy_from_slice(&bytes);
+        value
+    }
+
+    fn from_bigint(x: num_bigint::BigUint) -> Self
+    where
+        Self: Sized,
+    {
+        let max_value = Self::MODULUS;
+        assert!(
+            x <= num_bigint::BigUint::from_bytes_be(&max_value),
+            "{} is too large for type {}!",
+            x,
+            stringify!($ident)
+        );
+        let repr = x.to_bytes_be();
+        if repr.len() > LEN {
+            panic!("{} is too large for this type", x)
+        }
+
+        Self::new(Self::pad(&repr))
+    }
+}
+
+#[nat_mod("03fffffffffffffffffffffffffffffffb", 17)]
+struct FieldElement {}
+
+#[test]
+fn add() {
+    let x = FieldElement::from_hex("03fffffffffffffffffffffffffffffffa");
+    let y = FieldElement::from_hex("01");
+    let z = x + y;
+    assert_eq!(FieldElement::ZERO.as_ref(), z.as_ref());
+
+    let x = FieldElement::from_hex("03fffffffffffffffffffffffffffffffa");
+    let y = FieldElement::from_hex("02");
+    let z = x + y;
+    assert_eq!(FieldElement::from_hex("01").as_ref(), z.as_ref());
+}
+
+#[test]
+fn mul() {
+    let x = FieldElement::from_hex("03fffffffffffffffffffffffffffffffa");
+    let y = FieldElement::from_hex("01");
+    let z = x * y;
+    assert_eq!(x.as_ref(), z.as_ref());
+
+    let x = FieldElement::from_hex("03fffffffffffffffffffffffffffffffa");
+    let y = FieldElement::from_hex("02");
+    let z = x * y;
+    assert_eq!(
+        FieldElement::from_hex("03fffffffffffffffffffffffffffffff9").as_ref(),
+        z.as_ref()
+    );
+}
diff --git a/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst b/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst
new file mode 100644
index 0000000..e5516bc
--- /dev/null
+++ b/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst
@@ -0,0 +1,68 @@
+module Poly1305.FIELDELEMENT_mod
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+
+let v_FIELDELEMENT_MODULUS: array u8 17sz =
+  (let l =
+      [
+        3uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy;
+        255uy; 255uy; 255uy; 251uy
+      ]
+    in
+    assert_norm (List.Tot.length l == 17);
+    Rust_primitives.Hax.array_of_list l)
+
+let impl: Poly1305.Hacspec_helper.t_NatMod Poly1305.t_FieldElement 17sz =
+  {
+    mODULUS
+    =
+    (fun  ->
+        (let l =
+            [
+              3uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy;
+              255uy; 255uy; 255uy; 255uy; 251uy
+            ]
+          in
+          assert_norm (List.Tot.length l == 17);
+          Rust_primitives.Hax.array_of_list l));
+    mODULUS_STR = (fun  -> "03fffffffffffffffffffffffffffffffb");
+    zERO = (fun  -> Rust_primitives.Hax.repeat 0uy 17sz);
+    new_ = (fun (value: array u8 17sz) -> { Poly1305.FieldElement.f_value = value });
+    value
+    =
+    fun (self: Poly1305.t_FieldElement) -> Rust_primitives.unsize self.Poly1305.FieldElement.f_value
+  }
+
+let impl: Core.Convert.t_AsRef Poly1305.t_FieldElement (slice u8) =
+  {
+    as_ref
+    =
+    fun (self: Poly1305.t_FieldElement) -> Rust_primitives.unsize self.Poly1305.FieldElement.f_value
+  }
+
+(* 
+Last available AST for this item:
+
+/* TO DO */
+ *)
+
+let impl: Core.Convert.t_Into Poly1305.t_FieldElement (array u8 17sz) =
+  { into = fun (self: Poly1305.t_FieldElement) -> self.Poly1305.FieldElement.f_value }
+
+let impl: Core.Ops.Arith.t_Add Poly1305.t_FieldElement Poly1305.t_FieldElement =
+  {
+    output = Poly1305.t_FieldElement;
+    add
+    =
+    fun (self: Poly1305.t_FieldElement) (rhs: Poly1305.t_FieldElement) ->
+      Poly1305.Hacspec_helper.NatMod.fadd self rhs
+  }
+
+let impl: Core.Ops.Arith.t_Mul Poly1305.t_FieldElement Poly1305.t_FieldElement =
+  {
+    output = Poly1305.t_FieldElement;
+    mul
+    =
+    fun (self: Poly1305.t_FieldElement) (rhs: Poly1305.t_FieldElement) ->
+      Poly1305.Hacspec_helper.NatMod.fmul self rhs
+  }
\ No newline at end of file
diff --git a/poly1305-rust/proofs/fstar/extraction/Poly1305.fst b/poly1305-rust/proofs/fstar/extraction/Poly1305.fst
new file mode 100644
index 0000000..8905cd3
--- /dev/null
+++ b/poly1305-rust/proofs/fstar/extraction/Poly1305.fst
@@ -0,0 +1,119 @@
+module Poly1305
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+
+let t_PolyKey = array u8 32sz
+
+let v_BLOCKSIZE: usize = 16sz
+
+let t_PolyBlock = array u8 16sz
+
+let t_Poly1305Tag = array u8 16sz
+
+let t_SubBlock = Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+
+let t_BlockIndex = usize
+
+type t_FieldElement = { f_value:array u8 17sz }
+
+type t_PolyState = {
+  f_acc:t_FieldElement;
+  f_r:t_FieldElement;
+  f_key:array u8 32sz
+}
+
+let poly1305_encode_r (b: array u8 16sz) : t_FieldElement =
+  let n:u128 = Core.Num.from_le_bytes_under_impl_10 b in
+  let n:u128 = n &. pub_u128 21267647620597763993911028882763415551sz in
+  Poly1305.Hacspec_helper.NatMod.from_u128 n
+
+let poly1305_encode_block (b: array u8 16sz) : _ =
+  let f:t_FieldElement = Poly1305.Hacspec_helper.NatMod.from_le_bytes (Rust_primitives.unsize b) in
+  f +. Poly1305.Hacspec_helper.NatMod.pow2 128sz
+
+let poly1305_encode_last (pad_len: usize) (b: slice u8) : _ =
+  let f:t_FieldElement = Poly1305.Hacspec_helper.NatMod.from_le_bytes b in
+  f +. Poly1305.Hacspec_helper.NatMod.pow2 (8sz *. pad_len)
+
+let poly1305_init (key: array u8 32sz) : t_PolyState =
+  let r:t_FieldElement =
+    poly1305_encode_r (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into key.[ {
+                  Core.Ops.Range.Range.f_start = 0sz;
+                  Core.Ops.Range.Range.f_end = 16sz
+                } ]))
+  in
+  {
+    Poly1305.PolyState.f_acc = Poly1305.Hacspec_helper.NatMod.zero;
+    Poly1305.PolyState.f_r = r;
+    Poly1305.PolyState.f_key = key
+  }
+
+let poly1305_update_block (b: array u8 16sz) (st: t_PolyState) : t_PolyState =
+  let st:t_PolyState =
+    {
+      st with
+      Poly1305.PolyState.f_acc
+      =
+      (poly1305_encode_block b +. st.Poly1305.PolyState.f_acc) *. st.Poly1305.PolyState.f_r
+    }
+  in
+  st
+
+let poly1305_update_blocks (m: slice u8) (st: t_PolyState) : t_PolyState =
+  let st:t_PolyState =
+    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks_exact_under_impl
+              m
+              v_BLOCKSIZE))
+      st
+      (fun st chunk ->
+          poly1305_update_block (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into chunk)
+            )
+            st)
+  in
+  st
+
+let poly1305_update_last (pad_len: usize) (b: slice u8) (st: t_PolyState) : t_PolyState =
+  let st:t_PolyState = st in
+  let st:t_PolyState =
+    if Core.Slice.len_under_impl b <>. 0sz
+    then
+      let st:t_PolyState =
+        {
+          st with
+          Poly1305.PolyState.f_acc
+          =
+          (poly1305_encode_last pad_len b +. st.Poly1305.PolyState.f_acc) *.
+          st.Poly1305.PolyState.f_r
+        }
+      in
+      st
+    else st
+  in
+  st
+
+let poly1305_update (m: slice u8) (st: t_PolyState) : t_PolyState =
+  let st:t_PolyState = poly1305_update_blocks m st in
+  let last:slice u8 =
+    Core.Slice.Iter.remainder_under_impl_87 (Core.Slice.chunks_exact_under_impl m v_BLOCKSIZE)
+  in
+  poly1305_update_last (Core.Slice.len_under_impl last) last st
+
+let poly1305_finish (st: t_PolyState) : array u8 16sz =
+  let n:u128 =
+    Core.Num.from_le_bytes_under_impl_10 (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into
+              st.Poly1305.PolyState.f_key.[ {
+                  Core.Ops.Range.Range.f_start = 16sz;
+                  Core.Ops.Range.Range.f_end = 32sz
+                } ]))
+  in
+  let aby:array u8 17sz = Poly1305.Hacspec_helper.NatMod.to_le_bytes st.Poly1305.PolyState.f_acc in
+  let a:u128 =
+    Core.Num.from_le_bytes_under_impl_10 (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into
+              aby.[ { Core.Ops.Range.Range.f_start = 0sz; Core.Ops.Range.Range.f_end = 16sz } ]))
+  in
+  Core.Num.to_le_bytes_under_impl_10 (Core.Num.wrapping_add_under_impl_10 a n)
+
+let poly1305 (m: slice u8) (key: array u8 32sz) : array u8 16sz =
+  let st:t_PolyState = poly1305_init key in
+  let st:t_PolyState = poly1305_update m st in
+  poly1305_finish st
\ No newline at end of file
diff --git a/poly1305-rust/src/hacspec_helper.rs b/poly1305-rust/src/hacspec_helper.rs
new file mode 100644
index 0000000..445bd57
--- /dev/null
+++ b/poly1305-rust/src/hacspec_helper.rs
@@ -0,0 +1,146 @@
+/// This has to come from the lib.
+
+pub trait NatMod<const LEN: usize> {
+    const MODULUS: [u8; LEN];
+    const MODULUS_STR: &'static str;
+    const ZERO: [u8; LEN];
+
+    fn new(value: [u8; LEN]) -> Self;
+    fn value(&self) -> &[u8];
+
+    /// Add self with `rhs` and return the result `self + rhs % MODULUS`.
+    fn fadd(self, rhs: Self) -> Self
+    where
+        Self: Sized,
+    {
+        let lhs = num_bigint::BigUint::from_bytes_be(self.value());
+        let rhs = num_bigint::BigUint::from_bytes_be(rhs.value());
+        let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS);
+        let res = (lhs + rhs) % modulus;
+        let res = res.to_bytes_be();
+        assert!(res.len() <= LEN);
+        let mut value = Self::ZERO;
+        let offset = LEN - res.len();
+        for i in 0..res.len() {
+            value[offset + i] = res[i];
+        }
+        Self::new(value)
+    }
+
+    /// Multiply self with `rhs` and return the result `self * rhs % MODULUS`.
+    fn fmul(self, rhs: Self) -> Self
+    where
+        Self: Sized,
+    {
+        let lhs = num_bigint::BigUint::from_bytes_be(self.value());
+        let rhs = num_bigint::BigUint::from_bytes_be(rhs.value());
+        let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS);
+        let res = (lhs * rhs) % modulus;
+        let res = res.to_bytes_be();
+        assert!(res.len() <= LEN);
+        let mut value = Self::ZERO;
+        let offset = LEN - res.len();
+        for i in 0..res.len() {
+            value[offset + i] = res[i];
+        }
+        Self::new(value)
+    }
+
+    /// Zero element
+    fn zero() -> Self
+    where
+        Self: Sized,
+    {
+        Self::new(Self::ZERO)
+    }
+
+    /// Returns 2 to the power of the argument
+    fn pow2(x: usize) -> Self
+    where
+        Self: Sized,
+    {
+        let res = num_bigint::BigUint::from(1u32) << x;
+        Self::from_bigint(res)
+    }
+
+    /// Create a new [`#ident`] from a `u128` literal.
+    fn from_u128(literal: u128) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from(literal))
+    }
+
+    /// Create a new [`#ident`] from a little endian byte slice.
+    fn from_le_bytes(bytes: &[u8]) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from_bytes_le(bytes))
+    }
+
+    /// Create a new [`#ident`] from a little endian byte slice.
+    fn from_be_bytes(bytes: &[u8]) -> Self
+    where
+        Self: Sized,
+    {
+        Self::from_bigint(num_bigint::BigUint::from_bytes_be(bytes))
+    }
+
+    fn to_le_bytes(self) -> [u8; LEN]
+    where
+        Self: Sized,
+    {
+        Self::pad(&num_bigint::BigUint::from_bytes_be(self.value()).to_bytes_le())
+    }
+
+    /// Get hex string representation of this.
+    fn to_hex(&self) -> String {
+        let strs: Vec<String> = self.value().iter().map(|b| format!("{:02x}", b)).collect();
+        strs.join("")
+    }
+
+    /// New from hex string
+    fn from_hex(hex: &str) -> Self
+    where
+        Self: Sized,
+    {
+        assert!(hex.len() % 2 == 0);
+        let l = hex.len() / 2;
+        assert!(l <= LEN);
+        let mut value = [0u8; LEN];
+        let skip = LEN - l;
+        for i in 0..l {
+            value[skip + i] = u8::from_str_radix(&hex[2 * i..2 * i + 2], 16)
+                .expect("An unexpected error occurred.");
+        }
+        Self::new(value)
+    }
+
+    fn pad(bytes: &[u8]) -> [u8; LEN] {
+        let mut value = [0u8; LEN];
+        let upper = value.len();
+        let lower = upper - bytes.len();
+        value[lower..upper].copy_from_slice(&bytes);
+        value
+    }
+
+    fn from_bigint(x: num_bigint::BigUint) -> Self
+    where
+        Self: Sized,
+    {
+        let max_value = Self::MODULUS;
+        assert!(
+            x <= num_bigint::BigUint::from_bytes_be(&max_value),
+            "{} is too large for type {}!",
+            x,
+            stringify!($ident)
+        );
+        let repr = x.to_bytes_be();
+        if repr.len() > LEN {
+            panic!("{} is too large for this type", x)
+        }
+
+        Self::new(Self::pad(&repr))
+    }
+}
diff --git a/poly1305-rust/src/poly1305.rs b/poly1305-rust/src/poly1305.rs
new file mode 100644
index 0000000..d943f59
--- /dev/null
+++ b/poly1305-rust/src/poly1305.rs
@@ -0,0 +1,104 @@
+// WARNING:
+// This spec does not provide secret independence, and treats all keys as public.
+// Consequently, it should only be used as a FORMAL SPEC, NOT as a reference implementation.
+
+mod hacspec_helper;
+use hacspec_helper::*;
+use natmod::nat_mod;
+
+// Type definitions for use in poly1305.
+pub type PolyKey = [u8; 32];
+
+const BLOCKSIZE: usize = 16;
+
+// These are type aliases for convenience
+pub type PolyBlock = [u8; BLOCKSIZE];
+
+// These are actual types; fixed-length arrays.
+type Poly1305Tag = [u8; BLOCKSIZE];
+
+// A byte sequence of length <= BLOCKSIZE
+pub type SubBlock = Vec<u8>;
+
+// A length <= BLOCKSIZE
+pub type BlockIndex = usize;
+
+// This defines the field for modulo 2^130-5.
+// In particular `FieldElement` and `FieldCanvas` are defined.
+// The `FieldCanvas` is an integer type with 131-bit (to hold 2*(2^130-5)).
+// The `FieldElement` is a natural integer modulo 2^130-5.
+#[nat_mod("03fffffffffffffffffffffffffffffffb", 17)]
+struct FieldElement {}
+
+// Internal Poly1305 State
+pub struct PolyState {
+    acc: FieldElement,
+    r: FieldElement,
+    key: PolyKey,
+}
+
+pub fn poly1305_encode_r(b: PolyBlock) -> FieldElement {
+    let mut n = u128::from_le_bytes(b);
+    n = n & 0x0fff_fffc_0fff_fffc_0fff_fffc_0fff_ffffu128;
+    FieldElement::from_u128(n)
+}
+
+pub fn poly1305_encode_block(b: PolyBlock) -> FieldElement {
+    let f = FieldElement::from_le_bytes(&b);
+    f + FieldElement::pow2(128)
+}
+
+// In Poly1305 as used in this spec, pad_len is always the length of b, i.e. there is no padding
+// In Chacha20Poly1305, pad_len is set to BLOCKSIZE
+pub fn poly1305_encode_last(pad_len: BlockIndex, b: &[u8]) -> FieldElement {
+    let f = FieldElement::from_le_bytes(b);
+    f + FieldElement::pow2(8 * pad_len)
+}
+
+pub fn poly1305_init(key: PolyKey) -> PolyState {
+    let r = poly1305_encode_r(key[0..16].try_into().unwrap());
+    PolyState {
+        acc: FieldElement::zero(),
+        r,
+        key,
+    }
+}
+
+pub fn poly1305_update_block(b: PolyBlock, mut st: PolyState) -> PolyState {
+    st.acc = (poly1305_encode_block(b) + st.acc) * st.r;
+    st
+}
+
+pub fn poly1305_update_blocks(m: &[u8], mut st: PolyState) -> PolyState {
+    for chunk in m.chunks_exact(BLOCKSIZE) {
+        st = poly1305_update_block(chunk.try_into().unwrap(), st);
+    }
+    st
+}
+
+pub fn poly1305_update_last(pad_len: usize, b: &[u8], st: PolyState) -> PolyState {
+    let mut st = st;
+    if b.len() != 0 {
+        st.acc = (poly1305_encode_last(pad_len, b) + st.acc) * st.r;
+    }
+    st
+}
+
+pub fn poly1305_update(m: &[u8], st: PolyState) -> PolyState {
+    let st = poly1305_update_blocks(m, st);
+    let last = m.chunks_exact(BLOCKSIZE).remainder();
+    poly1305_update_last(last.len(), last, st)
+}
+
+pub fn poly1305_finish(st: PolyState) -> Poly1305Tag {
+    let n = u128::from_le_bytes(st.key[16..32].try_into().unwrap());
+    let aby = st.acc.to_le_bytes();
+    let a = u128::from_le_bytes(aby[0..16].try_into().unwrap());
+    (a.wrapping_add(n)).to_le_bytes()
+}
+
+pub fn poly1305(m: &[u8], key: PolyKey) -> Poly1305Tag {
+    let mut st = poly1305_init(key);
+    st = poly1305_update(m, st);
+    poly1305_finish(st)
+}
diff --git a/poly1305-rust/tests/test_poly1305.rs b/poly1305-rust/tests/test_poly1305.rs
new file mode 100644
index 0000000..6273363
--- /dev/null
+++ b/poly1305-rust/tests/test_poly1305.rs
@@ -0,0 +1,88 @@
+use poly1305::*;
+
+// TODO: More tests from openssl should be added
+//       https://github.com/openssl/openssl/blob/58cd83f83cb0fb4c0eaf97aef1c65996c0936a7d/test/recipes/30-test_evp_data/evpmac_poly1305.txt
+
+#[test]
+fn basic() {
+    // RFC 7539 Test Vectors
+    let msg = [
+        0x43, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x67, 0x72, 0x61, 0x70, 0x68, 0x69, 0x63, 0x20, 0x46,
+        0x6f, 0x72, 0x75, 0x6d, 0x20, 0x52, 0x65, 0x73, 0x65, 0x61, 0x72, 0x63, 0x68, 0x20, 0x47,
+        0x72, 0x6f, 0x75, 0x70,
+    ];
+    let k = [
+        0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33, 0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06,
+        0xa8, 0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd, 0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49,
+        0xf5, 0x1b,
+    ];
+    let expected = [
+        0xa8, 0x06, 0x1d, 0xc1, 0x30, 0x51, 0x36, 0xc6, 0xc2, 0x2b, 0x8b, 0xaf, 0x0c, 0x01, 0x27,
+        0xa9,
+    ];
+    let computed = poly1305(&msg, k);
+    assert_eq!(expected, computed)
+}
+
+#[test]
+fn openssl() {
+    // RFC 7539 Test Vectors
+    let msg = [
+        0x43, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x67, 0x72, 0x61, 0x70, 0x68, 0x69, 0x63, 0x20, 0x46,
+        0x6f, 0x72, 0x75, 0x6d, 0x20, 0x52, 0x65, 0x73, 0x65, 0x61, 0x72, 0x63, 0x68, 0x20, 0x47,
+        0x72, 0x6f, 0x75, 0x70,
+    ];
+    let k = [
+        0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33, 0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06,
+        0xa8, 0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd, 0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49,
+        0xf5, 0x1b,
+    ];
+    let expected = [
+        0xa8, 0x06, 0x1d, 0xc1, 0x30, 0x51, 0x36, 0xc6, 0xc2, 0x2b, 0x8b, 0xaf, 0x0c, 0x01, 0x27,
+        0xa9,
+    ];
+    let computed = poly1305(&msg, k);
+    assert_eq!(expected, computed)
+}
+
+#[test]
+fn corner_case() {
+    let msg = [
+        0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, 0x69, 0x73, 0x73, 0x69, 0x6f, 0x6e, 0x20,
+        0x74, 0x6f, 0x20, 0x74, 0x68, 0x65, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74,
+        0x65, 0x6e, 0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, 0x68, 0x65, 0x20, 0x43, 0x6f,
+        0x6e, 0x74, 0x72, 0x69, 0x62, 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, 0x6f, 0x72, 0x20, 0x70,
+        0x75, 0x62, 0x6c, 0x69, 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, 0x20, 0x61, 0x73, 0x20, 0x61,
+        0x6c, 0x6c, 0x20, 0x6f, 0x72, 0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, 0x20, 0x61,
+        0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, 0x74,
+        0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x20, 0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61,
+        0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e,
+        0x74, 0x20, 0x6d, 0x61, 0x64, 0x65, 0x20, 0x77, 0x69, 0x74, 0x68, 0x69, 0x6e, 0x20, 0x74,
+        0x68, 0x65, 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74, 0x20, 0x6f, 0x66, 0x20, 0x61,
+        0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x61, 0x63, 0x74, 0x69, 0x76, 0x69, 0x74, 0x79,
+        0x20, 0x69, 0x73, 0x20, 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, 0x65, 0x72, 0x65, 0x64, 0x20,
+        0x61, 0x6e, 0x20, 0x22, 0x49, 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, 0x69,
+        0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, 0x22, 0x2e, 0x20, 0x53, 0x75, 0x63, 0x68, 0x20, 0x73,
+        0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75,
+        0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65,
+        0x6e, 0x74, 0x73, 0x20, 0x69, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x73, 0x65, 0x73,
+        0x73, 0x69, 0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, 0x77, 0x65, 0x6c, 0x6c, 0x20,
+        0x61, 0x73, 0x20, 0x77, 0x72, 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, 0x61, 0x6e, 0x64, 0x20,
+        0x65, 0x6c, 0x65, 0x63, 0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, 0x20, 0x63, 0x6f, 0x6d, 0x6d,
+        0x75, 0x6e, 0x69, 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, 0x64, 0x65,
+        0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, 0x72,
+        0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c, 0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61,
+        0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65, 0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f,
+    ];
+    let k = [
+        0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+        0x00, 0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a,
+        0x86, 0x3e,
+    ];
+    let expected = [
+        0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a, 0x86,
+        0x3e,
+    ];
+    let computed = poly1305(&msg, k);
+    assert_eq!(expected, computed)
+}